Metamath Proof Explorer


Theorem dfac12lem2

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

Ref Expression
Hypotheses dfac12.1 ( 𝜑𝐴 ∈ On )
dfac12.3 ( 𝜑𝐹 : 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) –1-1→ On )
dfac12.4 𝐺 = recs ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = dom 𝑥 , ( ( suc ran ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( OrdIso ( E , ran ( 𝑥 dom 𝑥 ) ) ∘ ( 𝑥 dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) )
dfac12.5 ( 𝜑𝐶 ∈ On )
dfac12.h 𝐻 = ( OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∘ ( 𝐺 𝐶 ) )
dfac12.6 ( 𝜑𝐶𝐴 )
dfac12.8 ( 𝜑 → ∀ 𝑧𝐶 ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) –1-1→ On )
Assertion dfac12lem2 ( 𝜑 → ( 𝐺𝐶 ) : ( 𝑅1𝐶 ) –1-1→ On )

Proof

Step Hyp Ref Expression
1 dfac12.1 ( 𝜑𝐴 ∈ On )
2 dfac12.3 ( 𝜑𝐹 : 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) –1-1→ On )
3 dfac12.4 𝐺 = recs ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = dom 𝑥 , ( ( suc ran ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( OrdIso ( E , ran ( 𝑥 dom 𝑥 ) ) ∘ ( 𝑥 dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) )
4 dfac12.5 ( 𝜑𝐶 ∈ On )
5 dfac12.h 𝐻 = ( OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∘ ( 𝐺 𝐶 ) )
6 dfac12.6 ( 𝜑𝐶𝐴 )
7 dfac12.8 ( 𝜑 → ∀ 𝑧𝐶 ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) –1-1→ On )
8 3 tfr1 𝐺 Fn On
9 fnfun ( 𝐺 Fn On → Fun 𝐺 )
10 8 9 ax-mp Fun 𝐺
11 funimaexg ( ( Fun 𝐺𝐶 ∈ On ) → ( 𝐺𝐶 ) ∈ V )
12 10 4 11 sylancr ( 𝜑 → ( 𝐺𝐶 ) ∈ V )
13 uniexg ( ( 𝐺𝐶 ) ∈ V → ( 𝐺𝐶 ) ∈ V )
14 rnexg ( ( 𝐺𝐶 ) ∈ V → ran ( 𝐺𝐶 ) ∈ V )
15 12 13 14 3syl ( 𝜑 → ran ( 𝐺𝐶 ) ∈ V )
16 f1f ( ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) –1-1→ On → ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) ⟶ On )
17 fssxp ( ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) ⟶ On → ( 𝐺𝑧 ) ⊆ ( ( 𝑅1𝑧 ) × On ) )
18 ssv ( 𝑅1𝑧 ) ⊆ V
19 xpss1 ( ( 𝑅1𝑧 ) ⊆ V → ( ( 𝑅1𝑧 ) × On ) ⊆ ( V × On ) )
20 18 19 ax-mp ( ( 𝑅1𝑧 ) × On ) ⊆ ( V × On )
21 sstr ( ( ( 𝐺𝑧 ) ⊆ ( ( 𝑅1𝑧 ) × On ) ∧ ( ( 𝑅1𝑧 ) × On ) ⊆ ( V × On ) ) → ( 𝐺𝑧 ) ⊆ ( V × On ) )
22 20 21 mpan2 ( ( 𝐺𝑧 ) ⊆ ( ( 𝑅1𝑧 ) × On ) → ( 𝐺𝑧 ) ⊆ ( V × On ) )
23 fvex ( 𝐺𝑧 ) ∈ V
24 23 elpw ( ( 𝐺𝑧 ) ∈ 𝒫 ( V × On ) ↔ ( 𝐺𝑧 ) ⊆ ( V × On ) )
25 22 24 sylibr ( ( 𝐺𝑧 ) ⊆ ( ( 𝑅1𝑧 ) × On ) → ( 𝐺𝑧 ) ∈ 𝒫 ( V × On ) )
26 16 17 25 3syl ( ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) –1-1→ On → ( 𝐺𝑧 ) ∈ 𝒫 ( V × On ) )
27 26 ralimi ( ∀ 𝑧𝐶 ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) –1-1→ On → ∀ 𝑧𝐶 ( 𝐺𝑧 ) ∈ 𝒫 ( V × On ) )
28 7 27 syl ( 𝜑 → ∀ 𝑧𝐶 ( 𝐺𝑧 ) ∈ 𝒫 ( V × On ) )
29 onss ( 𝐶 ∈ On → 𝐶 ⊆ On )
30 4 29 syl ( 𝜑𝐶 ⊆ On )
31 8 fndmi dom 𝐺 = On
32 30 31 sseqtrrdi ( 𝜑𝐶 ⊆ dom 𝐺 )
33 funimass4 ( ( Fun 𝐺𝐶 ⊆ dom 𝐺 ) → ( ( 𝐺𝐶 ) ⊆ 𝒫 ( V × On ) ↔ ∀ 𝑧𝐶 ( 𝐺𝑧 ) ∈ 𝒫 ( V × On ) ) )
34 10 32 33 sylancr ( 𝜑 → ( ( 𝐺𝐶 ) ⊆ 𝒫 ( V × On ) ↔ ∀ 𝑧𝐶 ( 𝐺𝑧 ) ∈ 𝒫 ( V × On ) ) )
35 28 34 mpbird ( 𝜑 → ( 𝐺𝐶 ) ⊆ 𝒫 ( V × On ) )
36 sspwuni ( ( 𝐺𝐶 ) ⊆ 𝒫 ( V × On ) ↔ ( 𝐺𝐶 ) ⊆ ( V × On ) )
37 35 36 sylib ( 𝜑 ( 𝐺𝐶 ) ⊆ ( V × On ) )
38 rnss ( ( 𝐺𝐶 ) ⊆ ( V × On ) → ran ( 𝐺𝐶 ) ⊆ ran ( V × On ) )
39 37 38 syl ( 𝜑 → ran ( 𝐺𝐶 ) ⊆ ran ( V × On ) )
40 rnxpss ran ( V × On ) ⊆ On
41 39 40 sstrdi ( 𝜑 → ran ( 𝐺𝐶 ) ⊆ On )
42 ssonuni ( ran ( 𝐺𝐶 ) ∈ V → ( ran ( 𝐺𝐶 ) ⊆ On → ran ( 𝐺𝐶 ) ∈ On ) )
43 15 41 42 sylc ( 𝜑 ran ( 𝐺𝐶 ) ∈ On )
44 suceloni ( ran ( 𝐺𝐶 ) ∈ On → suc ran ( 𝐺𝐶 ) ∈ On )
45 43 44 syl ( 𝜑 → suc ran ( 𝐺𝐶 ) ∈ On )
46 45 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → suc ran ( 𝐺𝐶 ) ∈ On )
47 rankon ( rank ‘ 𝑦 ) ∈ On
48 omcl ( ( suc ran ( 𝐺𝐶 ) ∈ On ∧ ( rank ‘ 𝑦 ) ∈ On ) → ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) ∈ On )
49 46 47 48 sylancl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) ∈ On )
50 fveq2 ( 𝑧 = suc ( rank ‘ 𝑦 ) → ( 𝐺𝑧 ) = ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) )
51 f1eq1 ( ( 𝐺𝑧 ) = ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) → ( ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1𝑧 ) –1-1→ On ) )
52 50 51 syl ( 𝑧 = suc ( rank ‘ 𝑦 ) → ( ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1𝑧 ) –1-1→ On ) )
53 fveq2 ( 𝑧 = suc ( rank ‘ 𝑦 ) → ( 𝑅1𝑧 ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
54 f1eq2 ( ( 𝑅1𝑧 ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On ) )
55 53 54 syl ( 𝑧 = suc ( rank ‘ 𝑦 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On ) )
56 52 55 bitrd ( 𝑧 = suc ( rank ‘ 𝑦 ) → ( ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On ) )
57 7 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ∀ 𝑧𝐶 ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) –1-1→ On )
58 rankr1ai ( 𝑦 ∈ ( 𝑅1𝐶 ) → ( rank ‘ 𝑦 ) ∈ 𝐶 )
59 58 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( rank ‘ 𝑦 ) ∈ 𝐶 )
60 simpr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → 𝐶 = 𝐶 )
61 59 60 eleqtrd ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( rank ‘ 𝑦 ) ∈ 𝐶 )
62 eloni ( 𝐶 ∈ On → Ord 𝐶 )
63 4 62 syl ( 𝜑 → Ord 𝐶 )
64 63 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → Ord 𝐶 )
65 ordsucuniel ( Ord 𝐶 → ( ( rank ‘ 𝑦 ) ∈ 𝐶 ↔ suc ( rank ‘ 𝑦 ) ∈ 𝐶 ) )
66 64 65 syl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( ( rank ‘ 𝑦 ) ∈ 𝐶 ↔ suc ( rank ‘ 𝑦 ) ∈ 𝐶 ) )
67 61 66 mpbid ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → suc ( rank ‘ 𝑦 ) ∈ 𝐶 )
68 56 57 67 rspcdva ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On )
69 f1f ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ⟶ On )
70 68 69 syl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ⟶ On )
71 r1elwf ( 𝑦 ∈ ( 𝑅1𝐶 ) → 𝑦 ( 𝑅1 “ On ) )
72 71 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → 𝑦 ( 𝑅1 “ On ) )
73 rankidb ( 𝑦 ( 𝑅1 “ On ) → 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
74 72 73 syl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
75 70 74 ffvelrnd ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ On )
76 oacl ( ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) ∈ On ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ On ) → ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) ∈ On )
77 49 75 76 syl2anc ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) ∈ On )
78 f1f ( 𝐹 : 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) –1-1→ On → 𝐹 : 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) ⟶ On )
79 2 78 syl ( 𝜑𝐹 : 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) ⟶ On )
80 79 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝐹 : 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) ⟶ On )
81 imassrn ( 𝐻𝑦 ) ⊆ ran 𝐻
82 fvex ( 𝐺 𝐶 ) ∈ V
83 82 rnex ran ( 𝐺 𝐶 ) ∈ V
84 fveq2 ( 𝑧 = 𝐶 → ( 𝐺𝑧 ) = ( 𝐺 𝐶 ) )
85 f1eq1 ( ( 𝐺𝑧 ) = ( 𝐺 𝐶 ) → ( ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) –1-1→ On ↔ ( 𝐺 𝐶 ) : ( 𝑅1𝑧 ) –1-1→ On ) )
86 84 85 syl ( 𝑧 = 𝐶 → ( ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) –1-1→ On ↔ ( 𝐺 𝐶 ) : ( 𝑅1𝑧 ) –1-1→ On ) )
87 fveq2 ( 𝑧 = 𝐶 → ( 𝑅1𝑧 ) = ( 𝑅1 𝐶 ) )
88 f1eq2 ( ( 𝑅1𝑧 ) = ( 𝑅1 𝐶 ) → ( ( 𝐺 𝐶 ) : ( 𝑅1𝑧 ) –1-1→ On ↔ ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) –1-1→ On ) )
89 87 88 syl ( 𝑧 = 𝐶 → ( ( 𝐺 𝐶 ) : ( 𝑅1𝑧 ) –1-1→ On ↔ ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) –1-1→ On ) )
90 86 89 bitrd ( 𝑧 = 𝐶 → ( ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) –1-1→ On ↔ ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) –1-1→ On ) )
91 7 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ∀ 𝑧𝐶 ( 𝐺𝑧 ) : ( 𝑅1𝑧 ) –1-1→ On )
92 4 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝐶 ∈ On )
93 onuni ( 𝐶 ∈ On → 𝐶 ∈ On )
94 sucidg ( 𝐶 ∈ On → 𝐶 ∈ suc 𝐶 )
95 92 93 94 3syl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝐶 ∈ suc 𝐶 )
96 63 adantr ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) → Ord 𝐶 )
97 orduniorsuc ( Ord 𝐶 → ( 𝐶 = 𝐶𝐶 = suc 𝐶 ) )
98 96 97 syl ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) → ( 𝐶 = 𝐶𝐶 = suc 𝐶 ) )
99 98 orcanai ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝐶 = suc 𝐶 )
100 95 99 eleqtrrd ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝐶𝐶 )
101 90 91 100 rspcdva ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) –1-1→ On )
102 f1f ( ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) –1-1→ On → ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) ⟶ On )
103 frn ( ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) ⟶ On → ran ( 𝐺 𝐶 ) ⊆ On )
104 101 102 103 3syl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ran ( 𝐺 𝐶 ) ⊆ On )
105 epweon E We On
106 wess ( ran ( 𝐺 𝐶 ) ⊆ On → ( E We On → E We ran ( 𝐺 𝐶 ) ) )
107 104 105 106 mpisyl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → E We ran ( 𝐺 𝐶 ) )
108 eqid OrdIso ( E , ran ( 𝐺 𝐶 ) ) = OrdIso ( E , ran ( 𝐺 𝐶 ) )
109 108 oiiso ( ( ran ( 𝐺 𝐶 ) ∈ V ∧ E We ran ( 𝐺 𝐶 ) ) → OrdIso ( E , ran ( 𝐺 𝐶 ) ) Isom E , E ( dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) , ran ( 𝐺 𝐶 ) ) )
110 83 107 109 sylancr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → OrdIso ( E , ran ( 𝐺 𝐶 ) ) Isom E , E ( dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) , ran ( 𝐺 𝐶 ) ) )
111 isof1o ( OrdIso ( E , ran ( 𝐺 𝐶 ) ) Isom E , E ( dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) , ran ( 𝐺 𝐶 ) ) → OrdIso ( E , ran ( 𝐺 𝐶 ) ) : dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) –1-1-onto→ ran ( 𝐺 𝐶 ) )
112 f1ocnv ( OrdIso ( E , ran ( 𝐺 𝐶 ) ) : dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) –1-1-onto→ ran ( 𝐺 𝐶 ) → OrdIso ( E , ran ( 𝐺 𝐶 ) ) : ran ( 𝐺 𝐶 ) –1-1-onto→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) )
113 f1of1 ( OrdIso ( E , ran ( 𝐺 𝐶 ) ) : ran ( 𝐺 𝐶 ) –1-1-onto→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) → OrdIso ( E , ran ( 𝐺 𝐶 ) ) : ran ( 𝐺 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) )
114 110 111 112 113 4syl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → OrdIso ( E , ran ( 𝐺 𝐶 ) ) : ran ( 𝐺 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) )
115 f1f1orn ( ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) –1-1→ On → ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) –1-1-onto→ ran ( 𝐺 𝐶 ) )
116 f1of1 ( ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) –1-1-onto→ ran ( 𝐺 𝐶 ) → ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) –1-1→ ran ( 𝐺 𝐶 ) )
117 101 115 116 3syl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) –1-1→ ran ( 𝐺 𝐶 ) )
118 f1co ( ( OrdIso ( E , ran ( 𝐺 𝐶 ) ) : ran ( 𝐺 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∧ ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) –1-1→ ran ( 𝐺 𝐶 ) ) → ( OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∘ ( 𝐺 𝐶 ) ) : ( 𝑅1 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) )
119 114 117 118 syl2anc ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∘ ( 𝐺 𝐶 ) ) : ( 𝑅1 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) )
120 f1eq1 ( 𝐻 = ( OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∘ ( 𝐺 𝐶 ) ) → ( 𝐻 : ( 𝑅1 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ↔ ( OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∘ ( 𝐺 𝐶 ) ) : ( 𝑅1 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ) )
121 5 120 ax-mp ( 𝐻 : ( 𝑅1 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ↔ ( OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∘ ( 𝐺 𝐶 ) ) : ( 𝑅1 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) )
122 119 121 sylibr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝐻 : ( 𝑅1 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) )
123 f1f ( 𝐻 : ( 𝑅1 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) → 𝐻 : ( 𝑅1 𝐶 ) ⟶ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) )
124 frn ( 𝐻 : ( 𝑅1 𝐶 ) ⟶ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) → ran 𝐻 ⊆ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) )
125 122 123 124 3syl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ran 𝐻 ⊆ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) )
126 harcl ( har ‘ ( 𝑅1𝐴 ) ) ∈ On
127 126 onordi Ord ( har ‘ ( 𝑅1𝐴 ) )
128 108 oion ( ran ( 𝐺 𝐶 ) ∈ V → dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∈ On )
129 83 128 mp1i ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∈ On )
130 108 oien ( ( ran ( 𝐺 𝐶 ) ∈ V ∧ E We ran ( 𝐺 𝐶 ) ) → dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ≈ ran ( 𝐺 𝐶 ) )
131 83 107 130 sylancr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ≈ ran ( 𝐺 𝐶 ) )
132 fvex ( 𝑅1 𝐶 ) ∈ V
133 132 f1oen ( ( 𝐺 𝐶 ) : ( 𝑅1 𝐶 ) –1-1-onto→ ran ( 𝐺 𝐶 ) → ( 𝑅1 𝐶 ) ≈ ran ( 𝐺 𝐶 ) )
134 ensym ( ( 𝑅1 𝐶 ) ≈ ran ( 𝐺 𝐶 ) → ran ( 𝐺 𝐶 ) ≈ ( 𝑅1 𝐶 ) )
135 101 115 133 134 4syl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ran ( 𝐺 𝐶 ) ≈ ( 𝑅1 𝐶 ) )
136 fvex ( 𝑅1𝐴 ) ∈ V
137 1 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝐴 ∈ On )
138 6 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝐶𝐴 )
139 138 100 sseldd ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝐶𝐴 )
140 r1ord2 ( 𝐴 ∈ On → ( 𝐶𝐴 → ( 𝑅1 𝐶 ) ⊆ ( 𝑅1𝐴 ) ) )
141 137 139 140 sylc ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝑅1 𝐶 ) ⊆ ( 𝑅1𝐴 ) )
142 ssdomg ( ( 𝑅1𝐴 ) ∈ V → ( ( 𝑅1 𝐶 ) ⊆ ( 𝑅1𝐴 ) → ( 𝑅1 𝐶 ) ≼ ( 𝑅1𝐴 ) ) )
143 136 141 142 mpsyl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝑅1 𝐶 ) ≼ ( 𝑅1𝐴 ) )
144 endomtr ( ( ran ( 𝐺 𝐶 ) ≈ ( 𝑅1 𝐶 ) ∧ ( 𝑅1 𝐶 ) ≼ ( 𝑅1𝐴 ) ) → ran ( 𝐺 𝐶 ) ≼ ( 𝑅1𝐴 ) )
145 135 143 144 syl2anc ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ran ( 𝐺 𝐶 ) ≼ ( 𝑅1𝐴 ) )
146 endomtr ( ( dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ≈ ran ( 𝐺 𝐶 ) ∧ ran ( 𝐺 𝐶 ) ≼ ( 𝑅1𝐴 ) ) → dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ≼ ( 𝑅1𝐴 ) )
147 131 145 146 syl2anc ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ≼ ( 𝑅1𝐴 ) )
148 elharval ( dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∈ ( har ‘ ( 𝑅1𝐴 ) ) ↔ ( dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∈ On ∧ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ≼ ( 𝑅1𝐴 ) ) )
149 129 147 148 sylanbrc ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∈ ( har ‘ ( 𝑅1𝐴 ) ) )
150 ordelss ( ( Ord ( har ‘ ( 𝑅1𝐴 ) ) ∧ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∈ ( har ‘ ( 𝑅1𝐴 ) ) ) → dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ⊆ ( har ‘ ( 𝑅1𝐴 ) ) )
151 127 149 150 sylancr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ⊆ ( har ‘ ( 𝑅1𝐴 ) ) )
152 125 151 sstrd ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ran 𝐻 ⊆ ( har ‘ ( 𝑅1𝐴 ) ) )
153 81 152 sstrid ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝐻𝑦 ) ⊆ ( har ‘ ( 𝑅1𝐴 ) ) )
154 fvex ( har ‘ ( 𝑅1𝐴 ) ) ∈ V
155 154 elpw2 ( ( 𝐻𝑦 ) ∈ 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) ↔ ( 𝐻𝑦 ) ⊆ ( har ‘ ( 𝑅1𝐴 ) ) )
156 153 155 sylibr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝐻𝑦 ) ∈ 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) )
157 80 156 ffvelrnd ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝐹 ‘ ( 𝐻𝑦 ) ) ∈ On )
158 77 157 ifclda ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) → if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) ∈ On )
159 158 ex ( 𝜑 → ( 𝑦 ∈ ( 𝑅1𝐶 ) → if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) ∈ On ) )
160 iftrue ( 𝐶 = 𝐶 → if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) = ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) )
161 iftrue ( 𝐶 = 𝐶 → if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻𝑧 ) ) ) = ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) )
162 160 161 eqeq12d ( 𝐶 = 𝐶 → ( if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) = if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻𝑧 ) ) ) ↔ ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) = ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ) )
163 162 adantl ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) → ( if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) = if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻𝑧 ) ) ) ↔ ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) = ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ) )
164 45 ad2antrr ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) → suc ran ( 𝐺𝐶 ) ∈ On )
165 nsuceq0 suc ran ( 𝐺𝐶 ) ≠ ∅
166 165 a1i ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) → suc ran ( 𝐺𝐶 ) ≠ ∅ )
167 47 a1i ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) → ( rank ‘ 𝑦 ) ∈ On )
168 onsucuni ( ran ( 𝐺𝐶 ) ⊆ On → ran ( 𝐺𝐶 ) ⊆ suc ran ( 𝐺𝐶 ) )
169 41 168 syl ( 𝜑 → ran ( 𝐺𝐶 ) ⊆ suc ran ( 𝐺𝐶 ) )
170 169 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ran ( 𝐺𝐶 ) ⊆ suc ran ( 𝐺𝐶 ) )
171 30 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → 𝐶 ⊆ On )
172 fnfvima ( ( 𝐺 Fn On ∧ 𝐶 ⊆ On ∧ suc ( rank ‘ 𝑦 ) ∈ 𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ∈ ( 𝐺𝐶 ) )
173 8 171 67 172 mp3an2i ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ∈ ( 𝐺𝐶 ) )
174 elssuni ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ∈ ( 𝐺𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ⊆ ( 𝐺𝐶 ) )
175 rnss ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ⊆ ( 𝐺𝐶 ) → ran ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ⊆ ran ( 𝐺𝐶 ) )
176 173 174 175 3syl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ran ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ⊆ ran ( 𝐺𝐶 ) )
177 f1fn ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) Fn ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
178 68 177 syl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) Fn ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
179 fnfvelrn ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) Fn ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ ran ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) )
180 178 74 179 syl2anc ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ ran ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) )
181 176 180 sseldd ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ ran ( 𝐺𝐶 ) )
182 170 181 sseldd ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ suc ran ( 𝐺𝐶 ) )
183 182 adantlrr ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ suc ran ( 𝐺𝐶 ) )
184 rankon ( rank ‘ 𝑧 ) ∈ On
185 184 a1i ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) → ( rank ‘ 𝑧 ) ∈ On )
186 eleq1w ( 𝑦 = 𝑧 → ( 𝑦 ∈ ( 𝑅1𝐶 ) ↔ 𝑧 ∈ ( 𝑅1𝐶 ) ) )
187 186 anbi2d ( 𝑦 = 𝑧 → ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ↔ ( 𝜑𝑧 ∈ ( 𝑅1𝐶 ) ) ) )
188 187 anbi1d ( 𝑦 = 𝑧 → ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) ↔ ( ( 𝜑𝑧 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) ) )
189 fveq2 ( 𝑦 = 𝑧 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) )
190 suceq ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) → suc ( rank ‘ 𝑦 ) = suc ( rank ‘ 𝑧 ) )
191 189 190 syl ( 𝑦 = 𝑧 → suc ( rank ‘ 𝑦 ) = suc ( rank ‘ 𝑧 ) )
192 191 fveq2d ( 𝑦 = 𝑧 → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) = ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) )
193 id ( 𝑦 = 𝑧𝑦 = 𝑧 )
194 192 193 fveq12d ( 𝑦 = 𝑧 → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) )
195 194 eleq1d ( 𝑦 = 𝑧 → ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ suc ran ( 𝐺𝐶 ) ↔ ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ suc ran ( 𝐺𝐶 ) ) )
196 188 195 imbi12d ( 𝑦 = 𝑧 → ( ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ suc ran ( 𝐺𝐶 ) ) ↔ ( ( ( 𝜑𝑧 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ suc ran ( 𝐺𝐶 ) ) ) )
197 196 182 chvarvv ( ( ( 𝜑𝑧 ∈ ( 𝑅1𝐶 ) ) ∧ 𝐶 = 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ suc ran ( 𝐺𝐶 ) )
198 197 adantlrl ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ suc ran ( 𝐺𝐶 ) )
199 omopth2 ( ( ( suc ran ( 𝐺𝐶 ) ∈ On ∧ suc ran ( 𝐺𝐶 ) ≠ ∅ ) ∧ ( ( rank ‘ 𝑦 ) ∈ On ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ suc ran ( 𝐺𝐶 ) ) ∧ ( ( rank ‘ 𝑧 ) ∈ On ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ suc ran ( 𝐺𝐶 ) ) ) → ( ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) = ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ↔ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ) )
200 164 166 167 183 185 198 199 syl222anc ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) → ( ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) = ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ↔ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ) )
201 190 adantl ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → suc ( rank ‘ 𝑦 ) = suc ( rank ‘ 𝑧 ) )
202 201 fveq2d ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) = ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) )
203 202 fveq1d ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑧 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) )
204 203 eqeq2d ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑧 ) ↔ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) )
205 68 adantlrr ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On )
206 205 adantr ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On )
207 74 adantlrr ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) → 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
208 207 adantr ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
209 r1elwf ( 𝑧 ∈ ( 𝑅1𝐶 ) → 𝑧 ( 𝑅1 “ On ) )
210 rankidb ( 𝑧 ( 𝑅1 “ On ) → 𝑧 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑧 ) ) )
211 209 210 syl ( 𝑧 ∈ ( 𝑅1𝐶 ) → 𝑧 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑧 ) ) )
212 211 ad2antll ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) → 𝑧 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑧 ) ) )
213 212 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → 𝑧 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑧 ) ) )
214 201 fveq2d ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑧 ) ) )
215 213 214 eleqtrrd ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → 𝑧 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
216 f1fveq ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On ∧ ( 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ∧ 𝑧 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) ) → ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑧 ) ↔ 𝑦 = 𝑧 ) )
217 206 208 215 216 syl12anc ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑧 ) ↔ 𝑦 = 𝑧 ) )
218 204 217 bitr3d ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ↔ 𝑦 = 𝑧 ) )
219 218 biimpd ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
220 219 expimpd ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) → ( ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) → 𝑦 = 𝑧 ) )
221 189 194 jca ( 𝑦 = 𝑧 → ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) )
222 220 221 impbid1 ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) → ( ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ↔ 𝑦 = 𝑧 ) )
223 163 200 222 3bitrd ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ 𝐶 = 𝐶 ) → ( if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) = if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻𝑧 ) ) ) ↔ 𝑦 = 𝑧 ) )
224 iffalse ( ¬ 𝐶 = 𝐶 → if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) = ( 𝐹 ‘ ( 𝐻𝑦 ) ) )
225 iffalse ( ¬ 𝐶 = 𝐶 → if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻𝑧 ) ) ) = ( 𝐹 ‘ ( 𝐻𝑧 ) ) )
226 224 225 eqeq12d ( ¬ 𝐶 = 𝐶 → ( if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) = if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻𝑧 ) ) ) ↔ ( 𝐹 ‘ ( 𝐻𝑦 ) ) = ( 𝐹 ‘ ( 𝐻𝑧 ) ) ) )
227 226 adantl ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) = if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻𝑧 ) ) ) ↔ ( 𝐹 ‘ ( 𝐻𝑦 ) ) = ( 𝐹 ‘ ( 𝐻𝑧 ) ) ) )
228 2 ad2antrr ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝐹 : 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) –1-1→ On )
229 156 adantlrr ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝐻𝑦 ) ∈ 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) )
230 187 anbi1d ( 𝑦 = 𝑧 → ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) ↔ ( ( 𝜑𝑧 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) ) )
231 imaeq2 ( 𝑦 = 𝑧 → ( 𝐻𝑦 ) = ( 𝐻𝑧 ) )
232 231 eleq1d ( 𝑦 = 𝑧 → ( ( 𝐻𝑦 ) ∈ 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) ↔ ( 𝐻𝑧 ) ∈ 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) ) )
233 230 232 imbi12d ( 𝑦 = 𝑧 → ( ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝐻𝑦 ) ∈ 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) ) ↔ ( ( ( 𝜑𝑧 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝐻𝑧 ) ∈ 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) ) ) )
234 233 156 chvarvv ( ( ( 𝜑𝑧 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝐻𝑧 ) ∈ 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) )
235 234 adantlrl ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝐻𝑧 ) ∈ 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) )
236 f1fveq ( ( 𝐹 : 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) –1-1→ On ∧ ( ( 𝐻𝑦 ) ∈ 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) ∧ ( 𝐻𝑧 ) ∈ 𝒫 ( har ‘ ( 𝑅1𝐴 ) ) ) ) → ( ( 𝐹 ‘ ( 𝐻𝑦 ) ) = ( 𝐹 ‘ ( 𝐻𝑧 ) ) ↔ ( 𝐻𝑦 ) = ( 𝐻𝑧 ) ) )
237 228 229 235 236 syl12anc ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( ( 𝐹 ‘ ( 𝐻𝑦 ) ) = ( 𝐹 ‘ ( 𝐻𝑧 ) ) ↔ ( 𝐻𝑦 ) = ( 𝐻𝑧 ) ) )
238 122 adantlrr ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝐻 : ( 𝑅1 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) )
239 simplrl ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝑦 ∈ ( 𝑅1𝐶 ) )
240 99 fveq2d ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝑅1𝐶 ) = ( 𝑅1 ‘ suc 𝐶 ) )
241 r1suc ( 𝐶 ∈ On → ( 𝑅1 ‘ suc 𝐶 ) = 𝒫 ( 𝑅1 𝐶 ) )
242 92 93 241 3syl ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝑅1 ‘ suc 𝐶 ) = 𝒫 ( 𝑅1 𝐶 ) )
243 240 242 eqtrd ( ( ( 𝜑𝑦 ∈ ( 𝑅1𝐶 ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝑅1𝐶 ) = 𝒫 ( 𝑅1 𝐶 ) )
244 243 adantlrr ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( 𝑅1𝐶 ) = 𝒫 ( 𝑅1 𝐶 ) )
245 239 244 eleqtrd ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝑦 ∈ 𝒫 ( 𝑅1 𝐶 ) )
246 245 elpwid ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝑦 ⊆ ( 𝑅1 𝐶 ) )
247 simplrr ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝑧 ∈ ( 𝑅1𝐶 ) )
248 247 244 eleqtrd ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝑧 ∈ 𝒫 ( 𝑅1 𝐶 ) )
249 248 elpwid ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → 𝑧 ⊆ ( 𝑅1 𝐶 ) )
250 f1imaeq ( ( 𝐻 : ( 𝑅1 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 𝐶 ) ) ∧ ( 𝑦 ⊆ ( 𝑅1 𝐶 ) ∧ 𝑧 ⊆ ( 𝑅1 𝐶 ) ) ) → ( ( 𝐻𝑦 ) = ( 𝐻𝑧 ) ↔ 𝑦 = 𝑧 ) )
251 238 246 249 250 syl12anc ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( ( 𝐻𝑦 ) = ( 𝐻𝑧 ) ↔ 𝑦 = 𝑧 ) )
252 227 237 251 3bitrd ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) ∧ ¬ 𝐶 = 𝐶 ) → ( if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) = if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻𝑧 ) ) ) ↔ 𝑦 = 𝑧 ) )
253 223 252 pm2.61dan ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) ) → ( if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) = if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻𝑧 ) ) ) ↔ 𝑦 = 𝑧 ) )
254 253 ex ( 𝜑 → ( ( 𝑦 ∈ ( 𝑅1𝐶 ) ∧ 𝑧 ∈ ( 𝑅1𝐶 ) ) → ( if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) = if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻𝑧 ) ) ) ↔ 𝑦 = 𝑧 ) ) )
255 159 254 dom2lem ( 𝜑 → ( 𝑦 ∈ ( 𝑅1𝐶 ) ↦ if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) ) : ( 𝑅1𝐶 ) –1-1→ On )
256 1 2 3 4 5 dfac12lem1 ( 𝜑 → ( 𝐺𝐶 ) = ( 𝑦 ∈ ( 𝑅1𝐶 ) ↦ if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) ) )
257 f1eq1 ( ( 𝐺𝐶 ) = ( 𝑦 ∈ ( 𝑅1𝐶 ) ↦ if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) ) → ( ( 𝐺𝐶 ) : ( 𝑅1𝐶 ) –1-1→ On ↔ ( 𝑦 ∈ ( 𝑅1𝐶 ) ↦ if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) ) : ( 𝑅1𝐶 ) –1-1→ On ) )
258 256 257 syl ( 𝜑 → ( ( 𝐺𝐶 ) : ( 𝑅1𝐶 ) –1-1→ On ↔ ( 𝑦 ∈ ( 𝑅1𝐶 ) ↦ if ( 𝐶 = 𝐶 , ( ( suc ran ( 𝐺𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻𝑦 ) ) ) ) : ( 𝑅1𝐶 ) –1-1→ On ) )
259 255 258 mpbird ( 𝜑 → ( 𝐺𝐶 ) : ( 𝑅1𝐶 ) –1-1→ On )