Metamath Proof Explorer


Theorem aomclem1

Description: Lemma for dfac11 . This is the beginning of the proof that multiple choice is equivalent to choice. Our goal is to construct, by transfinite recursion, a well-ordering of ( R1A ) . In what follows, A is the index of the rank we wish to well-order, z is the collection of well-orderings constructed so far, dom z is the set of ordinal indices of constructed ranks i.e. the next rank to construct, and y is a postulated multiple-choice function.

Successor case 1, define a simple ordering from the well-ordered predecessor. (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypotheses aomclem1.b
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }
aomclem1.on
|- ( ph -> dom z e. On )
aomclem1.su
|- ( ph -> dom z = suc U. dom z )
aomclem1.we
|- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )
Assertion aomclem1
|- ( ph -> B Or ( R1 ` dom z ) )

Proof

Step Hyp Ref Expression
1 aomclem1.b
 |-  B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }
2 aomclem1.on
 |-  ( ph -> dom z e. On )
3 aomclem1.su
 |-  ( ph -> dom z = suc U. dom z )
4 aomclem1.we
 |-  ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )
5 fvex
 |-  ( R1 ` U. dom z ) e. _V
6 vex
 |-  z e. _V
7 6 dmex
 |-  dom z e. _V
8 7 uniex
 |-  U. dom z e. _V
9 8 sucid
 |-  U. dom z e. suc U. dom z
10 9 3 eleqtrrid
 |-  ( ph -> U. dom z e. dom z )
11 fveq2
 |-  ( a = U. dom z -> ( z ` a ) = ( z ` U. dom z ) )
12 fveq2
 |-  ( a = U. dom z -> ( R1 ` a ) = ( R1 ` U. dom z ) )
13 11 12 weeq12d
 |-  ( a = U. dom z -> ( ( z ` a ) We ( R1 ` a ) <-> ( z ` U. dom z ) We ( R1 ` U. dom z ) ) )
14 13 rspcva
 |-  ( ( U. dom z e. dom z /\ A. a e. dom z ( z ` a ) We ( R1 ` a ) ) -> ( z ` U. dom z ) We ( R1 ` U. dom z ) )
15 10 4 14 syl2anc
 |-  ( ph -> ( z ` U. dom z ) We ( R1 ` U. dom z ) )
16 1 wepwso
 |-  ( ( ( R1 ` U. dom z ) e. _V /\ ( z ` U. dom z ) We ( R1 ` U. dom z ) ) -> B Or ~P ( R1 ` U. dom z ) )
17 5 15 16 sylancr
 |-  ( ph -> B Or ~P ( R1 ` U. dom z ) )
18 3 fveq2d
 |-  ( ph -> ( R1 ` dom z ) = ( R1 ` suc U. dom z ) )
19 onuni
 |-  ( dom z e. On -> U. dom z e. On )
20 r1suc
 |-  ( U. dom z e. On -> ( R1 ` suc U. dom z ) = ~P ( R1 ` U. dom z ) )
21 2 19 20 3syl
 |-  ( ph -> ( R1 ` suc U. dom z ) = ~P ( R1 ` U. dom z ) )
22 18 21 eqtrd
 |-  ( ph -> ( R1 ` dom z ) = ~P ( R1 ` U. dom z ) )
23 soeq2
 |-  ( ( R1 ` dom z ) = ~P ( R1 ` U. dom z ) -> ( B Or ( R1 ` dom z ) <-> B Or ~P ( R1 ` U. dom z ) ) )
24 22 23 syl
 |-  ( ph -> ( B Or ( R1 ` dom z ) <-> B Or ~P ( R1 ` U. dom z ) ) )
25 17 24 mpbird
 |-  ( ph -> B Or ( R1 ` dom z ) )