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 )