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 ) ) |
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 ) ) |