For a proof by Jech related to AC implications, I've been looking for a
theorem along the lines of
$e T = { <. y , z >. | ... } $.
$p |- ( ( R We A /\ R Se A /\ A. x e. A S We B ) -> T We U_ x e. A B ) $.
(S and B are to be read as S(x) and B(x). Also, a version with more sethood
hypotheses would also be acceptable, since my specific use case is along
the lines of ( ( A e. On /\ A. x e. A ( f ` x ) We ( g ` x ) ) -> U_ x e. A
( g ` x ) e. dom card ).)
Intuitively, the idea for proving it is relatively simple (Jech elides it
with an "easily"): Given y and z, we first compare the R-minimal x such
that y e. B(x) with the R-minimal x' such that z e. B(x'); if x = x', then
we can fall back to comparing with S(x). In other words, we line up all the
B(x)s in order of their xs, then sort by S(x) within each B(x).
It's also pretty simple to write out a T implementing this procedure, but
working out the proof has me stumped. I tried directly working out the
conditions for T Fr U_ x e. A B and T Or U_ x e. A B, but I got lost in
extremely long lines of iota_ soup. So I looked into the existing theorems
for well-orders, but they don't seem helpful. fnwe
<https://us.metamath.org/mpeuni/fnwe.html> looked somewhat nice, except
that it requires a single S relation, which would be very messy to paste
together. Another idea was to use an injection from U_ x e. A B to <. A ,
U_ x e. A B >. with a lexicographical well-order, but wexp
<https://us.metamath.org/mpeuni/wexp.html> & co. would similarly require
the S relations to be pasted together.
Is there some clever way of proving this with existing theorems, or will I
have to do this the hard way?
Thank you,
Matthew House
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/c6ea2730-ed64-4464-9dfb-9c1cc173654an%40googlegroups.com.
