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