Metamath Proof Explorer

Theorem dfac12lem3

Description: Lemma for dfac12 . (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Hypotheses dfac12.1 
|- ( ph -> A e. On )
dfac12.3 
|- ( ph -> F : ~P ( har ` ( R1 ` A ) ) -1-1-> On )
dfac12.4 
|- G = recs ( ( x e. _V |-> ( y e. ( R1 ` dom x ) |-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) ) ) ) )
Assertion dfac12lem3 
|- ( ph -> ( R1 ` A ) e. dom card )

Proof

Step Hyp Ref Expression
1 dfac12.1 
 |-  ( ph -> A e. On )
2 dfac12.3 
 |-  ( ph -> F : ~P ( har ` ( R1 ` A ) ) -1-1-> On )
3 dfac12.4 
 |-  G = recs ( ( x e. _V |-> ( y e. ( R1 ` dom x ) |-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) ) ) ) )
4 fvex 
 |-  ( G ` A ) e. _V
5 4 rnex 
 |-  ran ( G ` A ) e. _V
6 ssid 
 |-  A C_ A
7 sseq1 
 |-  ( m = n -> ( m C_ A <-> n C_ A ) )
8 fveq2 
 |-  ( m = n -> ( G ` m ) = ( G ` n ) )
9 f1eq1 
 |-  ( ( G ` m ) = ( G ` n ) -> ( ( G ` m ) : ( R1 ` m ) -1-1-> On <-> ( G ` n ) : ( R1 ` m ) -1-1-> On ) )
10 8 9 syl 
 |-  ( m = n -> ( ( G ` m ) : ( R1 ` m ) -1-1-> On <-> ( G ` n ) : ( R1 ` m ) -1-1-> On ) )
11 fveq2 
 |-  ( m = n -> ( R1 ` m ) = ( R1 ` n ) )
12 f1eq2 
 |-  ( ( R1 ` m ) = ( R1 ` n ) -> ( ( G ` n ) : ( R1 ` m ) -1-1-> On <-> ( G ` n ) : ( R1 ` n ) -1-1-> On ) )
13 11 12 syl 
 |-  ( m = n -> ( ( G ` n ) : ( R1 ` m ) -1-1-> On <-> ( G ` n ) : ( R1 ` n ) -1-1-> On ) )
14 10 13 bitrd 
 |-  ( m = n -> ( ( G ` m ) : ( R1 ` m ) -1-1-> On <-> ( G ` n ) : ( R1 ` n ) -1-1-> On ) )
15 7 14 imbi12d 
 |-  ( m = n -> ( ( m C_ A -> ( G ` m ) : ( R1 ` m ) -1-1-> On ) <-> ( n C_ A -> ( G ` n ) : ( R1 ` n ) -1-1-> On ) ) )
16 15 imbi2d 
 |-  ( m = n -> ( ( ph -> ( m C_ A -> ( G ` m ) : ( R1 ` m ) -1-1-> On ) ) <-> ( ph -> ( n C_ A -> ( G ` n ) : ( R1 ` n ) -1-1-> On ) ) ) )
17 sseq1 
 |-  ( m = A -> ( m C_ A <-> A C_ A ) )
18 fveq2 
 |-  ( m = A -> ( G ` m ) = ( G ` A ) )
19 f1eq1 
 |-  ( ( G ` m ) = ( G ` A ) -> ( ( G ` m ) : ( R1 ` m ) -1-1-> On <-> ( G ` A ) : ( R1 ` m ) -1-1-> On ) )
20 18 19 syl 
 |-  ( m = A -> ( ( G ` m ) : ( R1 ` m ) -1-1-> On <-> ( G ` A ) : ( R1 ` m ) -1-1-> On ) )
21 fveq2 
 |-  ( m = A -> ( R1 ` m ) = ( R1 ` A ) )
22 f1eq2 
 |-  ( ( R1 ` m ) = ( R1 ` A ) -> ( ( G ` A ) : ( R1 ` m ) -1-1-> On <-> ( G ` A ) : ( R1 ` A ) -1-1-> On ) )
23 21 22 syl 
 |-  ( m = A -> ( ( G ` A ) : ( R1 ` m ) -1-1-> On <-> ( G ` A ) : ( R1 ` A ) -1-1-> On ) )
24 20 23 bitrd 
 |-  ( m = A -> ( ( G ` m ) : ( R1 ` m ) -1-1-> On <-> ( G ` A ) : ( R1 ` A ) -1-1-> On ) )
25 17 24 imbi12d 
 |-  ( m = A -> ( ( m C_ A -> ( G ` m ) : ( R1 ` m ) -1-1-> On ) <-> ( A C_ A -> ( G ` A ) : ( R1 ` A ) -1-1-> On ) ) )
26 25 imbi2d 
 |-  ( m = A -> ( ( ph -> ( m C_ A -> ( G ` m ) : ( R1 ` m ) -1-1-> On ) ) <-> ( ph -> ( A C_ A -> ( G ` A ) : ( R1 ` A ) -1-1-> On ) ) ) )
27 r19.21v 
 |-  ( A. n e. m ( ph -> ( n C_ A -> ( G ` n ) : ( R1 ` n ) -1-1-> On ) ) <-> ( ph -> A. n e. m ( n C_ A -> ( G ` n ) : ( R1 ` n ) -1-1-> On ) ) )
28 eloni 
 |-  ( m e. On -> Ord m )
29 28 ad2antrl 
 |-  ( ( ph /\ ( m e. On /\ m C_ A ) ) -> Ord m )
30 ordelss 
 |-  ( ( Ord m /\ n e. m ) -> n C_ m )
31 29 30 sylan 
 |-  ( ( ( ph /\ ( m e. On /\ m C_ A ) ) /\ n e. m ) -> n C_ m )
32 simplrr 
 |-  ( ( ( ph /\ ( m e. On /\ m C_ A ) ) /\ n e. m ) -> m C_ A )
33 31 32 sstrd 
 |-  ( ( ( ph /\ ( m e. On /\ m C_ A ) ) /\ n e. m ) -> n C_ A )
34 pm5.5 
 |-  ( n C_ A -> ( ( n C_ A -> ( G ` n ) : ( R1 ` n ) -1-1-> On ) <-> ( G ` n ) : ( R1 ` n ) -1-1-> On ) )
35 33 34 syl 
 |-  ( ( ( ph /\ ( m e. On /\ m C_ A ) ) /\ n e. m ) -> ( ( n C_ A -> ( G ` n ) : ( R1 ` n ) -1-1-> On ) <-> ( G ` n ) : ( R1 ` n ) -1-1-> On ) )
36 35 ralbidva 
 |-  ( ( ph /\ ( m e. On /\ m C_ A ) ) -> ( A. n e. m ( n C_ A -> ( G ` n ) : ( R1 ` n ) -1-1-> On ) <-> A. n e. m ( G ` n ) : ( R1 ` n ) -1-1-> On ) )
37 1 ad2antrr 
 |-  ( ( ( ph /\ ( m e. On /\ m C_ A ) ) /\ A. n e. m ( G ` n ) : ( R1 ` n ) -1-1-> On ) -> A e. On )
38 2 ad2antrr 
 |-  ( ( ( ph /\ ( m e. On /\ m C_ A ) ) /\ A. n e. m ( G ` n ) : ( R1 ` n ) -1-1-> On ) -> F : ~P ( har ` ( R1 ` A ) ) -1-1-> On )
39 simplrl 
 |-  ( ( ( ph /\ ( m e. On /\ m C_ A ) ) /\ A. n e. m ( G ` n ) : ( R1 ` n ) -1-1-> On ) -> m e. On )
40 eqid 
 |-  ( `' OrdIso ( _E , ran ( G ` U. m ) ) o. ( G ` U. m ) ) = ( `' OrdIso ( _E , ran ( G ` U. m ) ) o. ( G ` U. m ) )
41 simplrr 
 |-  ( ( ( ph /\ ( m e. On /\ m C_ A ) ) /\ A. n e. m ( G ` n ) : ( R1 ` n ) -1-1-> On ) -> m C_ A )
42 simpr 
 |-  ( ( ( ph /\ ( m e. On /\ m C_ A ) ) /\ A. n e. m ( G ` n ) : ( R1 ` n ) -1-1-> On ) -> A. n e. m ( G ` n ) : ( R1 ` n ) -1-1-> On )
43 fveq2 
 |-  ( n = z -> ( G ` n ) = ( G ` z ) )
44 f1eq1 
 |-  ( ( G ` n ) = ( G ` z ) -> ( ( G ` n ) : ( R1 ` n ) -1-1-> On <-> ( G ` z ) : ( R1 ` n ) -1-1-> On ) )
45 43 44 syl 
 |-  ( n = z -> ( ( G ` n ) : ( R1 ` n ) -1-1-> On <-> ( G ` z ) : ( R1 ` n ) -1-1-> On ) )
46 fveq2 
 |-  ( n = z -> ( R1 ` n ) = ( R1 ` z ) )
47 f1eq2 
 |-  ( ( R1 ` n ) = ( R1 ` z ) -> ( ( G ` z ) : ( R1 ` n ) -1-1-> On <-> ( G ` z ) : ( R1 ` z ) -1-1-> On ) )
48 46 47 syl 
 |-  ( n = z -> ( ( G ` z ) : ( R1 ` n ) -1-1-> On <-> ( G ` z ) : ( R1 ` z ) -1-1-> On ) )
49 45 48 bitrd 
 |-  ( n = z -> ( ( G ` n ) : ( R1 ` n ) -1-1-> On <-> ( G ` z ) : ( R1 ` z ) -1-1-> On ) )
50 49 cbvralvw 
 |-  ( A. n e. m ( G ` n ) : ( R1 ` n ) -1-1-> On <-> A. z e. m ( G ` z ) : ( R1 ` z ) -1-1-> On )
51 42 50 sylib 
 |-  ( ( ( ph /\ ( m e. On /\ m C_ A ) ) /\ A. n e. m ( G ` n ) : ( R1 ` n ) -1-1-> On ) -> A. z e. m ( G ` z ) : ( R1 ` z ) -1-1-> On )
52 37 38 3 39 40 41 51 dfac12lem2 
 |-  ( ( ( ph /\ ( m e. On /\ m C_ A ) ) /\ A. n e. m ( G ` n ) : ( R1 ` n ) -1-1-> On ) -> ( G ` m ) : ( R1 ` m ) -1-1-> On )
53 52 ex 
 |-  ( ( ph /\ ( m e. On /\ m C_ A ) ) -> ( A. n e. m ( G ` n ) : ( R1 ` n ) -1-1-> On -> ( G ` m ) : ( R1 ` m ) -1-1-> On ) )
54 36 53 sylbid 
 |-  ( ( ph /\ ( m e. On /\ m C_ A ) ) -> ( A. n e. m ( n C_ A -> ( G ` n ) : ( R1 ` n ) -1-1-> On ) -> ( G ` m ) : ( R1 ` m ) -1-1-> On ) )
55 54 expr 
 |-  ( ( ph /\ m e. On ) -> ( m C_ A -> ( A. n e. m ( n C_ A -> ( G ` n ) : ( R1 ` n ) -1-1-> On ) -> ( G ` m ) : ( R1 ` m ) -1-1-> On ) ) )
56 55 com23 
 |-  ( ( ph /\ m e. On ) -> ( A. n e. m ( n C_ A -> ( G ` n ) : ( R1 ` n ) -1-1-> On ) -> ( m C_ A -> ( G ` m ) : ( R1 ` m ) -1-1-> On ) ) )
57 56 expcom 
 |-  ( m e. On -> ( ph -> ( A. n e. m ( n C_ A -> ( G ` n ) : ( R1 ` n ) -1-1-> On ) -> ( m C_ A -> ( G ` m ) : ( R1 ` m ) -1-1-> On ) ) ) )
58 57 a2d 
 |-  ( m e. On -> ( ( ph -> A. n e. m ( n C_ A -> ( G ` n ) : ( R1 ` n ) -1-1-> On ) ) -> ( ph -> ( m C_ A -> ( G ` m ) : ( R1 ` m ) -1-1-> On ) ) ) )
59 27 58 biimtrid 
 |-  ( m e. On -> ( A. n e. m ( ph -> ( n C_ A -> ( G ` n ) : ( R1 ` n ) -1-1-> On ) ) -> ( ph -> ( m C_ A -> ( G ` m ) : ( R1 ` m ) -1-1-> On ) ) ) )
60 16 26 59 tfis3 
 |-  ( A e. On -> ( ph -> ( A C_ A -> ( G ` A ) : ( R1 ` A ) -1-1-> On ) ) )
61 1 60 mpcom 
 |-  ( ph -> ( A C_ A -> ( G ` A ) : ( R1 ` A ) -1-1-> On ) )
62 6 61 mpi 
 |-  ( ph -> ( G ` A ) : ( R1 ` A ) -1-1-> On )
63 f1f 
 |-  ( ( G ` A ) : ( R1 ` A ) -1-1-> On -> ( G ` A ) : ( R1 ` A ) --> On )
64 frn 
 |-  ( ( G ` A ) : ( R1 ` A ) --> On -> ran ( G ` A ) C_ On )
65 62 63 64 3syl 
 |-  ( ph -> ran ( G ` A ) C_ On )
66 onssnum 
 |-  ( ( ran ( G ` A ) e. _V /\ ran ( G ` A ) C_ On ) -> ran ( G ` A ) e. dom card )
67 5 65 66 sylancr 
 |-  ( ph -> ran ( G ` A ) e. dom card )
68 f1f1orn 
 |-  ( ( G ` A ) : ( R1 ` A ) -1-1-> On -> ( G ` A ) : ( R1 ` A ) -1-1-onto-> ran ( G ` A ) )
69 62 68 syl 
 |-  ( ph -> ( G ` A ) : ( R1 ` A ) -1-1-onto-> ran ( G ` A ) )
70 fvex 
 |-  ( R1 ` A ) e. _V
71 70 f1oen 
 |-  ( ( G ` A ) : ( R1 ` A ) -1-1-onto-> ran ( G ` A ) -> ( R1 ` A ) ~~ ran ( G ` A ) )
72 ennum 
 |-  ( ( R1 ` A ) ~~ ran ( G ` A ) -> ( ( R1 ` A ) e. dom card <-> ran ( G ` A ) e. dom card ) )
73 69 71 72 3syl 
 |-  ( ph -> ( ( R1 ` A ) e. dom card <-> ran ( G ` A ) e. dom card ) )
74 67 73 mpbird 
 |-  ( ph -> ( R1 ` A ) e. dom card )