Metamath Proof Explorer

Theorem aomclem4

Description: Lemma for dfac11 . Limit case. Patch together well-orderings constructed so far using fnwe2 to cover the limit rank. (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses aomclem4.f 
|- F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }
aomclem4.on 
|- ( ph -> dom z e. On )
aomclem4.su 
|- ( ph -> dom z = U. dom z )
aomclem4.we 
|- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )
Assertion aomclem4 
|- ( ph -> F We ( R1 ` dom z ) )

Proof

Step Hyp Ref Expression
1 aomclem4.f 
 |-  F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }
2 aomclem4.on 
 |-  ( ph -> dom z e. On )
3 aomclem4.su 
 |-  ( ph -> dom z = U. dom z )
4 aomclem4.we 
 |-  ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )
5 suceq 
 |-  ( c = ( rank ` a ) -> suc c = suc ( rank ` a ) )
6 5 fveq2d 
 |-  ( c = ( rank ` a ) -> ( z ` suc c ) = ( z ` suc ( rank ` a ) ) )
7 r1fnon 
 |-  R1 Fn On
8 fnfun 
 |-  ( R1 Fn On -> Fun R1 )
9 7 8 ax-mp 
 |-  Fun R1
10 7 fndmi 
 |-  dom R1 = On
11 10 eqimss2i 
 |-  On C_ dom R1
12 9 11 pm3.2i 
 |-  ( Fun R1 /\ On C_ dom R1 )
13 funfvima2 
 |-  ( ( Fun R1 /\ On C_ dom R1 ) -> ( dom z e. On -> ( R1 ` dom z ) e. ( R1 " On ) ) )
14 12 2 13 mpsyl 
 |-  ( ph -> ( R1 ` dom z ) e. ( R1 " On ) )
15 elssuni 
 |-  ( ( R1 ` dom z ) e. ( R1 " On ) -> ( R1 ` dom z ) C_ U. ( R1 " On ) )
16 14 15 syl 
 |-  ( ph -> ( R1 ` dom z ) C_ U. ( R1 " On ) )
17 16 sselda 
 |-  ( ( ph /\ b e. ( R1 ` dom z ) ) -> b e. U. ( R1 " On ) )
18 rankidb 
 |-  ( b e. U. ( R1 " On ) -> b e. ( R1 ` suc ( rank ` b ) ) )
19 17 18 syl 
 |-  ( ( ph /\ b e. ( R1 ` dom z ) ) -> b e. ( R1 ` suc ( rank ` b ) ) )
20 suceq 
 |-  ( ( rank ` b ) = ( rank ` a ) -> suc ( rank ` b ) = suc ( rank ` a ) )
21 20 fveq2d 
 |-  ( ( rank ` b ) = ( rank ` a ) -> ( R1 ` suc ( rank ` b ) ) = ( R1 ` suc ( rank ` a ) ) )
22 21 eleq2d 
 |-  ( ( rank ` b ) = ( rank ` a ) -> ( b e. ( R1 ` suc ( rank ` b ) ) <-> b e. ( R1 ` suc ( rank ` a ) ) ) )
23 19 22 syl5ibcom 
 |-  ( ( ph /\ b e. ( R1 ` dom z ) ) -> ( ( rank ` b ) = ( rank ` a ) -> b e. ( R1 ` suc ( rank ` a ) ) ) )
24 23 expimpd 
 |-  ( ph -> ( ( b e. ( R1 ` dom z ) /\ ( rank ` b ) = ( rank ` a ) ) -> b e. ( R1 ` suc ( rank ` a ) ) ) )
25 24 ss2abdv 
 |-  ( ph -> { b | ( b e. ( R1 ` dom z ) /\ ( rank ` b ) = ( rank ` a ) ) } C_ { b | b e. ( R1 ` suc ( rank ` a ) ) } )
26 df-rab 
 |-  { b e. ( R1 ` dom z ) | ( rank ` b ) = ( rank ` a ) } = { b | ( b e. ( R1 ` dom z ) /\ ( rank ` b ) = ( rank ` a ) ) }
27 abid1 
 |-  ( R1 ` suc ( rank ` a ) ) = { b | b e. ( R1 ` suc ( rank ` a ) ) }
28 25 26 27 3sstr4g 
 |-  ( ph -> { b e. ( R1 ` dom z ) | ( rank ` b ) = ( rank ` a ) } C_ ( R1 ` suc ( rank ` a ) ) )
29 28 adantr 
 |-  ( ( ph /\ a e. ( R1 ` dom z ) ) -> { b e. ( R1 ` dom z ) | ( rank ` b ) = ( rank ` a ) } C_ ( R1 ` suc ( rank ` a ) ) )
30 fveq2 
 |-  ( b = suc ( rank ` a ) -> ( z ` b ) = ( z ` suc ( rank ` a ) ) )
31 fveq2 
 |-  ( b = suc ( rank ` a ) -> ( R1 ` b ) = ( R1 ` suc ( rank ` a ) ) )
32 30 31 weeq12d 
 |-  ( b = suc ( rank ` a ) -> ( ( z ` b ) We ( R1 ` b ) <-> ( z ` suc ( rank ` a ) ) We ( R1 ` suc ( rank ` a ) ) ) )
33 fveq2 
 |-  ( a = b -> ( z ` a ) = ( z ` b ) )
34 fveq2 
 |-  ( a = b -> ( R1 ` a ) = ( R1 ` b ) )
35 33 34 weeq12d 
 |-  ( a = b -> ( ( z ` a ) We ( R1 ` a ) <-> ( z ` b ) We ( R1 ` b ) ) )
36 35 cbvralvw 
 |-  ( A. a e. dom z ( z ` a ) We ( R1 ` a ) <-> A. b e. dom z ( z ` b ) We ( R1 ` b ) )
37 4 36 sylib 
 |-  ( ph -> A. b e. dom z ( z ` b ) We ( R1 ` b ) )
38 37 adantr 
 |-  ( ( ph /\ a e. ( R1 ` dom z ) ) -> A. b e. dom z ( z ` b ) We ( R1 ` b ) )
39 rankr1ai 
 |-  ( a e. ( R1 ` dom z ) -> ( rank ` a ) e. dom z )
40 39 adantl 
 |-  ( ( ph /\ a e. ( R1 ` dom z ) ) -> ( rank ` a ) e. dom z )
41 eloni 
 |-  ( dom z e. On -> Ord dom z )
42 2 41 syl 
 |-  ( ph -> Ord dom z )
43 limsuc2 
 |-  ( ( Ord dom z /\ dom z = U. dom z ) -> ( ( rank ` a ) e. dom z <-> suc ( rank ` a ) e. dom z ) )
44 42 3 43 syl2anc 
 |-  ( ph -> ( ( rank ` a ) e. dom z <-> suc ( rank ` a ) e. dom z ) )
45 44 adantr 
 |-  ( ( ph /\ a e. ( R1 ` dom z ) ) -> ( ( rank ` a ) e. dom z <-> suc ( rank ` a ) e. dom z ) )
46 40 45 mpbid 
 |-  ( ( ph /\ a e. ( R1 ` dom z ) ) -> suc ( rank ` a ) e. dom z )
47 32 38 46 rspcdva 
 |-  ( ( ph /\ a e. ( R1 ` dom z ) ) -> ( z ` suc ( rank ` a ) ) We ( R1 ` suc ( rank ` a ) ) )
48 wess 
 |-  ( { b e. ( R1 ` dom z ) | ( rank ` b ) = ( rank ` a ) } C_ ( R1 ` suc ( rank ` a ) ) -> ( ( z ` suc ( rank ` a ) ) We ( R1 ` suc ( rank ` a ) ) -> ( z ` suc ( rank ` a ) ) We { b e. ( R1 ` dom z ) | ( rank ` b ) = ( rank ` a ) } ) )
49 29 47 48 sylc 
 |-  ( ( ph /\ a e. ( R1 ` dom z ) ) -> ( z ` suc ( rank ` a ) ) We { b e. ( R1 ` dom z ) | ( rank ` b ) = ( rank ` a ) } )
50 rankf 
 |-  rank : U. ( R1 " On ) --> On
51 50 a1i 
 |-  ( ph -> rank : U. ( R1 " On ) --> On )
52 51 16 fssresd 
 |-  ( ph -> ( rank |` ( R1 ` dom z ) ) : ( R1 ` dom z ) --> On )
53 epweon 
 |-  _E We On
54 53 a1i 
 |-  ( ph -> _E We On )
55 6 1 49 52 54 fnwe2 
 |-  ( ph -> F We ( R1 ` dom z ) )