MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac12lem2 Structured version   Visualization version   GIF version

Theorem dfac12lem2 9248
Description: Lemma for dfac12 9253. (Contributed by Mario Carneiro, 29-May-2015.)
Hypotheses
Ref Expression
dfac12.1 (𝜑𝐴 ∈ On)
dfac12.3 (𝜑𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On)
dfac12.4 𝐺 = recs((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = dom 𝑥, ((suc ran ran 𝑥 ·𝑜 (rank‘𝑦)) +𝑜 ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((OrdIso( E , ran (𝑥 dom 𝑥)) ∘ (𝑥 dom 𝑥)) “ 𝑦))))))
dfac12.5 (𝜑𝐶 ∈ On)
dfac12.h 𝐻 = (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶))
dfac12.6 (𝜑𝐶𝐴)
dfac12.8 (𝜑 → ∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On)
Assertion
Ref Expression
dfac12lem2 (𝜑 → (𝐺𝐶):(𝑅1𝐶)–1-1→On)
Distinct variable groups:   𝑦,𝑧,𝐴   𝑥,𝑦,𝑧,𝐶   𝑥,𝐺,𝑦,𝑧   𝜑,𝑦,𝑧   𝑥,𝐹,𝑦,𝑧   𝑦,𝐻,𝑧
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)   𝐻(𝑥)

Proof of Theorem dfac12lem2
StepHypRef Expression
1 dfac12.4 . . . . . . . . . . . . . 14 𝐺 = recs((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = dom 𝑥, ((suc ran ran 𝑥 ·𝑜 (rank‘𝑦)) +𝑜 ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((OrdIso( E , ran (𝑥 dom 𝑥)) ∘ (𝑥 dom 𝑥)) “ 𝑦))))))
21tfr1 7726 . . . . . . . . . . . . 13 𝐺 Fn On
3 fnfun 6196 . . . . . . . . . . . . 13 (𝐺 Fn On → Fun 𝐺)
42, 3ax-mp 5 . . . . . . . . . . . 12 Fun 𝐺
5 dfac12.5 . . . . . . . . . . . 12 (𝜑𝐶 ∈ On)
6 funimaexg 6183 . . . . . . . . . . . 12 ((Fun 𝐺𝐶 ∈ On) → (𝐺𝐶) ∈ V)
74, 5, 6sylancr 577 . . . . . . . . . . 11 (𝜑 → (𝐺𝐶) ∈ V)
8 uniexg 7182 . . . . . . . . . . 11 ((𝐺𝐶) ∈ V → (𝐺𝐶) ∈ V)
9 rnexg 7325 . . . . . . . . . . 11 ( (𝐺𝐶) ∈ V → ran (𝐺𝐶) ∈ V)
107, 8, 93syl 18 . . . . . . . . . 10 (𝜑 → ran (𝐺𝐶) ∈ V)
11 dfac12.8 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On)
12 f1f 6313 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧):(𝑅1𝑧)–1-1→On → (𝐺𝑧):(𝑅1𝑧)⟶On)
13 fssxp 6272 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧):(𝑅1𝑧)⟶On → (𝐺𝑧) ⊆ ((𝑅1𝑧) × On))
14 ssv 3819 . . . . . . . . . . . . . . . . . . . 20 (𝑅1𝑧) ⊆ V
15 xpss1 5326 . . . . . . . . . . . . . . . . . . . 20 ((𝑅1𝑧) ⊆ V → ((𝑅1𝑧) × On) ⊆ (V × On))
1614, 15ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑅1𝑧) × On) ⊆ (V × On)
17 sstr 3803 . . . . . . . . . . . . . . . . . . 19 (((𝐺𝑧) ⊆ ((𝑅1𝑧) × On) ∧ ((𝑅1𝑧) × On) ⊆ (V × On)) → (𝐺𝑧) ⊆ (V × On))
1816, 17mpan2 674 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑧) ⊆ ((𝑅1𝑧) × On) → (𝐺𝑧) ⊆ (V × On))
19 fvex 6418 . . . . . . . . . . . . . . . . . . 19 (𝐺𝑧) ∈ V
2019elpw 4354 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑧) ∈ 𝒫 (V × On) ↔ (𝐺𝑧) ⊆ (V × On))
2118, 20sylibr 225 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧) ⊆ ((𝑅1𝑧) × On) → (𝐺𝑧) ∈ 𝒫 (V × On))
2212, 13, 213syl 18 . . . . . . . . . . . . . . . 16 ((𝐺𝑧):(𝑅1𝑧)–1-1→On → (𝐺𝑧) ∈ 𝒫 (V × On))
2322ralimi 3139 . . . . . . . . . . . . . . 15 (∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On → ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On))
2411, 23syl 17 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On))
25 onss 7217 . . . . . . . . . . . . . . . . 17 (𝐶 ∈ On → 𝐶 ⊆ On)
265, 25syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ⊆ On)
27 fndm 6198 . . . . . . . . . . . . . . . . 17 (𝐺 Fn On → dom 𝐺 = On)
282, 27ax-mp 5 . . . . . . . . . . . . . . . 16 dom 𝐺 = On
2926, 28syl6sseqr 3846 . . . . . . . . . . . . . . 15 (𝜑𝐶 ⊆ dom 𝐺)
30 funimass4 6465 . . . . . . . . . . . . . . 15 ((Fun 𝐺𝐶 ⊆ dom 𝐺) → ((𝐺𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On)))
314, 29, 30sylancr 577 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On)))
3224, 31mpbird 248 . . . . . . . . . . . . 13 (𝜑 → (𝐺𝐶) ⊆ 𝒫 (V × On))
33 sspwuni 4799 . . . . . . . . . . . . 13 ((𝐺𝐶) ⊆ 𝒫 (V × On) ↔ (𝐺𝐶) ⊆ (V × On))
3432, 33sylib 209 . . . . . . . . . . . 12 (𝜑 (𝐺𝐶) ⊆ (V × On))
35 rnss 5552 . . . . . . . . . . . 12 ( (𝐺𝐶) ⊆ (V × On) → ran (𝐺𝐶) ⊆ ran (V × On))
3634, 35syl 17 . . . . . . . . . . 11 (𝜑 → ran (𝐺𝐶) ⊆ ran (V × On))
37 rnxpss 5774 . . . . . . . . . . 11 ran (V × On) ⊆ On
3836, 37syl6ss 3807 . . . . . . . . . 10 (𝜑 → ran (𝐺𝐶) ⊆ On)
39 ssonuni 7213 . . . . . . . . . 10 (ran (𝐺𝐶) ∈ V → (ran (𝐺𝐶) ⊆ On → ran (𝐺𝐶) ∈ On))
4010, 38, 39sylc 65 . . . . . . . . 9 (𝜑 ran (𝐺𝐶) ∈ On)
41 suceloni 7240 . . . . . . . . 9 ( ran (𝐺𝐶) ∈ On → suc ran (𝐺𝐶) ∈ On)
4240, 41syl 17 . . . . . . . 8 (𝜑 → suc ran (𝐺𝐶) ∈ On)
4342ad2antrr 708 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → suc ran (𝐺𝐶) ∈ On)
44 rankon 8902 . . . . . . 7 (rank‘𝑦) ∈ On
45 omcl 7850 . . . . . . 7 ((suc ran (𝐺𝐶) ∈ On ∧ (rank‘𝑦) ∈ On) → (suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) ∈ On)
4643, 44, 45sylancl 576 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) ∈ On)
47 fveq2 6405 . . . . . . . . . . 11 (𝑧 = suc (rank‘𝑦) → (𝐺𝑧) = (𝐺‘suc (rank‘𝑦)))
48 f1eq1 6308 . . . . . . . . . . 11 ((𝐺𝑧) = (𝐺‘suc (rank‘𝑦)) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1𝑧)–1-1→On))
4947, 48syl 17 . . . . . . . . . 10 (𝑧 = suc (rank‘𝑦) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1𝑧)–1-1→On))
50 fveq2 6405 . . . . . . . . . . 11 (𝑧 = suc (rank‘𝑦) → (𝑅1𝑧) = (𝑅1‘suc (rank‘𝑦)))
51 f1eq2 6309 . . . . . . . . . . 11 ((𝑅1𝑧) = (𝑅1‘suc (rank‘𝑦)) → ((𝐺‘suc (rank‘𝑦)):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
5250, 51syl 17 . . . . . . . . . 10 (𝑧 = suc (rank‘𝑦) → ((𝐺‘suc (rank‘𝑦)):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
5349, 52bitrd 270 . . . . . . . . 9 (𝑧 = suc (rank‘𝑦) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
5411ad2antrr 708 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On)
55 rankr1ai 8905 . . . . . . . . . . . 12 (𝑦 ∈ (𝑅1𝐶) → (rank‘𝑦) ∈ 𝐶)
5655ad2antlr 709 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ 𝐶)
57 simpr 473 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝐶 = 𝐶)
5856, 57eleqtrd 2886 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ 𝐶)
59 eloni 5943 . . . . . . . . . . . . 13 (𝐶 ∈ On → Ord 𝐶)
605, 59syl 17 . . . . . . . . . . . 12 (𝜑 → Ord 𝐶)
6160ad2antrr 708 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → Ord 𝐶)
62 ordsucuniel 7251 . . . . . . . . . . 11 (Ord 𝐶 → ((rank‘𝑦) ∈ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
6361, 62syl 17 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((rank‘𝑦) ∈ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
6458, 63mpbid 223 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → suc (rank‘𝑦) ∈ 𝐶)
6553, 54, 64rspcdva 3507 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
66 f1f 6313 . . . . . . . 8 ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))⟶On)
6765, 66syl 17 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))⟶On)
68 r1elwf 8903 . . . . . . . . 9 (𝑦 ∈ (𝑅1𝐶) → 𝑦 (𝑅1 “ On))
6968ad2antlr 709 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝑦 (𝑅1 “ On))
70 rankidb 8907 . . . . . . . 8 (𝑦 (𝑅1 “ On) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
7169, 70syl 17 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
7267, 71ffvelrnd 6579 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On)
73 oacl 7849 . . . . . 6 (((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) ∈ On ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On) → ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
7446, 72, 73syl2anc 575 . . . . 5 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
75 dfac12.3 . . . . . . . 8 (𝜑𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On)
76 f1f 6313 . . . . . . . 8 (𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On → 𝐹:𝒫 (har‘(𝑅1𝐴))⟶On)
7775, 76syl 17 . . . . . . 7 (𝜑𝐹:𝒫 (har‘(𝑅1𝐴))⟶On)
7877ad2antrr 708 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐹:𝒫 (har‘(𝑅1𝐴))⟶On)
79 imassrn 5684 . . . . . . . 8 (𝐻𝑦) ⊆ ran 𝐻
80 fvex 6418 . . . . . . . . . . . . . . 15 (𝐺 𝐶) ∈ V
8180rnex 7327 . . . . . . . . . . . . . 14 ran (𝐺 𝐶) ∈ V
82 fveq2 6405 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝐶 → (𝐺𝑧) = (𝐺 𝐶))
83 f1eq1 6308 . . . . . . . . . . . . . . . . . . 19 ((𝐺𝑧) = (𝐺 𝐶) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1𝑧)–1-1→On))
8482, 83syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝐶 → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1𝑧)–1-1→On))
85 fveq2 6405 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝐶 → (𝑅1𝑧) = (𝑅1 𝐶))
86 f1eq2 6309 . . . . . . . . . . . . . . . . . . 19 ((𝑅1𝑧) = (𝑅1 𝐶) → ((𝐺 𝐶):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1 𝐶)–1-1→On))
8785, 86syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝐶 → ((𝐺 𝐶):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1 𝐶)–1-1→On))
8884, 87bitrd 270 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝐶 → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1 𝐶)–1-1→On))
8911ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On)
905ad2antrr 708 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 ∈ On)
91 onuni 7220 . . . . . . . . . . . . . . . . . . 19 (𝐶 ∈ On → 𝐶 ∈ On)
92 sucidg 6013 . . . . . . . . . . . . . . . . . . 19 ( 𝐶 ∈ On → 𝐶 ∈ suc 𝐶)
9390, 91, 923syl 18 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 ∈ suc 𝐶)
9460adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (𝑅1𝐶)) → Ord 𝐶)
95 orduniorsuc 7257 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝐶 → (𝐶 = 𝐶𝐶 = suc 𝐶))
9694, 95syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (𝑅1𝐶)) → (𝐶 = 𝐶𝐶 = suc 𝐶))
9796orcanai 1016 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 = suc 𝐶)
9893, 97eleqtrrd 2887 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐶)
9988, 89, 98rspcdva 3507 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐺 𝐶):(𝑅1 𝐶)–1-1→On)
100 f1f 6313 . . . . . . . . . . . . . . . 16 ((𝐺 𝐶):(𝑅1 𝐶)–1-1→On → (𝐺 𝐶):(𝑅1 𝐶)⟶On)
101 frn 6259 . . . . . . . . . . . . . . . 16 ((𝐺 𝐶):(𝑅1 𝐶)⟶On → ran (𝐺 𝐶) ⊆ On)
10299, 100, 1013syl 18 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran (𝐺 𝐶) ⊆ On)
103 epweon 7210 . . . . . . . . . . . . . . 15 E We On
104 wess 5295 . . . . . . . . . . . . . . 15 (ran (𝐺 𝐶) ⊆ On → ( E We On → E We ran (𝐺 𝐶)))
105102, 103, 104mpisyl 21 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → E We ran (𝐺 𝐶))
106 eqid 2805 . . . . . . . . . . . . . . 15 OrdIso( E , ran (𝐺 𝐶)) = OrdIso( E , ran (𝐺 𝐶))
107106oiiso 8678 . . . . . . . . . . . . . 14 ((ran (𝐺 𝐶) ∈ V ∧ E We ran (𝐺 𝐶)) → OrdIso( E , ran (𝐺 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺 𝐶)), ran (𝐺 𝐶)))
10881, 105, 107sylancr 577 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → OrdIso( E , ran (𝐺 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺 𝐶)), ran (𝐺 𝐶)))
109 isof1o 6794 . . . . . . . . . . . . 13 (OrdIso( E , ran (𝐺 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺 𝐶)), ran (𝐺 𝐶)) → OrdIso( E , ran (𝐺 𝐶)):dom OrdIso( E , ran (𝐺 𝐶))–1-1-onto→ran (𝐺 𝐶))
110 f1ocnv 6362 . . . . . . . . . . . . 13 (OrdIso( E , ran (𝐺 𝐶)):dom OrdIso( E , ran (𝐺 𝐶))–1-1-onto→ran (𝐺 𝐶) → OrdIso( E , ran (𝐺 𝐶)):ran (𝐺 𝐶)–1-1-onto→dom OrdIso( E , ran (𝐺 𝐶)))
111 f1of1 6349 . . . . . . . . . . . . 13 (OrdIso( E , ran (𝐺 𝐶)):ran (𝐺 𝐶)–1-1-onto→dom OrdIso( E , ran (𝐺 𝐶)) → OrdIso( E , ran (𝐺 𝐶)):ran (𝐺 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
112108, 109, 110, 1114syl 19 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → OrdIso( E , ran (𝐺 𝐶)):ran (𝐺 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
113 f1f1orn 6361 . . . . . . . . . . . . 13 ((𝐺 𝐶):(𝑅1 𝐶)–1-1→On → (𝐺 𝐶):(𝑅1 𝐶)–1-1-onto→ran (𝐺 𝐶))
114 f1of1 6349 . . . . . . . . . . . . 13 ((𝐺 𝐶):(𝑅1 𝐶)–1-1-onto→ran (𝐺 𝐶) → (𝐺 𝐶):(𝑅1 𝐶)–1-1→ran (𝐺 𝐶))
11599, 113, 1143syl 18 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐺 𝐶):(𝑅1 𝐶)–1-1→ran (𝐺 𝐶))
116 f1co 6323 . . . . . . . . . . . 12 ((OrdIso( E , ran (𝐺 𝐶)):ran (𝐺 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) ∧ (𝐺 𝐶):(𝑅1 𝐶)–1-1→ran (𝐺 𝐶)) → (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)):(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
117112, 115, 116syl2anc 575 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)):(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
118 dfac12.h . . . . . . . . . . . 12 𝐻 = (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶))
119 f1eq1 6308 . . . . . . . . . . . 12 (𝐻 = (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)) → (𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) ↔ (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)):(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶))))
120118, 119ax-mp 5 . . . . . . . . . . 11 (𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) ↔ (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)):(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
121117, 120sylibr 225 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
122 f1f 6313 . . . . . . . . . 10 (𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) → 𝐻:(𝑅1 𝐶)⟶dom OrdIso( E , ran (𝐺 𝐶)))
123 frn 6259 . . . . . . . . . 10 (𝐻:(𝑅1 𝐶)⟶dom OrdIso( E , ran (𝐺 𝐶)) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺 𝐶)))
124121, 122, 1233syl 18 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺 𝐶)))
125 harcl 8702 . . . . . . . . . . 11 (har‘(𝑅1𝐴)) ∈ On
126125onordi 6042 . . . . . . . . . 10 Ord (har‘(𝑅1𝐴))
127106oion 8677 . . . . . . . . . . . 12 (ran (𝐺 𝐶) ∈ V → dom OrdIso( E , ran (𝐺 𝐶)) ∈ On)
12881, 127mp1i 13 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ∈ On)
129106oien 8679 . . . . . . . . . . . . 13 ((ran (𝐺 𝐶) ∈ V ∧ E We ran (𝐺 𝐶)) → dom OrdIso( E , ran (𝐺 𝐶)) ≈ ran (𝐺 𝐶))
13081, 105, 129sylancr 577 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ≈ ran (𝐺 𝐶))
131 fvex 6418 . . . . . . . . . . . . . . 15 (𝑅1 𝐶) ∈ V
132131f1oen 8210 . . . . . . . . . . . . . 14 ((𝐺 𝐶):(𝑅1 𝐶)–1-1-onto→ran (𝐺 𝐶) → (𝑅1 𝐶) ≈ ran (𝐺 𝐶))
133 ensym 8238 . . . . . . . . . . . . . 14 ((𝑅1 𝐶) ≈ ran (𝐺 𝐶) → ran (𝐺 𝐶) ≈ (𝑅1 𝐶))
13499, 113, 132, 1334syl 19 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran (𝐺 𝐶) ≈ (𝑅1 𝐶))
135 fvex 6418 . . . . . . . . . . . . . 14 (𝑅1𝐴) ∈ V
136 dfac12.1 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ On)
137136ad2antrr 708 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐴 ∈ On)
138 dfac12.6 . . . . . . . . . . . . . . . . 17 (𝜑𝐶𝐴)
139138ad2antrr 708 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐴)
140139, 98sseldd 3796 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐴)
141 r1ord2 8888 . . . . . . . . . . . . . . 15 (𝐴 ∈ On → ( 𝐶𝐴 → (𝑅1 𝐶) ⊆ (𝑅1𝐴)))
142137, 140, 141sylc 65 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1 𝐶) ⊆ (𝑅1𝐴))
143 ssdomg 8235 . . . . . . . . . . . . . 14 ((𝑅1𝐴) ∈ V → ((𝑅1 𝐶) ⊆ (𝑅1𝐴) → (𝑅1 𝐶) ≼ (𝑅1𝐴)))
144135, 142, 143mpsyl 68 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1 𝐶) ≼ (𝑅1𝐴))
145 endomtr 8247 . . . . . . . . . . . . 13 ((ran (𝐺 𝐶) ≈ (𝑅1 𝐶) ∧ (𝑅1 𝐶) ≼ (𝑅1𝐴)) → ran (𝐺 𝐶) ≼ (𝑅1𝐴))
146134, 144, 145syl2anc 575 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran (𝐺 𝐶) ≼ (𝑅1𝐴))
147 endomtr 8247 . . . . . . . . . . . 12 ((dom OrdIso( E , ran (𝐺 𝐶)) ≈ ran (𝐺 𝐶) ∧ ran (𝐺 𝐶) ≼ (𝑅1𝐴)) → dom OrdIso( E , ran (𝐺 𝐶)) ≼ (𝑅1𝐴))
148130, 146, 147syl2anc 575 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ≼ (𝑅1𝐴))
149 elharval 8704 . . . . . . . . . . 11 (dom OrdIso( E , ran (𝐺 𝐶)) ∈ (har‘(𝑅1𝐴)) ↔ (dom OrdIso( E , ran (𝐺 𝐶)) ∈ On ∧ dom OrdIso( E , ran (𝐺 𝐶)) ≼ (𝑅1𝐴)))
150128, 148, 149sylanbrc 574 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ∈ (har‘(𝑅1𝐴)))
151 ordelss 5949 . . . . . . . . . 10 ((Ord (har‘(𝑅1𝐴)) ∧ dom OrdIso( E , ran (𝐺 𝐶)) ∈ (har‘(𝑅1𝐴))) → dom OrdIso( E , ran (𝐺 𝐶)) ⊆ (har‘(𝑅1𝐴)))
152126, 150, 151sylancr 577 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ⊆ (har‘(𝑅1𝐴)))
153124, 152sstrd 3805 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran 𝐻 ⊆ (har‘(𝑅1𝐴)))
15479, 153syl5ss 3806 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ⊆ (har‘(𝑅1𝐴)))
155 fvex 6418 . . . . . . . 8 (har‘(𝑅1𝐴)) ∈ V
156155elpw2 5017 . . . . . . 7 ((𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)) ↔ (𝐻𝑦) ⊆ (har‘(𝑅1𝐴)))
157154, 156sylibr 225 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)))
15878, 157ffvelrnd 6579 . . . . 5 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐹‘(𝐻𝑦)) ∈ On)
15974, 158ifclda 4310 . . . 4 ((𝜑𝑦 ∈ (𝑅1𝐶)) → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) ∈ On)
160159ex 399 . . 3 (𝜑 → (𝑦 ∈ (𝑅1𝐶) → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) ∈ On))
161 iftrue 4282 . . . . . . . 8 (𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)))
162 iftrue 4282 . . . . . . . 8 (𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) = ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)))
163161, 162eqeq12d 2820 . . . . . . 7 (𝐶 = 𝐶 → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧))))
164163adantl 469 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧))))
16542ad2antrr 708 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → suc ran (𝐺𝐶) ∈ On)
166 nsuceq0 6015 . . . . . . . 8 suc ran (𝐺𝐶) ≠ ∅
167166a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → suc ran (𝐺𝐶) ≠ ∅)
16844a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ On)
169 onsucuni 7255 . . . . . . . . . . 11 (ran (𝐺𝐶) ⊆ On → ran (𝐺𝐶) ⊆ suc ran (𝐺𝐶))
17038, 169syl 17 . . . . . . . . . 10 (𝜑 → ran (𝐺𝐶) ⊆ suc ran (𝐺𝐶))
171170ad2antrr 708 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ran (𝐺𝐶) ⊆ suc ran (𝐺𝐶))
1722a1i 11 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝐺 Fn On)
17326ad2antrr 708 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝐶 ⊆ On)
174 fnfvima 6718 . . . . . . . . . . . 12 ((𝐺 Fn On ∧ 𝐶 ⊆ On ∧ suc (rank‘𝑦) ∈ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺𝐶))
175172, 173, 64, 174syl3anc 1483 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺𝐶))
176 elssuni 4657 . . . . . . . . . . 11 ((𝐺‘suc (rank‘𝑦)) ∈ (𝐺𝐶) → (𝐺‘suc (rank‘𝑦)) ⊆ (𝐺𝐶))
177 rnss 5552 . . . . . . . . . . 11 ((𝐺‘suc (rank‘𝑦)) ⊆ (𝐺𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran (𝐺𝐶))
178175, 176, 1773syl 18 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran (𝐺𝐶))
179 f1fn 6314 . . . . . . . . . . . 12 ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)))
18065, 179syl 17 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)))
181 fnfvelrn 6575 . . . . . . . . . . 11 (((𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)) ∧ 𝑦 ∈ (𝑅1‘suc (rank‘𝑦))) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
182180, 71, 181syl2anc 575 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
183178, 182sseldd 3796 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺𝐶))
184171, 183sseldd 3796 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶))
185184adantlrr 703 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶))
186 rankon 8902 . . . . . . . 8 (rank‘𝑧) ∈ On
187186a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (rank‘𝑧) ∈ On)
188 eleq1w 2867 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑦 ∈ (𝑅1𝐶) ↔ 𝑧 ∈ (𝑅1𝐶)))
189188anbi2d 616 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝜑𝑦 ∈ (𝑅1𝐶)) ↔ (𝜑𝑧 ∈ (𝑅1𝐶))))
190189anbi1d 617 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) ↔ ((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶)))
191 fveq2 6405 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (rank‘𝑦) = (rank‘𝑧))
192 suceq 6000 . . . . . . . . . . . . . 14 ((rank‘𝑦) = (rank‘𝑧) → suc (rank‘𝑦) = suc (rank‘𝑧))
193191, 192syl 17 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → suc (rank‘𝑦) = suc (rank‘𝑧))
194193fveq2d 6409 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
195 id 22 . . . . . . . . . . . 12 (𝑦 = 𝑧𝑦 = 𝑧)
196194, 195fveq12d 6412 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
197196eleq1d 2869 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶) ↔ ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶)))
198190, 197imbi12d 335 . . . . . . . . 9 (𝑦 = 𝑧 → ((((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶)) ↔ (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶))))
199198, 184chvarv 2439 . . . . . . . 8 (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶))
200199adantlrl 702 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶))
201 omopth2 7898 . . . . . . 7 (((suc ran (𝐺𝐶) ∈ On ∧ suc ran (𝐺𝐶) ≠ ∅) ∧ ((rank‘𝑦) ∈ On ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶)) ∧ ((rank‘𝑧) ∈ On ∧ ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶))) → (((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))))
202165, 167, 168, 185, 187, 200, 201syl222anc 1498 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))))
203192adantl 469 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → suc (rank‘𝑦) = suc (rank‘𝑧))
204203fveq2d 6409 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
205204fveq1d 6407 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → ((𝐺‘suc (rank‘𝑦))‘𝑧) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
206205eqeq2d 2815 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
20765adantlrr 703 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
208207adantr 468 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
20971adantlrr 703 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
210209adantr 468 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
211 r1elwf 8903 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑅1𝐶) → 𝑧 (𝑅1 “ On))
212 rankidb 8907 . . . . . . . . . . . . . . 15 (𝑧 (𝑅1 “ On) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
213211, 212syl 17 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑅1𝐶) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
214213ad2antll 711 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
215214ad2antrr 708 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
216203fveq2d 6409 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝑅1‘suc (rank‘𝑦)) = (𝑅1‘suc (rank‘𝑧)))
217215, 216eleqtrrd 2887 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑦)))
218 f1fveq 6740 . . . . . . . . . . 11 (((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On ∧ (𝑦 ∈ (𝑅1‘suc (rank‘𝑦)) ∧ 𝑧 ∈ (𝑅1‘suc (rank‘𝑦)))) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧))
219208, 210, 217, 218syl12anc 856 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧))
220206, 219bitr3d 272 . . . . . . . . 9 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) ↔ 𝑦 = 𝑧))
221220biimpd 220 . . . . . . . 8 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) → 𝑦 = 𝑧))
222221expimpd 443 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) → 𝑦 = 𝑧))
223191, 196jca 503 . . . . . . 7 (𝑦 = 𝑧 → ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
224222, 223impbid1 216 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ 𝑦 = 𝑧))
225164, 202, 2243bitrd 296 . . . . 5 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧))
226 iffalse 4285 . . . . . . . 8 𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = (𝐹‘(𝐻𝑦)))
227 iffalse 4285 . . . . . . . 8 𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) = (𝐹‘(𝐻𝑧)))
228226, 227eqeq12d 2820 . . . . . . 7 𝐶 = 𝐶 → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ (𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧))))
229228adantl 469 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ (𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧))))
23075ad2antrr 708 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On)
231157adantlrr 703 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)))
232189anbi1d 617 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) ↔ ((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶)))
233 imaeq2 5669 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝐻𝑦) = (𝐻𝑧))
234233eleq1d 2869 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)) ↔ (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴))))
235232, 234imbi12d 335 . . . . . . . . 9 (𝑦 = 𝑧 → ((((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴))) ↔ (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))))
236235, 157chvarv 2439 . . . . . . . 8 (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))
237236adantlrl 702 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))
238 f1fveq 6740 . . . . . . 7 ((𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On ∧ ((𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)) ∧ (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))) → ((𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧)) ↔ (𝐻𝑦) = (𝐻𝑧)))
239230, 231, 237, 238syl12anc 856 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → ((𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧)) ↔ (𝐻𝑦) = (𝐻𝑧)))
240121adantlrr 703 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
241 simplrl 786 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑦 ∈ (𝑅1𝐶))
24297fveq2d 6409 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1𝐶) = (𝑅1‘suc 𝐶))
243 r1suc 8877 . . . . . . . . . . . 12 ( 𝐶 ∈ On → (𝑅1‘suc 𝐶) = 𝒫 (𝑅1 𝐶))
24490, 91, 2433syl 18 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1‘suc 𝐶) = 𝒫 (𝑅1 𝐶))
245242, 244eqtrd 2839 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1𝐶) = 𝒫 (𝑅1 𝐶))
246245adantlrr 703 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (𝑅1𝐶) = 𝒫 (𝑅1 𝐶))
247241, 246eleqtrd 2886 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑦 ∈ 𝒫 (𝑅1 𝐶))
248247elpwid 4360 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑦 ⊆ (𝑅1 𝐶))
249 simplrr 787 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑧 ∈ (𝑅1𝐶))
250249, 246eleqtrd 2886 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑧 ∈ 𝒫 (𝑅1 𝐶))
251250elpwid 4360 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑧 ⊆ (𝑅1 𝐶))
252 f1imaeq 6743 . . . . . . 7 ((𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) ∧ (𝑦 ⊆ (𝑅1 𝐶) ∧ 𝑧 ⊆ (𝑅1 𝐶))) → ((𝐻𝑦) = (𝐻𝑧) ↔ 𝑦 = 𝑧))
253240, 248, 251, 252syl12anc 856 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → ((𝐻𝑦) = (𝐻𝑧) ↔ 𝑦 = 𝑧))
254229, 239, 2533bitrd 296 . . . . 5 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧))
255225, 254pm2.61dan 838 . . . 4 ((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧))
256255ex 399 . . 3 (𝜑 → ((𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶)) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧)))
257160, 256dom2lem 8229 . 2 (𝜑 → (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))):(𝑅1𝐶)–1-1→On)
258136, 75, 1, 5, 118dfac12lem1 9247 . . 3 (𝜑 → (𝐺𝐶) = (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))))
259 f1eq1 6308 . . 3 ((𝐺𝐶) = (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))) → ((𝐺𝐶):(𝑅1𝐶)–1-1→On ↔ (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))):(𝑅1𝐶)–1-1→On))
260258, 259syl 17 . 2 (𝜑 → ((𝐺𝐶):(𝑅1𝐶)–1-1→On ↔ (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))):(𝑅1𝐶)–1-1→On))
261257, 260mpbird 248 1 (𝜑 → (𝐺𝐶):(𝑅1𝐶)–1-1→On)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865   = wceq 1637  wcel 2158  wne 2977  wral 3095  Vcvv 3390  wss 3766  c0 4113  ifcif 4276  𝒫 cpw 4348   cuni 4626   class class class wbr 4840  cmpt 4919   E cep 5220   We wwe 5266   × cxp 5306  ccnv 5307  dom cdm 5308  ran crn 5309  cima 5311  ccom 5312  Ord word 5932  Oncon0 5933  suc csuc 5935  Fun wfun 6092   Fn wfn 6093  wf 6094  1-1wf1 6095  1-1-ontowf1o 6097  cfv 6098   Isom wiso 6099  (class class class)co 6871  recscrecs 7700   +𝑜 coa 7790   ·𝑜 comu 7791  cen 8186  cdom 8187  OrdIsocoi 8650  harchar 8697  𝑅1cr1 8869  rankcrnk 8870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-se 5268  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-isom 6107  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-om 7293  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-oadd 7797  df-omul 7798  df-er 7976  df-en 8190  df-dom 8191  df-oi 8651  df-har 8699  df-r1 8871  df-rank 8872
This theorem is referenced by:  dfac12lem3  9249
  Copyright terms: Public domain W3C validator