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

Theorem dfac12lem2 8917
Description: Lemma for dfac12 8922. (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 7445 . . . . . . . . . . . . 13 𝐺 Fn On
3 fnfun 5951 . . . . . . . . . . . . 13 (𝐺 Fn On → Fun 𝐺)
42, 3ax-mp 5 . . . . . . . . . . . 12 Fun 𝐺
5 dfac12.5 . . . . . . . . . . . 12 (𝜑𝐶 ∈ On)
6 funimaexg 5938 . . . . . . . . . . . 12 ((Fun 𝐺𝐶 ∈ On) → (𝐺𝐶) ∈ V)
74, 5, 6sylancr 694 . . . . . . . . . . 11 (𝜑 → (𝐺𝐶) ∈ V)
8 uniexg 6915 . . . . . . . . . . 11 ((𝐺𝐶) ∈ V → (𝐺𝐶) ∈ V)
9 rnexg 7052 . . . . . . . . . . 11 ( (𝐺𝐶) ∈ V → ran (𝐺𝐶) ∈ V)
107, 8, 93syl 18 . . . . . . . . . 10 (𝜑 → ran (𝐺𝐶) ∈ V)
11 dfac12.8 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On)
12 f1f 6063 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧):(𝑅1𝑧)–1-1→On → (𝐺𝑧):(𝑅1𝑧)⟶On)
13 fssxp 6022 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧):(𝑅1𝑧)⟶On → (𝐺𝑧) ⊆ ((𝑅1𝑧) × On))
14 ssv 3609 . . . . . . . . . . . . . . . . . . . 20 (𝑅1𝑧) ⊆ V
15 xpss1 5194 . . . . . . . . . . . . . . . . . . . 20 ((𝑅1𝑧) ⊆ V → ((𝑅1𝑧) × On) ⊆ (V × On))
1614, 15ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑅1𝑧) × On) ⊆ (V × On)
17 sstr 3595 . . . . . . . . . . . . . . . . . . 19 (((𝐺𝑧) ⊆ ((𝑅1𝑧) × On) ∧ ((𝑅1𝑧) × On) ⊆ (V × On)) → (𝐺𝑧) ⊆ (V × On))
1816, 17mpan2 706 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑧) ⊆ ((𝑅1𝑧) × On) → (𝐺𝑧) ⊆ (V × On))
19 fvex 6163 . . . . . . . . . . . . . . . . . . 19 (𝐺𝑧) ∈ V
2019elpw 4141 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑧) ∈ 𝒫 (V × On) ↔ (𝐺𝑧) ⊆ (V × On))
2118, 20sylibr 224 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧) ⊆ ((𝑅1𝑧) × On) → (𝐺𝑧) ∈ 𝒫 (V × On))
2212, 13, 213syl 18 . . . . . . . . . . . . . . . 16 ((𝐺𝑧):(𝑅1𝑧)–1-1→On → (𝐺𝑧) ∈ 𝒫 (V × On))
2322ralimi 2947 . . . . . . . . . . . . . . 15 (∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On → ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On))
2411, 23syl 17 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On))
25 onss 6944 . . . . . . . . . . . . . . . . 17 (𝐶 ∈ On → 𝐶 ⊆ On)
265, 25syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ⊆ On)
27 fndm 5953 . . . . . . . . . . . . . . . . 17 (𝐺 Fn On → dom 𝐺 = On)
282, 27ax-mp 5 . . . . . . . . . . . . . . . 16 dom 𝐺 = On
2926, 28syl6sseqr 3636 . . . . . . . . . . . . . . 15 (𝜑𝐶 ⊆ dom 𝐺)
30 funimass4 6209 . . . . . . . . . . . . . . 15 ((Fun 𝐺𝐶 ⊆ dom 𝐺) → ((𝐺𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On)))
314, 29, 30sylancr 694 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On)))
3224, 31mpbird 247 . . . . . . . . . . . . 13 (𝜑 → (𝐺𝐶) ⊆ 𝒫 (V × On))
33 sspwuni 4582 . . . . . . . . . . . . 13 ((𝐺𝐶) ⊆ 𝒫 (V × On) ↔ (𝐺𝐶) ⊆ (V × On))
3432, 33sylib 208 . . . . . . . . . . . 12 (𝜑 (𝐺𝐶) ⊆ (V × On))
35 rnss 5319 . . . . . . . . . . . 12 ( (𝐺𝐶) ⊆ (V × On) → ran (𝐺𝐶) ⊆ ran (V × On))
3634, 35syl 17 . . . . . . . . . . 11 (𝜑 → ran (𝐺𝐶) ⊆ ran (V × On))
37 rnxpss 5530 . . . . . . . . . . 11 ran (V × On) ⊆ On
3836, 37syl6ss 3599 . . . . . . . . . 10 (𝜑 → ran (𝐺𝐶) ⊆ On)
39 ssonuni 6940 . . . . . . . . . 10 (ran (𝐺𝐶) ∈ V → (ran (𝐺𝐶) ⊆ On → ran (𝐺𝐶) ∈ On))
4010, 38, 39sylc 65 . . . . . . . . 9 (𝜑 ran (𝐺𝐶) ∈ On)
41 suceloni 6967 . . . . . . . . 9 ( ran (𝐺𝐶) ∈ On → suc ran (𝐺𝐶) ∈ On)
4240, 41syl 17 . . . . . . . 8 (𝜑 → suc ran (𝐺𝐶) ∈ On)
4342ad2antrr 761 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → suc ran (𝐺𝐶) ∈ On)
44 rankon 8609 . . . . . . 7 (rank‘𝑦) ∈ On
45 omcl 7568 . . . . . . 7 ((suc ran (𝐺𝐶) ∈ On ∧ (rank‘𝑦) ∈ On) → (suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) ∈ On)
4643, 44, 45sylancl 693 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) ∈ On)
47 rankr1ai 8612 . . . . . . . . . . . 12 (𝑦 ∈ (𝑅1𝐶) → (rank‘𝑦) ∈ 𝐶)
4847ad2antlr 762 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ 𝐶)
49 simpr 477 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝐶 = 𝐶)
5048, 49eleqtrd 2700 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ 𝐶)
51 eloni 5697 . . . . . . . . . . . . 13 (𝐶 ∈ On → Ord 𝐶)
525, 51syl 17 . . . . . . . . . . . 12 (𝜑 → Ord 𝐶)
5352ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → Ord 𝐶)
54 ordsucuniel 6978 . . . . . . . . . . 11 (Ord 𝐶 → ((rank‘𝑦) ∈ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
5553, 54syl 17 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((rank‘𝑦) ∈ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
5650, 55mpbid 222 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → suc (rank‘𝑦) ∈ 𝐶)
5711ad2antrr 761 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On)
58 fveq2 6153 . . . . . . . . . . . 12 (𝑧 = suc (rank‘𝑦) → (𝐺𝑧) = (𝐺‘suc (rank‘𝑦)))
59 f1eq1 6058 . . . . . . . . . . . 12 ((𝐺𝑧) = (𝐺‘suc (rank‘𝑦)) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1𝑧)–1-1→On))
6058, 59syl 17 . . . . . . . . . . 11 (𝑧 = suc (rank‘𝑦) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1𝑧)–1-1→On))
61 fveq2 6153 . . . . . . . . . . . 12 (𝑧 = suc (rank‘𝑦) → (𝑅1𝑧) = (𝑅1‘suc (rank‘𝑦)))
62 f1eq2 6059 . . . . . . . . . . . 12 ((𝑅1𝑧) = (𝑅1‘suc (rank‘𝑦)) → ((𝐺‘suc (rank‘𝑦)):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
6361, 62syl 17 . . . . . . . . . . 11 (𝑧 = suc (rank‘𝑦) → ((𝐺‘suc (rank‘𝑦)):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
6460, 63bitrd 268 . . . . . . . . . 10 (𝑧 = suc (rank‘𝑦) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
6564rspcv 3294 . . . . . . . . 9 (suc (rank‘𝑦) ∈ 𝐶 → (∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
6656, 57, 65sylc 65 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
67 f1f 6063 . . . . . . . 8 ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))⟶On)
6866, 67syl 17 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))⟶On)
69 r1elwf 8610 . . . . . . . . 9 (𝑦 ∈ (𝑅1𝐶) → 𝑦 (𝑅1 “ On))
7069ad2antlr 762 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝑦 (𝑅1 “ On))
71 rankidb 8614 . . . . . . . 8 (𝑦 (𝑅1 “ On) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
7270, 71syl 17 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
7368, 72ffvelrnd 6321 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On)
74 oacl 7567 . . . . . 6 (((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) ∈ On ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On) → ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
7546, 73, 74syl2anc 692 . . . . 5 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
76 dfac12.3 . . . . . . . 8 (𝜑𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On)
77 f1f 6063 . . . . . . . 8 (𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On → 𝐹:𝒫 (har‘(𝑅1𝐴))⟶On)
7876, 77syl 17 . . . . . . 7 (𝜑𝐹:𝒫 (har‘(𝑅1𝐴))⟶On)
7978ad2antrr 761 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐹:𝒫 (har‘(𝑅1𝐴))⟶On)
80 imassrn 5441 . . . . . . . 8 (𝐻𝑦) ⊆ ran 𝐻
81 fvex 6163 . . . . . . . . . . . . . . 15 (𝐺 𝐶) ∈ V
8281rnex 7054 . . . . . . . . . . . . . 14 ran (𝐺 𝐶) ∈ V
835ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 ∈ On)
84 onuni 6947 . . . . . . . . . . . . . . . . . . 19 (𝐶 ∈ On → 𝐶 ∈ On)
85 sucidg 5767 . . . . . . . . . . . . . . . . . . 19 ( 𝐶 ∈ On → 𝐶 ∈ suc 𝐶)
8683, 84, 853syl 18 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 ∈ suc 𝐶)
8752adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (𝑅1𝐶)) → Ord 𝐶)
88 orduniorsuc 6984 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝐶 → (𝐶 = 𝐶𝐶 = suc 𝐶))
8987, 88syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (𝑅1𝐶)) → (𝐶 = 𝐶𝐶 = suc 𝐶))
9089orcanai 951 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 = suc 𝐶)
9186, 90eleqtrrd 2701 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐶)
9211ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On)
93 fveq2 6153 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝐶 → (𝐺𝑧) = (𝐺 𝐶))
94 f1eq1 6058 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝑧) = (𝐺 𝐶) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1𝑧)–1-1→On))
9593, 94syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝐶 → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1𝑧)–1-1→On))
96 fveq2 6153 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝐶 → (𝑅1𝑧) = (𝑅1 𝐶))
97 f1eq2 6059 . . . . . . . . . . . . . . . . . . . 20 ((𝑅1𝑧) = (𝑅1 𝐶) → ((𝐺 𝐶):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1 𝐶)–1-1→On))
9896, 97syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝐶 → ((𝐺 𝐶):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1 𝐶)–1-1→On))
9995, 98bitrd 268 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝐶 → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1 𝐶)–1-1→On))
10099rspcv 3294 . . . . . . . . . . . . . . . . 17 ( 𝐶𝐶 → (∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On → (𝐺 𝐶):(𝑅1 𝐶)–1-1→On))
10191, 92, 100sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐺 𝐶):(𝑅1 𝐶)–1-1→On)
102 f1f 6063 . . . . . . . . . . . . . . . 16 ((𝐺 𝐶):(𝑅1 𝐶)–1-1→On → (𝐺 𝐶):(𝑅1 𝐶)⟶On)
103 frn 6015 . . . . . . . . . . . . . . . 16 ((𝐺 𝐶):(𝑅1 𝐶)⟶On → ran (𝐺 𝐶) ⊆ On)
104101, 102, 1033syl 18 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran (𝐺 𝐶) ⊆ On)
105 epweon 6937 . . . . . . . . . . . . . . 15 E We On
106 wess 5066 . . . . . . . . . . . . . . 15 (ran (𝐺 𝐶) ⊆ On → ( E We On → E We ran (𝐺 𝐶)))
107104, 105, 106mpisyl 21 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → E We ran (𝐺 𝐶))
108 eqid 2621 . . . . . . . . . . . . . . 15 OrdIso( E , ran (𝐺 𝐶)) = OrdIso( E , ran (𝐺 𝐶))
109108oiiso 8393 . . . . . . . . . . . . . 14 ((ran (𝐺 𝐶) ∈ V ∧ E We ran (𝐺 𝐶)) → OrdIso( E , ran (𝐺 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺 𝐶)), ran (𝐺 𝐶)))
11082, 107, 109sylancr 694 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → OrdIso( E , ran (𝐺 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺 𝐶)), ran (𝐺 𝐶)))
111 isof1o 6533 . . . . . . . . . . . . 13 (OrdIso( E , ran (𝐺 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺 𝐶)), ran (𝐺 𝐶)) → OrdIso( E , ran (𝐺 𝐶)):dom OrdIso( E , ran (𝐺 𝐶))–1-1-onto→ran (𝐺 𝐶))
112 f1ocnv 6111 . . . . . . . . . . . . 13 (OrdIso( E , ran (𝐺 𝐶)):dom OrdIso( E , ran (𝐺 𝐶))–1-1-onto→ran (𝐺 𝐶) → OrdIso( E , ran (𝐺 𝐶)):ran (𝐺 𝐶)–1-1-onto→dom OrdIso( E , ran (𝐺 𝐶)))
113 f1of1 6098 . . . . . . . . . . . . 13 (OrdIso( E , ran (𝐺 𝐶)):ran (𝐺 𝐶)–1-1-onto→dom OrdIso( E , ran (𝐺 𝐶)) → OrdIso( E , ran (𝐺 𝐶)):ran (𝐺 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
114110, 111, 112, 1134syl 19 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → OrdIso( E , ran (𝐺 𝐶)):ran (𝐺 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
115 f1f1orn 6110 . . . . . . . . . . . . 13 ((𝐺 𝐶):(𝑅1 𝐶)–1-1→On → (𝐺 𝐶):(𝑅1 𝐶)–1-1-onto→ran (𝐺 𝐶))
116 f1of1 6098 . . . . . . . . . . . . 13 ((𝐺 𝐶):(𝑅1 𝐶)–1-1-onto→ran (𝐺 𝐶) → (𝐺 𝐶):(𝑅1 𝐶)–1-1→ran (𝐺 𝐶))
117101, 115, 1163syl 18 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐺 𝐶):(𝑅1 𝐶)–1-1→ran (𝐺 𝐶))
118 f1co 6072 . . . . . . . . . . . 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 (𝐺 𝐶)))
119114, 117, 118syl2anc 692 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)):(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
120 dfac12.h . . . . . . . . . . . 12 𝐻 = (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶))
121 f1eq1 6058 . . . . . . . . . . . 12 (𝐻 = (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)) → (𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) ↔ (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)):(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶))))
122120, 121ax-mp 5 . . . . . . . . . . 11 (𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) ↔ (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)):(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
123119, 122sylibr 224 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
124 f1f 6063 . . . . . . . . . 10 (𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) → 𝐻:(𝑅1 𝐶)⟶dom OrdIso( E , ran (𝐺 𝐶)))
125 frn 6015 . . . . . . . . . 10 (𝐻:(𝑅1 𝐶)⟶dom OrdIso( E , ran (𝐺 𝐶)) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺 𝐶)))
126123, 124, 1253syl 18 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺 𝐶)))
127 harcl 8417 . . . . . . . . . . 11 (har‘(𝑅1𝐴)) ∈ On
128127onordi 5796 . . . . . . . . . 10 Ord (har‘(𝑅1𝐴))
129108oion 8392 . . . . . . . . . . . 12 (ran (𝐺 𝐶) ∈ V → dom OrdIso( E , ran (𝐺 𝐶)) ∈ On)
13082, 129mp1i 13 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ∈ On)
131108oien 8394 . . . . . . . . . . . . 13 ((ran (𝐺 𝐶) ∈ V ∧ E We ran (𝐺 𝐶)) → dom OrdIso( E , ran (𝐺 𝐶)) ≈ ran (𝐺 𝐶))
13282, 107, 131sylancr 694 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ≈ ran (𝐺 𝐶))
133 fvex 6163 . . . . . . . . . . . . . . 15 (𝑅1 𝐶) ∈ V
134133f1oen 7927 . . . . . . . . . . . . . 14 ((𝐺 𝐶):(𝑅1 𝐶)–1-1-onto→ran (𝐺 𝐶) → (𝑅1 𝐶) ≈ ran (𝐺 𝐶))
135 ensym 7956 . . . . . . . . . . . . . 14 ((𝑅1 𝐶) ≈ ran (𝐺 𝐶) → ran (𝐺 𝐶) ≈ (𝑅1 𝐶))
136101, 115, 134, 1354syl 19 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran (𝐺 𝐶) ≈ (𝑅1 𝐶))
137 fvex 6163 . . . . . . . . . . . . . 14 (𝑅1𝐴) ∈ V
138 dfac12.1 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ On)
139138ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐴 ∈ On)
140 dfac12.6 . . . . . . . . . . . . . . . . 17 (𝜑𝐶𝐴)
141140ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐴)
142141, 91sseldd 3588 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐴)
143 r1ord2 8595 . . . . . . . . . . . . . . 15 (𝐴 ∈ On → ( 𝐶𝐴 → (𝑅1 𝐶) ⊆ (𝑅1𝐴)))
144139, 142, 143sylc 65 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1 𝐶) ⊆ (𝑅1𝐴))
145 ssdomg 7952 . . . . . . . . . . . . . 14 ((𝑅1𝐴) ∈ V → ((𝑅1 𝐶) ⊆ (𝑅1𝐴) → (𝑅1 𝐶) ≼ (𝑅1𝐴)))
146137, 144, 145mpsyl 68 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1 𝐶) ≼ (𝑅1𝐴))
147 endomtr 7965 . . . . . . . . . . . . 13 ((ran (𝐺 𝐶) ≈ (𝑅1 𝐶) ∧ (𝑅1 𝐶) ≼ (𝑅1𝐴)) → ran (𝐺 𝐶) ≼ (𝑅1𝐴))
148136, 146, 147syl2anc 692 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran (𝐺 𝐶) ≼ (𝑅1𝐴))
149 endomtr 7965 . . . . . . . . . . . 12 ((dom OrdIso( E , ran (𝐺 𝐶)) ≈ ran (𝐺 𝐶) ∧ ran (𝐺 𝐶) ≼ (𝑅1𝐴)) → dom OrdIso( E , ran (𝐺 𝐶)) ≼ (𝑅1𝐴))
150132, 148, 149syl2anc 692 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ≼ (𝑅1𝐴))
151 elharval 8419 . . . . . . . . . . 11 (dom OrdIso( E , ran (𝐺 𝐶)) ∈ (har‘(𝑅1𝐴)) ↔ (dom OrdIso( E , ran (𝐺 𝐶)) ∈ On ∧ dom OrdIso( E , ran (𝐺 𝐶)) ≼ (𝑅1𝐴)))
152130, 150, 151sylanbrc 697 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ∈ (har‘(𝑅1𝐴)))
153 ordelss 5703 . . . . . . . . . 10 ((Ord (har‘(𝑅1𝐴)) ∧ dom OrdIso( E , ran (𝐺 𝐶)) ∈ (har‘(𝑅1𝐴))) → dom OrdIso( E , ran (𝐺 𝐶)) ⊆ (har‘(𝑅1𝐴)))
154128, 152, 153sylancr 694 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ⊆ (har‘(𝑅1𝐴)))
155126, 154sstrd 3597 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran 𝐻 ⊆ (har‘(𝑅1𝐴)))
15680, 155syl5ss 3598 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ⊆ (har‘(𝑅1𝐴)))
157 fvex 6163 . . . . . . . 8 (har‘(𝑅1𝐴)) ∈ V
158157elpw2 4793 . . . . . . 7 ((𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)) ↔ (𝐻𝑦) ⊆ (har‘(𝑅1𝐴)))
159156, 158sylibr 224 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)))
16079, 159ffvelrnd 6321 . . . . 5 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐹‘(𝐻𝑦)) ∈ On)
16175, 160ifclda 4097 . . . 4 ((𝜑𝑦 ∈ (𝑅1𝐶)) → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) ∈ On)
162161ex 450 . . 3 (𝜑 → (𝑦 ∈ (𝑅1𝐶) → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) ∈ On))
163 iftrue 4069 . . . . . . . 8 (𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)))
164 iftrue 4069 . . . . . . . 8 (𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) = ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)))
165163, 164eqeq12d 2636 . . . . . . 7 (𝐶 = 𝐶 → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧))))
166165adantl 482 . . . . . 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‘𝑧))‘𝑧))))
16742ad2antrr 761 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → suc ran (𝐺𝐶) ∈ On)
168 nsuceq0 5769 . . . . . . . 8 suc ran (𝐺𝐶) ≠ ∅
169168a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → suc ran (𝐺𝐶) ≠ ∅)
17044a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ On)
171 onsucuni 6982 . . . . . . . . . . 11 (ran (𝐺𝐶) ⊆ On → ran (𝐺𝐶) ⊆ suc ran (𝐺𝐶))
17238, 171syl 17 . . . . . . . . . 10 (𝜑 → ran (𝐺𝐶) ⊆ suc ran (𝐺𝐶))
173172ad2antrr 761 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ran (𝐺𝐶) ⊆ suc ran (𝐺𝐶))
1742a1i 11 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝐺 Fn On)
17526ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝐶 ⊆ On)
176 fnfvima 6456 . . . . . . . . . . . 12 ((𝐺 Fn On ∧ 𝐶 ⊆ On ∧ suc (rank‘𝑦) ∈ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺𝐶))
177174, 175, 56, 176syl3anc 1323 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺𝐶))
178 elssuni 4438 . . . . . . . . . . 11 ((𝐺‘suc (rank‘𝑦)) ∈ (𝐺𝐶) → (𝐺‘suc (rank‘𝑦)) ⊆ (𝐺𝐶))
179 rnss 5319 . . . . . . . . . . 11 ((𝐺‘suc (rank‘𝑦)) ⊆ (𝐺𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran (𝐺𝐶))
180177, 178, 1793syl 18 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran (𝐺𝐶))
181 f1fn 6064 . . . . . . . . . . . 12 ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)))
18266, 181syl 17 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)))
183 fnfvelrn 6317 . . . . . . . . . . 11 (((𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)) ∧ 𝑦 ∈ (𝑅1‘suc (rank‘𝑦))) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
184182, 72, 183syl2anc 692 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
185180, 184sseldd 3588 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺𝐶))
186173, 185sseldd 3588 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶))
187186adantlrr 756 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶))
188 rankon 8609 . . . . . . . 8 (rank‘𝑧) ∈ On
189188a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (rank‘𝑧) ∈ On)
190 eleq1 2686 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑦 ∈ (𝑅1𝐶) ↔ 𝑧 ∈ (𝑅1𝐶)))
191190anbi2d 739 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝜑𝑦 ∈ (𝑅1𝐶)) ↔ (𝜑𝑧 ∈ (𝑅1𝐶))))
192191anbi1d 740 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) ↔ ((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶)))
193 fveq2 6153 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (rank‘𝑦) = (rank‘𝑧))
194 suceq 5754 . . . . . . . . . . . . . 14 ((rank‘𝑦) = (rank‘𝑧) → suc (rank‘𝑦) = suc (rank‘𝑧))
195193, 194syl 17 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → suc (rank‘𝑦) = suc (rank‘𝑧))
196195fveq2d 6157 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
197 id 22 . . . . . . . . . . . 12 (𝑦 = 𝑧𝑦 = 𝑧)
198196, 197fveq12d 6159 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
199198eleq1d 2683 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶) ↔ ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶)))
200192, 199imbi12d 334 . . . . . . . . 9 (𝑦 = 𝑧 → ((((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶)) ↔ (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶))))
201200, 186chvarv 2262 . . . . . . . 8 (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶))
202201adantlrl 755 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶))
203 omopth2 7616 . . . . . . 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‘𝑧))‘𝑧))))
204167, 169, 170, 187, 189, 202, 203syl222anc 1339 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))))
205194adantl 482 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → suc (rank‘𝑦) = suc (rank‘𝑧))
206205fveq2d 6157 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
207206fveq1d 6155 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → ((𝐺‘suc (rank‘𝑦))‘𝑧) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
208207eqeq2d 2631 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
20966adantlrr 756 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
210209adantr 481 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
21172adantlrr 756 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
212211adantr 481 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
213 r1elwf 8610 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑅1𝐶) → 𝑧 (𝑅1 “ On))
214 rankidb 8614 . . . . . . . . . . . . . . 15 (𝑧 (𝑅1 “ On) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
215213, 214syl 17 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑅1𝐶) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
216215ad2antll 764 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
217216ad2antrr 761 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
218205fveq2d 6157 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝑅1‘suc (rank‘𝑦)) = (𝑅1‘suc (rank‘𝑧)))
219217, 218eleqtrrd 2701 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑦)))
220 f1fveq 6479 . . . . . . . . . . 11 (((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On ∧ (𝑦 ∈ (𝑅1‘suc (rank‘𝑦)) ∧ 𝑧 ∈ (𝑅1‘suc (rank‘𝑦)))) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧))
221210, 212, 219, 220syl12anc 1321 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧))
222208, 221bitr3d 270 . . . . . . . . 9 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) ↔ 𝑦 = 𝑧))
223222biimpd 219 . . . . . . . 8 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) → 𝑦 = 𝑧))
224223expimpd 628 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) → 𝑦 = 𝑧))
225193, 198jca 554 . . . . . . 7 (𝑦 = 𝑧 → ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
226224, 225impbid1 215 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ 𝑦 = 𝑧))
227166, 204, 2263bitrd 294 . . . . 5 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧))
228 iffalse 4072 . . . . . . . 8 𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = (𝐹‘(𝐻𝑦)))
229 iffalse 4072 . . . . . . . 8 𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) = (𝐹‘(𝐻𝑧)))
230228, 229eqeq12d 2636 . . . . . . 7 𝐶 = 𝐶 → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ (𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧))))
231230adantl 482 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ (𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧))))
23276ad2antrr 761 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On)
233159adantlrr 756 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)))
234191anbi1d 740 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) ↔ ((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶)))
235 imaeq2 5426 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝐻𝑦) = (𝐻𝑧))
236235eleq1d 2683 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)) ↔ (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴))))
237234, 236imbi12d 334 . . . . . . . . 9 (𝑦 = 𝑧 → ((((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴))) ↔ (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))))
238237, 159chvarv 2262 . . . . . . . 8 (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))
239238adantlrl 755 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))
240 f1fveq 6479 . . . . . . 7 ((𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On ∧ ((𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)) ∧ (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))) → ((𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧)) ↔ (𝐻𝑦) = (𝐻𝑧)))
241232, 233, 239, 240syl12anc 1321 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → ((𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧)) ↔ (𝐻𝑦) = (𝐻𝑧)))
242123adantlrr 756 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
243 simplrl 799 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑦 ∈ (𝑅1𝐶))
24490fveq2d 6157 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1𝐶) = (𝑅1‘suc 𝐶))
245 r1suc 8584 . . . . . . . . . . . 12 ( 𝐶 ∈ On → (𝑅1‘suc 𝐶) = 𝒫 (𝑅1 𝐶))
24683, 84, 2453syl 18 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1‘suc 𝐶) = 𝒫 (𝑅1 𝐶))
247244, 246eqtrd 2655 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1𝐶) = 𝒫 (𝑅1 𝐶))
248247adantlrr 756 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (𝑅1𝐶) = 𝒫 (𝑅1 𝐶))
249243, 248eleqtrd 2700 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑦 ∈ 𝒫 (𝑅1 𝐶))
250249elpwid 4146 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑦 ⊆ (𝑅1 𝐶))
251 simplrr 800 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑧 ∈ (𝑅1𝐶))
252251, 248eleqtrd 2700 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑧 ∈ 𝒫 (𝑅1 𝐶))
253252elpwid 4146 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑧 ⊆ (𝑅1 𝐶))
254 f1imaeq 6482 . . . . . . 7 ((𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) ∧ (𝑦 ⊆ (𝑅1 𝐶) ∧ 𝑧 ⊆ (𝑅1 𝐶))) → ((𝐻𝑦) = (𝐻𝑧) ↔ 𝑦 = 𝑧))
255242, 250, 253, 254syl12anc 1321 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → ((𝐻𝑦) = (𝐻𝑧) ↔ 𝑦 = 𝑧))
256231, 241, 2553bitrd 294 . . . . 5 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧))
257227, 256pm2.61dan 831 . . . 4 ((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧))
258257ex 450 . . 3 (𝜑 → ((𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶)) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑧)) +𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧)))
259162, 258dom2lem 7946 . 2 (𝜑 → (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))):(𝑅1𝐶)–1-1→On)
260138, 76, 1, 5, 120dfac12lem1 8916 . . 3 (𝜑 → (𝐺𝐶) = (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))))
261 f1eq1 6058 . . 3 ((𝐺𝐶) = (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))) → ((𝐺𝐶):(𝑅1𝐶)–1-1→On ↔ (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))):(𝑅1𝐶)–1-1→On))
262260, 261syl 17 . 2 (𝜑 → ((𝐺𝐶):(𝑅1𝐶)–1-1→On ↔ (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·𝑜 (rank‘𝑦)) +𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))):(𝑅1𝐶)–1-1→On))
263259, 262mpbird 247 1 (𝜑 → (𝐺𝐶):(𝑅1𝐶)–1-1→On)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  Vcvv 3189  wss 3559  c0 3896  ifcif 4063  𝒫 cpw 4135   cuni 4407   class class class wbr 4618  cmpt 4678   E cep 4988   We wwe 5037   × cxp 5077  ccnv 5078  dom cdm 5079  ran crn 5080  cima 5082  ccom 5083  Ord word 5686  Oncon0 5687  suc csuc 5689  Fun wfun 5846   Fn wfn 5847  wf 5848  1-1wf1 5849  1-1-ontowf1o 5851  cfv 5852   Isom wiso 5853  (class class class)co 6610  recscrecs 7419   +𝑜 coa 7509   ·𝑜 comu 7510  cen 7903  cdom 7904  OrdIsocoi 8365  harchar 8412  𝑅1cr1 8576  rankcrnk 8577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-oadd 7516  df-omul 7517  df-er 7694  df-en 7907  df-dom 7908  df-oi 8366  df-har 8414  df-r1 8578  df-rank 8579
This theorem is referenced by:  dfac12lem3  8918
  Copyright terms: Public domain W3C validator