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

Theorem dfac12lem2 10126
Description: Lemma for dfac12 10131. (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 𝑥 ·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
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 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((OrdIso( E , ran (𝑥 dom 𝑥)) ∘ (𝑥 dom 𝑥)) “ 𝑦))))))
21tfr1 8384 . . . . . . . . . . . . 13 𝐺 Fn On
3 fnfun 6641 . . . . . . . . . . . . 13 (𝐺 Fn On → Fun 𝐺)
42, 3ax-mp 5 . . . . . . . . . . . 12 Fun 𝐺
5 dfac12.5 . . . . . . . . . . . 12 (𝜑𝐶 ∈ On)
6 funimaexg 6626 . . . . . . . . . . . 12 ((Fun 𝐺𝐶 ∈ On) → (𝐺𝐶) ∈ V)
74, 5, 6sylancr 588 . . . . . . . . . . 11 (𝜑 → (𝐺𝐶) ∈ V)
8 uniexg 7717 . . . . . . . . . . 11 ((𝐺𝐶) ∈ V → (𝐺𝐶) ∈ V)
9 rnexg 7882 . . . . . . . . . . 11 ( (𝐺𝐶) ∈ V → ran (𝐺𝐶) ∈ V)
107, 8, 93syl 18 . . . . . . . . . 10 (𝜑 → ran (𝐺𝐶) ∈ V)
11 dfac12.8 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On)
12 f1f 6777 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧):(𝑅1𝑧)–1-1→On → (𝐺𝑧):(𝑅1𝑧)⟶On)
13 fssxp 6735 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧):(𝑅1𝑧)⟶On → (𝐺𝑧) ⊆ ((𝑅1𝑧) × On))
14 ssv 4004 . . . . . . . . . . . . . . . . . . . 20 (𝑅1𝑧) ⊆ V
15 xpss1 5691 . . . . . . . . . . . . . . . . . . . 20 ((𝑅1𝑧) ⊆ V → ((𝑅1𝑧) × On) ⊆ (V × On))
1614, 15ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑅1𝑧) × On) ⊆ (V × On)
17 sstr 3988 . . . . . . . . . . . . . . . . . . 19 (((𝐺𝑧) ⊆ ((𝑅1𝑧) × On) ∧ ((𝑅1𝑧) × On) ⊆ (V × On)) → (𝐺𝑧) ⊆ (V × On))
1816, 17mpan2 690 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑧) ⊆ ((𝑅1𝑧) × On) → (𝐺𝑧) ⊆ (V × On))
19 fvex 6894 . . . . . . . . . . . . . . . . . . 19 (𝐺𝑧) ∈ V
2019elpw 4602 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑧) ∈ 𝒫 (V × On) ↔ (𝐺𝑧) ⊆ (V × On))
2118, 20sylibr 233 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧) ⊆ ((𝑅1𝑧) × On) → (𝐺𝑧) ∈ 𝒫 (V × On))
2212, 13, 213syl 18 . . . . . . . . . . . . . . . 16 ((𝐺𝑧):(𝑅1𝑧)–1-1→On → (𝐺𝑧) ∈ 𝒫 (V × On))
2322ralimi 3084 . . . . . . . . . . . . . . 15 (∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On → ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On))
2411, 23syl 17 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On))
25 onss 7759 . . . . . . . . . . . . . . . . 17 (𝐶 ∈ On → 𝐶 ⊆ On)
265, 25syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ⊆ On)
272fndmi 6645 . . . . . . . . . . . . . . . 16 dom 𝐺 = On
2826, 27sseqtrrdi 4031 . . . . . . . . . . . . . . 15 (𝜑𝐶 ⊆ dom 𝐺)
29 funimass4 6946 . . . . . . . . . . . . . . 15 ((Fun 𝐺𝐶 ⊆ dom 𝐺) → ((𝐺𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On)))
304, 28, 29sylancr 588 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On)))
3124, 30mpbird 257 . . . . . . . . . . . . 13 (𝜑 → (𝐺𝐶) ⊆ 𝒫 (V × On))
32 sspwuni 5099 . . . . . . . . . . . . 13 ((𝐺𝐶) ⊆ 𝒫 (V × On) ↔ (𝐺𝐶) ⊆ (V × On))
3331, 32sylib 217 . . . . . . . . . . . 12 (𝜑 (𝐺𝐶) ⊆ (V × On))
34 rnss 5933 . . . . . . . . . . . 12 ( (𝐺𝐶) ⊆ (V × On) → ran (𝐺𝐶) ⊆ ran (V × On))
3533, 34syl 17 . . . . . . . . . . 11 (𝜑 → ran (𝐺𝐶) ⊆ ran (V × On))
36 rnxpss 6163 . . . . . . . . . . 11 ran (V × On) ⊆ On
3735, 36sstrdi 3992 . . . . . . . . . 10 (𝜑 → ran (𝐺𝐶) ⊆ On)
38 ssonuni 7754 . . . . . . . . . 10 (ran (𝐺𝐶) ∈ V → (ran (𝐺𝐶) ⊆ On → ran (𝐺𝐶) ∈ On))
3910, 37, 38sylc 65 . . . . . . . . 9 (𝜑 ran (𝐺𝐶) ∈ On)
40 onsuc 7786 . . . . . . . . 9 ( ran (𝐺𝐶) ∈ On → suc ran (𝐺𝐶) ∈ On)
4139, 40syl 17 . . . . . . . 8 (𝜑 → suc ran (𝐺𝐶) ∈ On)
4241ad2antrr 725 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → suc ran (𝐺𝐶) ∈ On)
43 rankon 9777 . . . . . . 7 (rank‘𝑦) ∈ On
44 omcl 8523 . . . . . . 7 ((suc ran (𝐺𝐶) ∈ On ∧ (rank‘𝑦) ∈ On) → (suc ran (𝐺𝐶) ·o (rank‘𝑦)) ∈ On)
4542, 43, 44sylancl 587 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (suc ran (𝐺𝐶) ·o (rank‘𝑦)) ∈ On)
46 fveq2 6881 . . . . . . . . . . 11 (𝑧 = suc (rank‘𝑦) → (𝐺𝑧) = (𝐺‘suc (rank‘𝑦)))
47 f1eq1 6772 . . . . . . . . . . 11 ((𝐺𝑧) = (𝐺‘suc (rank‘𝑦)) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1𝑧)–1-1→On))
4846, 47syl 17 . . . . . . . . . 10 (𝑧 = suc (rank‘𝑦) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1𝑧)–1-1→On))
49 fveq2 6881 . . . . . . . . . . 11 (𝑧 = suc (rank‘𝑦) → (𝑅1𝑧) = (𝑅1‘suc (rank‘𝑦)))
50 f1eq2 6773 . . . . . . . . . . 11 ((𝑅1𝑧) = (𝑅1‘suc (rank‘𝑦)) → ((𝐺‘suc (rank‘𝑦)):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
5149, 50syl 17 . . . . . . . . . 10 (𝑧 = suc (rank‘𝑦) → ((𝐺‘suc (rank‘𝑦)):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
5248, 51bitrd 279 . . . . . . . . 9 (𝑧 = suc (rank‘𝑦) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
5311ad2antrr 725 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On)
54 rankr1ai 9780 . . . . . . . . . . . 12 (𝑦 ∈ (𝑅1𝐶) → (rank‘𝑦) ∈ 𝐶)
5554ad2antlr 726 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ 𝐶)
56 simpr 486 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝐶 = 𝐶)
5755, 56eleqtrd 2836 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ 𝐶)
58 eloni 6366 . . . . . . . . . . . . 13 (𝐶 ∈ On → Ord 𝐶)
595, 58syl 17 . . . . . . . . . . . 12 (𝜑 → Ord 𝐶)
6059ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → Ord 𝐶)
61 ordsucuniel 7799 . . . . . . . . . . 11 (Ord 𝐶 → ((rank‘𝑦) ∈ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
6260, 61syl 17 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((rank‘𝑦) ∈ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
6357, 62mpbid 231 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → suc (rank‘𝑦) ∈ 𝐶)
6452, 53, 63rspcdva 3612 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
65 f1f 6777 . . . . . . . 8 ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))⟶On)
6664, 65syl 17 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))⟶On)
67 r1elwf 9778 . . . . . . . . 9 (𝑦 ∈ (𝑅1𝐶) → 𝑦 (𝑅1 “ On))
6867ad2antlr 726 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝑦 (𝑅1 “ On))
69 rankidb 9782 . . . . . . . 8 (𝑦 (𝑅1 “ On) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
7068, 69syl 17 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
7166, 70ffvelcdmd 7075 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On)
72 oacl 8522 . . . . . 6 (((suc ran (𝐺𝐶) ·o (rank‘𝑦)) ∈ On ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On) → ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
7345, 71, 72syl2anc 585 . . . . 5 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
74 dfac12.3 . . . . . . . 8 (𝜑𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On)
75 f1f 6777 . . . . . . . 8 (𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On → 𝐹:𝒫 (har‘(𝑅1𝐴))⟶On)
7674, 75syl 17 . . . . . . 7 (𝜑𝐹:𝒫 (har‘(𝑅1𝐴))⟶On)
7776ad2antrr 725 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐹:𝒫 (har‘(𝑅1𝐴))⟶On)
78 imassrn 6063 . . . . . . . 8 (𝐻𝑦) ⊆ ran 𝐻
79 fvex 6894 . . . . . . . . . . . . . . 15 (𝐺 𝐶) ∈ V
8079rnex 7890 . . . . . . . . . . . . . 14 ran (𝐺 𝐶) ∈ V
81 fveq2 6881 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝐶 → (𝐺𝑧) = (𝐺 𝐶))
82 f1eq1 6772 . . . . . . . . . . . . . . . . . . 19 ((𝐺𝑧) = (𝐺 𝐶) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1𝑧)–1-1→On))
8381, 82syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝐶 → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1𝑧)–1-1→On))
84 fveq2 6881 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝐶 → (𝑅1𝑧) = (𝑅1 𝐶))
85 f1eq2 6773 . . . . . . . . . . . . . . . . . . 19 ((𝑅1𝑧) = (𝑅1 𝐶) → ((𝐺 𝐶):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1 𝐶)–1-1→On))
8684, 85syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝐶 → ((𝐺 𝐶):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1 𝐶)–1-1→On))
8783, 86bitrd 279 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝐶 → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1 𝐶)–1-1→On))
8811ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On)
895ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 ∈ On)
90 onuni 7763 . . . . . . . . . . . . . . . . . . 19 (𝐶 ∈ On → 𝐶 ∈ On)
91 sucidg 6437 . . . . . . . . . . . . . . . . . . 19 ( 𝐶 ∈ On → 𝐶 ∈ suc 𝐶)
9289, 90, 913syl 18 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 ∈ suc 𝐶)
9359adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (𝑅1𝐶)) → Ord 𝐶)
94 orduniorsuc 7805 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝐶 → (𝐶 = 𝐶𝐶 = suc 𝐶))
9593, 94syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (𝑅1𝐶)) → (𝐶 = 𝐶𝐶 = suc 𝐶))
9695orcanai 1002 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 = suc 𝐶)
9792, 96eleqtrrd 2837 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐶)
9887, 88, 97rspcdva 3612 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐺 𝐶):(𝑅1 𝐶)–1-1→On)
99 f1f 6777 . . . . . . . . . . . . . . . 16 ((𝐺 𝐶):(𝑅1 𝐶)–1-1→On → (𝐺 𝐶):(𝑅1 𝐶)⟶On)
100 frn 6714 . . . . . . . . . . . . . . . 16 ((𝐺 𝐶):(𝑅1 𝐶)⟶On → ran (𝐺 𝐶) ⊆ On)
10198, 99, 1003syl 18 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran (𝐺 𝐶) ⊆ On)
102 epweon 7749 . . . . . . . . . . . . . . 15 E We On
103 wess 5659 . . . . . . . . . . . . . . 15 (ran (𝐺 𝐶) ⊆ On → ( E We On → E We ran (𝐺 𝐶)))
104101, 102, 103mpisyl 21 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → E We ran (𝐺 𝐶))
105 eqid 2733 . . . . . . . . . . . . . . 15 OrdIso( E , ran (𝐺 𝐶)) = OrdIso( E , ran (𝐺 𝐶))
106105oiiso 9519 . . . . . . . . . . . . . 14 ((ran (𝐺 𝐶) ∈ V ∧ E We ran (𝐺 𝐶)) → OrdIso( E , ran (𝐺 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺 𝐶)), ran (𝐺 𝐶)))
10780, 104, 106sylancr 588 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → OrdIso( E , ran (𝐺 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺 𝐶)), ran (𝐺 𝐶)))
108 isof1o 7307 . . . . . . . . . . . . 13 (OrdIso( E , ran (𝐺 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺 𝐶)), ran (𝐺 𝐶)) → OrdIso( E , ran (𝐺 𝐶)):dom OrdIso( E , ran (𝐺 𝐶))–1-1-onto→ran (𝐺 𝐶))
109 f1ocnv 6835 . . . . . . . . . . . . 13 (OrdIso( E , ran (𝐺 𝐶)):dom OrdIso( E , ran (𝐺 𝐶))–1-1-onto→ran (𝐺 𝐶) → OrdIso( E , ran (𝐺 𝐶)):ran (𝐺 𝐶)–1-1-onto→dom OrdIso( E , ran (𝐺 𝐶)))
110 f1of1 6822 . . . . . . . . . . . . 13 (OrdIso( E , ran (𝐺 𝐶)):ran (𝐺 𝐶)–1-1-onto→dom OrdIso( E , ran (𝐺 𝐶)) → OrdIso( E , ran (𝐺 𝐶)):ran (𝐺 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
111107, 108, 109, 1104syl 19 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → OrdIso( E , ran (𝐺 𝐶)):ran (𝐺 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
112 f1f1orn 6834 . . . . . . . . . . . . 13 ((𝐺 𝐶):(𝑅1 𝐶)–1-1→On → (𝐺 𝐶):(𝑅1 𝐶)–1-1-onto→ran (𝐺 𝐶))
113 f1of1 6822 . . . . . . . . . . . . 13 ((𝐺 𝐶):(𝑅1 𝐶)–1-1-onto→ran (𝐺 𝐶) → (𝐺 𝐶):(𝑅1 𝐶)–1-1→ran (𝐺 𝐶))
11498, 112, 1133syl 18 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐺 𝐶):(𝑅1 𝐶)–1-1→ran (𝐺 𝐶))
115 f1co 6789 . . . . . . . . . . . 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 (𝐺 𝐶)))
116111, 114, 115syl2anc 585 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)):(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
117 dfac12.h . . . . . . . . . . . 12 𝐻 = (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶))
118 f1eq1 6772 . . . . . . . . . . . 12 (𝐻 = (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)) → (𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) ↔ (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)):(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶))))
119117, 118ax-mp 5 . . . . . . . . . . 11 (𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) ↔ (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)):(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
120116, 119sylibr 233 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
121 f1f 6777 . . . . . . . . . 10 (𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) → 𝐻:(𝑅1 𝐶)⟶dom OrdIso( E , ran (𝐺 𝐶)))
122 frn 6714 . . . . . . . . . 10 (𝐻:(𝑅1 𝐶)⟶dom OrdIso( E , ran (𝐺 𝐶)) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺 𝐶)))
123120, 121, 1223syl 18 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺 𝐶)))
124 harcl 9541 . . . . . . . . . . 11 (har‘(𝑅1𝐴)) ∈ On
125124onordi 6467 . . . . . . . . . 10 Ord (har‘(𝑅1𝐴))
126105oion 9518 . . . . . . . . . . . 12 (ran (𝐺 𝐶) ∈ V → dom OrdIso( E , ran (𝐺 𝐶)) ∈ On)
12780, 126mp1i 13 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ∈ On)
128105oien 9520 . . . . . . . . . . . . 13 ((ran (𝐺 𝐶) ∈ V ∧ E We ran (𝐺 𝐶)) → dom OrdIso( E , ran (𝐺 𝐶)) ≈ ran (𝐺 𝐶))
12980, 104, 128sylancr 588 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ≈ ran (𝐺 𝐶))
130 fvex 6894 . . . . . . . . . . . . . . 15 (𝑅1 𝐶) ∈ V
131130f1oen 8957 . . . . . . . . . . . . . 14 ((𝐺 𝐶):(𝑅1 𝐶)–1-1-onto→ran (𝐺 𝐶) → (𝑅1 𝐶) ≈ ran (𝐺 𝐶))
132 ensym 8987 . . . . . . . . . . . . . 14 ((𝑅1 𝐶) ≈ ran (𝐺 𝐶) → ran (𝐺 𝐶) ≈ (𝑅1 𝐶))
13398, 112, 131, 1324syl 19 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran (𝐺 𝐶) ≈ (𝑅1 𝐶))
134 fvex 6894 . . . . . . . . . . . . . 14 (𝑅1𝐴) ∈ V
135 dfac12.1 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ On)
136135ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐴 ∈ On)
137 dfac12.6 . . . . . . . . . . . . . . . . 17 (𝜑𝐶𝐴)
138137ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐴)
139138, 97sseldd 3981 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐴)
140 r1ord2 9763 . . . . . . . . . . . . . . 15 (𝐴 ∈ On → ( 𝐶𝐴 → (𝑅1 𝐶) ⊆ (𝑅1𝐴)))
141136, 139, 140sylc 65 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1 𝐶) ⊆ (𝑅1𝐴))
142 ssdomg 8984 . . . . . . . . . . . . . 14 ((𝑅1𝐴) ∈ V → ((𝑅1 𝐶) ⊆ (𝑅1𝐴) → (𝑅1 𝐶) ≼ (𝑅1𝐴)))
143134, 141, 142mpsyl 68 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1 𝐶) ≼ (𝑅1𝐴))
144 endomtr 8996 . . . . . . . . . . . . 13 ((ran (𝐺 𝐶) ≈ (𝑅1 𝐶) ∧ (𝑅1 𝐶) ≼ (𝑅1𝐴)) → ran (𝐺 𝐶) ≼ (𝑅1𝐴))
145133, 143, 144syl2anc 585 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran (𝐺 𝐶) ≼ (𝑅1𝐴))
146 endomtr 8996 . . . . . . . . . . . 12 ((dom OrdIso( E , ran (𝐺 𝐶)) ≈ ran (𝐺 𝐶) ∧ ran (𝐺 𝐶) ≼ (𝑅1𝐴)) → dom OrdIso( E , ran (𝐺 𝐶)) ≼ (𝑅1𝐴))
147129, 145, 146syl2anc 585 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ≼ (𝑅1𝐴))
148 elharval 9543 . . . . . . . . . . 11 (dom OrdIso( E , ran (𝐺 𝐶)) ∈ (har‘(𝑅1𝐴)) ↔ (dom OrdIso( E , ran (𝐺 𝐶)) ∈ On ∧ dom OrdIso( E , ran (𝐺 𝐶)) ≼ (𝑅1𝐴)))
149127, 147, 148sylanbrc 584 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ∈ (har‘(𝑅1𝐴)))
150 ordelss 6372 . . . . . . . . . 10 ((Ord (har‘(𝑅1𝐴)) ∧ dom OrdIso( E , ran (𝐺 𝐶)) ∈ (har‘(𝑅1𝐴))) → dom OrdIso( E , ran (𝐺 𝐶)) ⊆ (har‘(𝑅1𝐴)))
151125, 149, 150sylancr 588 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ⊆ (har‘(𝑅1𝐴)))
152123, 151sstrd 3990 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran 𝐻 ⊆ (har‘(𝑅1𝐴)))
15378, 152sstrid 3991 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ⊆ (har‘(𝑅1𝐴)))
154 fvex 6894 . . . . . . . 8 (har‘(𝑅1𝐴)) ∈ V
155154elpw2 5341 . . . . . . 7 ((𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)) ↔ (𝐻𝑦) ⊆ (har‘(𝑅1𝐴)))
156153, 155sylibr 233 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)))
15777, 156ffvelcdmd 7075 . . . . 5 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐹‘(𝐻𝑦)) ∈ On)
15873, 157ifclda 4559 . . . 4 ((𝜑𝑦 ∈ (𝑅1𝐶)) → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) ∈ On)
159158ex 414 . . 3 (𝜑 → (𝑦 ∈ (𝑅1𝐶) → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) ∈ On))
160 iftrue 4530 . . . . . . . 8 (𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)))
161 iftrue 4530 . . . . . . . 8 (𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) = ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)))
162160, 161eqeq12d 2749 . . . . . . 7 (𝐶 = 𝐶 → (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‘𝑧))‘𝑧))))
163162adantl 483 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅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‘𝑧))‘𝑧))))
16441ad2antrr 725 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → suc ran (𝐺𝐶) ∈ On)
165 nsuceq0 6439 . . . . . . . 8 suc ran (𝐺𝐶) ≠ ∅
166165a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → suc ran (𝐺𝐶) ≠ ∅)
16743a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ On)
168 onsucuni 7803 . . . . . . . . . . 11 (ran (𝐺𝐶) ⊆ On → ran (𝐺𝐶) ⊆ suc ran (𝐺𝐶))
16937, 168syl 17 . . . . . . . . . 10 (𝜑 → ran (𝐺𝐶) ⊆ suc ran (𝐺𝐶))
170169ad2antrr 725 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ran (𝐺𝐶) ⊆ suc ran (𝐺𝐶))
17126ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝐶 ⊆ On)
172 fnfvima 7222 . . . . . . . . . . . 12 ((𝐺 Fn On ∧ 𝐶 ⊆ On ∧ suc (rank‘𝑦) ∈ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺𝐶))
1732, 171, 63, 172mp3an2i 1467 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺𝐶))
174 elssuni 4937 . . . . . . . . . . 11 ((𝐺‘suc (rank‘𝑦)) ∈ (𝐺𝐶) → (𝐺‘suc (rank‘𝑦)) ⊆ (𝐺𝐶))
175 rnss 5933 . . . . . . . . . . 11 ((𝐺‘suc (rank‘𝑦)) ⊆ (𝐺𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran (𝐺𝐶))
176173, 174, 1753syl 18 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran (𝐺𝐶))
177 f1fn 6778 . . . . . . . . . . . 12 ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)))
17864, 177syl 17 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)))
179 fnfvelrn 7070 . . . . . . . . . . 11 (((𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)) ∧ 𝑦 ∈ (𝑅1‘suc (rank‘𝑦))) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
180178, 70, 179syl2anc 585 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
181176, 180sseldd 3981 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺𝐶))
182170, 181sseldd 3981 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶))
183182adantlrr 720 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶))
184 rankon 9777 . . . . . . . 8 (rank‘𝑧) ∈ On
185184a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (rank‘𝑧) ∈ On)
186 eleq1w 2817 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑦 ∈ (𝑅1𝐶) ↔ 𝑧 ∈ (𝑅1𝐶)))
187186anbi2d 630 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝜑𝑦 ∈ (𝑅1𝐶)) ↔ (𝜑𝑧 ∈ (𝑅1𝐶))))
188187anbi1d 631 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) ↔ ((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶)))
189 fveq2 6881 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (rank‘𝑦) = (rank‘𝑧))
190 suceq 6422 . . . . . . . . . . . . . 14 ((rank‘𝑦) = (rank‘𝑧) → suc (rank‘𝑦) = suc (rank‘𝑧))
191189, 190syl 17 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → suc (rank‘𝑦) = suc (rank‘𝑧))
192191fveq2d 6885 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
193 id 22 . . . . . . . . . . . 12 (𝑦 = 𝑧𝑦 = 𝑧)
194192, 193fveq12d 6888 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
195194eleq1d 2819 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶) ↔ ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶)))
196188, 195imbi12d 345 . . . . . . . . 9 (𝑦 = 𝑧 → ((((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶)) ↔ (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶))))
197196, 182chvarvv 2003 . . . . . . . 8 (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶))
198197adantlrl 719 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶))
199 omopth2 8572 . . . . . . 7 (((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‘𝑧))‘𝑧))))
200164, 166, 167, 183, 185, 198, 199syl222anc 1387 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))))
201190adantl 483 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → suc (rank‘𝑦) = suc (rank‘𝑧))
202201fveq2d 6885 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
203202fveq1d 6883 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → ((𝐺‘suc (rank‘𝑦))‘𝑧) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
204203eqeq2d 2744 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
20564adantlrr 720 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
206205adantr 482 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
20770adantlrr 720 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
208207adantr 482 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
209 r1elwf 9778 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑅1𝐶) → 𝑧 (𝑅1 “ On))
210 rankidb 9782 . . . . . . . . . . . . . . 15 (𝑧 (𝑅1 “ On) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
211209, 210syl 17 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑅1𝐶) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
212211ad2antll 728 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
213212ad2antrr 725 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
214201fveq2d 6885 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝑅1‘suc (rank‘𝑦)) = (𝑅1‘suc (rank‘𝑧)))
215213, 214eleqtrrd 2837 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑦)))
216 f1fveq 7248 . . . . . . . . . . 11 (((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On ∧ (𝑦 ∈ (𝑅1‘suc (rank‘𝑦)) ∧ 𝑧 ∈ (𝑅1‘suc (rank‘𝑦)))) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧))
217206, 208, 215, 216syl12anc 836 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧))
218204, 217bitr3d 281 . . . . . . . . 9 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) ↔ 𝑦 = 𝑧))
219218biimpd 228 . . . . . . . 8 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) → 𝑦 = 𝑧))
220219expimpd 455 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) → 𝑦 = 𝑧))
221189, 194jca 513 . . . . . . 7 (𝑦 = 𝑧 → ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
222220, 221impbid1 224 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ 𝑦 = 𝑧))
223163, 200, 2223bitrd 305 . . . . 5 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧))
224 iffalse 4533 . . . . . . . 8 𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = (𝐹‘(𝐻𝑦)))
225 iffalse 4533 . . . . . . . 8 𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) = (𝐹‘(𝐻𝑧)))
226224, 225eqeq12d 2749 . . . . . . 7 𝐶 = 𝐶 → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ (𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧))))
227226adantl 483 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ (𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧))))
22874ad2antrr 725 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On)
229156adantlrr 720 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)))
230187anbi1d 631 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) ↔ ((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶)))
231 imaeq2 6048 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝐻𝑦) = (𝐻𝑧))
232231eleq1d 2819 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)) ↔ (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴))))
233230, 232imbi12d 345 . . . . . . . . 9 (𝑦 = 𝑧 → ((((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴))) ↔ (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))))
234233, 156chvarvv 2003 . . . . . . . 8 (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))
235234adantlrl 719 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))
236 f1fveq 7248 . . . . . . 7 ((𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On ∧ ((𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)) ∧ (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))) → ((𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧)) ↔ (𝐻𝑦) = (𝐻𝑧)))
237228, 229, 235, 236syl12anc 836 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → ((𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧)) ↔ (𝐻𝑦) = (𝐻𝑧)))
238120adantlrr 720 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
239 simplrl 776 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑦 ∈ (𝑅1𝐶))
24096fveq2d 6885 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1𝐶) = (𝑅1‘suc 𝐶))
241 r1suc 9752 . . . . . . . . . . . 12 ( 𝐶 ∈ On → (𝑅1‘suc 𝐶) = 𝒫 (𝑅1 𝐶))
24289, 90, 2413syl 18 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1‘suc 𝐶) = 𝒫 (𝑅1 𝐶))
243240, 242eqtrd 2773 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1𝐶) = 𝒫 (𝑅1 𝐶))
244243adantlrr 720 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (𝑅1𝐶) = 𝒫 (𝑅1 𝐶))
245239, 244eleqtrd 2836 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑦 ∈ 𝒫 (𝑅1 𝐶))
246245elpwid 4607 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑦 ⊆ (𝑅1 𝐶))
247 simplrr 777 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑧 ∈ (𝑅1𝐶))
248247, 244eleqtrd 2836 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑧 ∈ 𝒫 (𝑅1 𝐶))
249248elpwid 4607 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑧 ⊆ (𝑅1 𝐶))
250 f1imaeq 7251 . . . . . . 7 ((𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) ∧ (𝑦 ⊆ (𝑅1 𝐶) ∧ 𝑧 ⊆ (𝑅1 𝐶))) → ((𝐻𝑦) = (𝐻𝑧) ↔ 𝑦 = 𝑧))
251238, 246, 249, 250syl12anc 836 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → ((𝐻𝑦) = (𝐻𝑧) ↔ 𝑦 = 𝑧))
252227, 237, 2513bitrd 305 . . . . 5 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧))
253223, 252pm2.61dan 812 . . . 4 ((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧))
254253ex 414 . . 3 (𝜑 → ((𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶)) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧)))
255159, 254dom2lem 8976 . 2 (𝜑 → (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))):(𝑅1𝐶)–1-1→On)
256135, 74, 1, 5, 117dfac12lem1 10125 . . 3 (𝜑 → (𝐺𝐶) = (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))))
257 f1eq1 6772 . . 3 ((𝐺𝐶) = (𝑦 ∈ (𝑅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))
258256, 257syl 17 . 2 (𝜑 → ((𝐺𝐶):(𝑅1𝐶)–1-1→On ↔ (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))):(𝑅1𝐶)–1-1→On))
259255, 258mpbird 257 1 (𝜑 → (𝐺𝐶):(𝑅1𝐶)–1-1→On)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846   = wceq 1542  wcel 2107  wne 2941  wral 3062  Vcvv 3475  wss 3946  c0 4320  ifcif 4524  𝒫 cpw 4598   cuni 4904   class class class wbr 5144  cmpt 5227   E cep 5575   We wwe 5626   × cxp 5670  ccnv 5671  dom cdm 5672  ran crn 5673  cima 5675  ccom 5676  Ord word 6355  Oncon0 6356  suc csuc 6358  Fun wfun 6529   Fn wfn 6530  wf 6531  1-1wf1 6532  1-1-ontowf1o 6534  cfv 6535   Isom wiso 6536  (class class class)co 7396  recscrecs 8357   +o coa 8450   ·o comu 8451  cen 8924  cdom 8925  OrdIsocoi 9491  harchar 9538  𝑅1cr1 9744  rankcrnk 9745
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5359  ax-pr 5423  ax-un 7712
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-int 4947  df-iun 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6292  df-ord 6359  df-on 6360  df-lim 6361  df-suc 6362  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-isom 6544  df-riota 7352  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7843  df-2nd 7963  df-frecs 8253  df-wrecs 8284  df-recs 8358  df-rdg 8397  df-oadd 8457  df-omul 8458  df-er 8691  df-en 8928  df-dom 8929  df-oi 9492  df-har 9539  df-r1 9746  df-rank 9747
This theorem is referenced by:  dfac12lem3  10127
  Copyright terms: Public domain W3C validator