Metamath Proof Explorer

Theorem dfac12lem1

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 ) ) ) ) ) )
dfac12.5 
|- ( ph -> C e. On )
dfac12.h 
|- H = ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) )
Assertion dfac12lem1 
|- ( ph -> ( G ` C ) = ( y e. ( R1 ` C ) |-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) )

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 dfac12.5 
 |-  ( ph -> C e. On )
5 dfac12.h 
 |-  H = ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) )
6 3 tfr2 
 |-  ( C e. On -> ( G ` C ) = ( ( 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 ) ) ) ) ) ` ( G |` C ) ) )
7 4 6 syl 
 |-  ( ph -> ( G ` C ) = ( ( 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 ) ) ) ) ) ` ( G |` C ) ) )
8 3 tfr1 
 |-  G Fn On
9 fnfun 
 |-  ( G Fn On -> Fun G )
10 8 9 ax-mp 
 |-  Fun G
11 resfunexg 
 |-  ( ( Fun G /\ C e. On ) -> ( G |` C ) e. _V )
12 10 4 11 sylancr 
 |-  ( ph -> ( G |` C ) e. _V )
13 dmeq 
 |-  ( x = ( G |` C ) -> dom x = dom ( G |` C ) )
14 13 fveq2d 
 |-  ( x = ( G |` C ) -> ( R1 ` dom x ) = ( R1 ` dom ( G |` C ) ) )
15 13 unieqd 
 |-  ( x = ( G |` C ) -> U. dom x = U. dom ( G |` C ) )
16 13 15 eqeq12d 
 |-  ( x = ( G |` C ) -> ( dom x = U. dom x <-> dom ( G |` C ) = U. dom ( G |` C ) ) )
17 rneq 
 |-  ( x = ( G |` C ) -> ran x = ran ( G |` C ) )
18 df-ima 
 |-  ( G " C ) = ran ( G |` C )
19 17 18 eqtr4di 
 |-  ( x = ( G |` C ) -> ran x = ( G " C ) )
20 19 unieqd 
 |-  ( x = ( G |` C ) -> U. ran x = U. ( G " C ) )
21 20 rneqd 
 |-  ( x = ( G |` C ) -> ran U. ran x = ran U. ( G " C ) )
22 21 unieqd 
 |-  ( x = ( G |` C ) -> U. ran U. ran x = U. ran U. ( G " C ) )
23 suceq 
 |-  ( U. ran U. ran x = U. ran U. ( G " C ) -> suc U. ran U. ran x = suc U. ran U. ( G " C ) )
24 22 23 syl 
 |-  ( x = ( G |` C ) -> suc U. ran U. ran x = suc U. ran U. ( G " C ) )
25 24 oveq1d 
 |-  ( x = ( G |` C ) -> ( suc U. ran U. ran x .o ( rank ` y ) ) = ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) )
26 fveq1 
 |-  ( x = ( G |` C ) -> ( x ` suc ( rank ` y ) ) = ( ( G |` C ) ` suc ( rank ` y ) ) )
27 26 fveq1d 
 |-  ( x = ( G |` C ) -> ( ( x ` suc ( rank ` y ) ) ` y ) = ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) )
28 25 27 oveq12d 
 |-  ( x = ( G |` C ) -> ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) )
29 id 
 |-  ( x = ( G |` C ) -> x = ( G |` C ) )
30 29 15 fveq12d 
 |-  ( x = ( G |` C ) -> ( x ` U. dom x ) = ( ( G |` C ) ` U. dom ( G |` C ) ) )
31 30 rneqd 
 |-  ( x = ( G |` C ) -> ran ( x ` U. dom x ) = ran ( ( G |` C ) ` U. dom ( G |` C ) ) )
32 oieq2 
 |-  ( ran ( x ` U. dom x ) = ran ( ( G |` C ) ` U. dom ( G |` C ) ) -> OrdIso ( _E , ran ( x ` U. dom x ) ) = OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) )
33 31 32 syl 
 |-  ( x = ( G |` C ) -> OrdIso ( _E , ran ( x ` U. dom x ) ) = OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) )
34 33 cnveqd 
 |-  ( x = ( G |` C ) -> `' OrdIso ( _E , ran ( x ` U. dom x ) ) = `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) )
35 34 30 coeq12d 
 |-  ( x = ( G |` C ) -> ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) = ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) )
36 35 imaeq1d 
 |-  ( x = ( G |` C ) -> ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) = ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) )
37 36 fveq2d 
 |-  ( x = ( G |` C ) -> ( F ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) = ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) )
38 16 28 37 ifbieq12d 
 |-  ( x = ( G |` C ) -> 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 ) ) ) = if ( dom ( G |` C ) = U. dom ( G |` C ) , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) )
39 14 38 mpteq12dv 
 |-  ( x = ( G |` C ) -> ( 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 ) ) ) ) = ( y e. ( R1 ` dom ( G |` C ) ) |-> if ( dom ( G |` C ) = U. dom ( G |` C ) , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) ) )
40 eqid 
 |-  ( 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 ) ) ) ) ) = ( 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 ) ) ) ) )
41 fvex 
 |-  ( R1 ` dom ( G |` C ) ) e. _V
42 41 mptex 
 |-  ( y e. ( R1 ` dom ( G |` C ) ) |-> if ( dom ( G |` C ) = U. dom ( G |` C ) , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) ) e. _V
43 39 40 42 fvmpt 
 |-  ( ( G |` C ) e. _V -> ( ( 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 ) ) ) ) ) ` ( G |` C ) ) = ( y e. ( R1 ` dom ( G |` C ) ) |-> if ( dom ( G |` C ) = U. dom ( G |` C ) , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) ) )
44 12 43 syl 
 |-  ( ph -> ( ( 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 ) ) ) ) ) ` ( G |` C ) ) = ( y e. ( R1 ` dom ( G |` C ) ) |-> if ( dom ( G |` C ) = U. dom ( G |` C ) , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) ) )
45 onss 
 |-  ( C e. On -> C C_ On )
46 4 45 syl 
 |-  ( ph -> C C_ On )
47 fnssres 
 |-  ( ( G Fn On /\ C C_ On ) -> ( G |` C ) Fn C )
48 8 46 47 sylancr 
 |-  ( ph -> ( G |` C ) Fn C )
49 48 fndmd 
 |-  ( ph -> dom ( G |` C ) = C )
50 49 fveq2d 
 |-  ( ph -> ( R1 ` dom ( G |` C ) ) = ( R1 ` C ) )
51 50 mpteq1d 
 |-  ( ph -> ( y e. ( R1 ` dom ( G |` C ) ) |-> if ( dom ( G |` C ) = U. dom ( G |` C ) , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) ) = ( y e. ( R1 ` C ) |-> if ( dom ( G |` C ) = U. dom ( G |` C ) , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) ) )
52 49 adantr 
 |-  ( ( ph /\ y e. ( R1 ` C ) ) -> dom ( G |` C ) = C )
53 52 unieqd 
 |-  ( ( ph /\ y e. ( R1 ` C ) ) -> U. dom ( G |` C ) = U. C )
54 52 53 eqeq12d 
 |-  ( ( ph /\ y e. ( R1 ` C ) ) -> ( dom ( G |` C ) = U. dom ( G |` C ) <-> C = U. C ) )
55 54 ifbid 
 |-  ( ( ph /\ y e. ( R1 ` C ) ) -> if ( dom ( G |` C ) = U. dom ( G |` C ) , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) )
56 rankr1ai 
 |-  ( y e. ( R1 ` C ) -> ( rank ` y ) e. C )
57 56 ad2antlr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( rank ` y ) e. C )
58 simpr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> C = U. C )
59 57 58 eleqtrd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( rank ` y ) e. U. C )
60 eloni 
 |-  ( C e. On -> Ord C )
61 ordsucuniel 
 |-  ( Ord C -> ( ( rank ` y ) e. U. C <-> suc ( rank ` y ) e. C ) )
62 4 60 61 3syl 
 |-  ( ph -> ( ( rank ` y ) e. U. C <-> suc ( rank ` y ) e. C ) )
63 62 ad2antrr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( rank ` y ) e. U. C <-> suc ( rank ` y ) e. C ) )
64 59 63 mpbid 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> suc ( rank ` y ) e. C )
65 64 fvresd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G |` C ) ` suc ( rank ` y ) ) = ( G ` suc ( rank ` y ) ) )
66 65 fveq1d 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` y ) ) ` y ) )
67 66 oveq2d 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) )
68 67 ifeq1da 
 |-  ( ( ph /\ y e. ( R1 ` C ) ) -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) )
69 53 adantr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> U. dom ( G |` C ) = U. C )
70 69 fveq2d 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( ( G |` C ) ` U. dom ( G |` C ) ) = ( ( G |` C ) ` U. C ) )
71 4 ad2antrr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> C e. On )
72 uniexg 
 |-  ( C e. On -> U. C e. _V )
73 sucidg 
 |-  ( U. C e. _V -> U. C e. suc U. C )
74 71 72 73 3syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> U. C e. suc U. C )
75 4 adantr 
 |-  ( ( ph /\ y e. ( R1 ` C ) ) -> C e. On )
76 orduniorsuc 
 |-  ( Ord C -> ( C = U. C \/ C = suc U. C ) )
77 75 60 76 3syl 
 |-  ( ( ph /\ y e. ( R1 ` C ) ) -> ( C = U. C \/ C = suc U. C ) )
78 77 orcanai 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> C = suc U. C )
79 74 78 eleqtrrd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> U. C e. C )
80 79 fvresd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( ( G |` C ) ` U. C ) = ( G ` U. C ) )
81 70 80 eqtrd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( ( G |` C ) ` U. dom ( G |` C ) ) = ( G ` U. C ) )
82 81 rneqd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ran ( ( G |` C ) ` U. dom ( G |` C ) ) = ran ( G ` U. C ) )
83 oieq2 
 |-  ( ran ( ( G |` C ) ` U. dom ( G |` C ) ) = ran ( G ` U. C ) -> OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) = OrdIso ( _E , ran ( G ` U. C ) ) )
84 82 83 syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) = OrdIso ( _E , ran ( G ` U. C ) ) )
85 84 cnveqd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) = `' OrdIso ( _E , ran ( G ` U. C ) ) )
86 85 81 coeq12d 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) = ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) ) )
87 86 5 eqtr4di 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) = H )
88 87 imaeq1d 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) = ( H " y ) )
89 88 fveq2d 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) = ( F ` ( H " y ) ) )
90 89 ifeq2da 
 |-  ( ( ph /\ y e. ( R1 ` C ) ) -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) )
91 55 68 90 3eqtrd 
 |-  ( ( ph /\ y e. ( R1 ` C ) ) -> if ( dom ( G |` C ) = U. dom ( G |` C ) , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) )
92 91 mpteq2dva 
 |-  ( ph -> ( y e. ( R1 ` C ) |-> if ( dom ( G |` C ) = U. dom ( G |` C ) , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) ) = ( y e. ( R1 ` C ) |-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) )
93 51 92 eqtrd 
 |-  ( ph -> ( y e. ( R1 ` dom ( G |` C ) ) |-> if ( dom ( G |` C ) = U. dom ( G |` C ) , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( ( G |` C ) ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( ( G |` C ) ` U. dom ( G |` C ) ) ) o. ( ( G |` C ) ` U. dom ( G |` C ) ) ) " y ) ) ) ) = ( y e. ( R1 ` C ) |-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) )
94 7 44 93 3eqtrd 
 |-  ( ph -> ( G ` C ) = ( y e. ( R1 ` C ) |-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) )