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

Theorem dfac12lem2 9597
 Description: Lemma for dfac12 9602. (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 8044 . . . . . . . . . . . . 13 𝐺 Fn On
3 fnfun 6435 . . . . . . . . . . . . 13 (𝐺 Fn On → Fun 𝐺)
42, 3ax-mp 5 . . . . . . . . . . . 12 Fun 𝐺
5 dfac12.5 . . . . . . . . . . . 12 (𝜑𝐶 ∈ On)
6 funimaexg 6422 . . . . . . . . . . . 12 ((Fun 𝐺𝐶 ∈ On) → (𝐺𝐶) ∈ V)
74, 5, 6sylancr 591 . . . . . . . . . . 11 (𝜑 → (𝐺𝐶) ∈ V)
8 uniexg 7465 . . . . . . . . . . 11 ((𝐺𝐶) ∈ V → (𝐺𝐶) ∈ V)
9 rnexg 7615 . . . . . . . . . . 11 ( (𝐺𝐶) ∈ V → ran (𝐺𝐶) ∈ V)
107, 8, 93syl 18 . . . . . . . . . 10 (𝜑 → ran (𝐺𝐶) ∈ V)
11 dfac12.8 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On)
12 f1f 6561 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧):(𝑅1𝑧)–1-1→On → (𝐺𝑧):(𝑅1𝑧)⟶On)
13 fssxp 6520 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧):(𝑅1𝑧)⟶On → (𝐺𝑧) ⊆ ((𝑅1𝑧) × On))
14 ssv 3917 . . . . . . . . . . . . . . . . . . . 20 (𝑅1𝑧) ⊆ V
15 xpss1 5544 . . . . . . . . . . . . . . . . . . . 20 ((𝑅1𝑧) ⊆ V → ((𝑅1𝑧) × On) ⊆ (V × On))
1614, 15ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑅1𝑧) × On) ⊆ (V × On)
17 sstr 3901 . . . . . . . . . . . . . . . . . . 19 (((𝐺𝑧) ⊆ ((𝑅1𝑧) × On) ∧ ((𝑅1𝑧) × On) ⊆ (V × On)) → (𝐺𝑧) ⊆ (V × On))
1816, 17mpan2 691 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑧) ⊆ ((𝑅1𝑧) × On) → (𝐺𝑧) ⊆ (V × On))
19 fvex 6672 . . . . . . . . . . . . . . . . . . 19 (𝐺𝑧) ∈ V
2019elpw 4499 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑧) ∈ 𝒫 (V × On) ↔ (𝐺𝑧) ⊆ (V × On))
2118, 20sylibr 237 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧) ⊆ ((𝑅1𝑧) × On) → (𝐺𝑧) ∈ 𝒫 (V × On))
2212, 13, 213syl 18 . . . . . . . . . . . . . . . 16 ((𝐺𝑧):(𝑅1𝑧)–1-1→On → (𝐺𝑧) ∈ 𝒫 (V × On))
2322ralimi 3093 . . . . . . . . . . . . . . 15 (∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On → ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On))
2411, 23syl 17 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On))
25 onss 7505 . . . . . . . . . . . . . . . . 17 (𝐶 ∈ On → 𝐶 ⊆ On)
265, 25syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ⊆ On)
272fndmi 6438 . . . . . . . . . . . . . . . 16 dom 𝐺 = On
2826, 27sseqtrrdi 3944 . . . . . . . . . . . . . . 15 (𝜑𝐶 ⊆ dom 𝐺)
29 funimass4 6719 . . . . . . . . . . . . . . 15 ((Fun 𝐺𝐶 ⊆ dom 𝐺) → ((𝐺𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On)))
304, 28, 29sylancr 591 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧𝐶 (𝐺𝑧) ∈ 𝒫 (V × On)))
3124, 30mpbird 260 . . . . . . . . . . . . 13 (𝜑 → (𝐺𝐶) ⊆ 𝒫 (V × On))
32 sspwuni 4988 . . . . . . . . . . . . 13 ((𝐺𝐶) ⊆ 𝒫 (V × On) ↔ (𝐺𝐶) ⊆ (V × On))
3331, 32sylib 221 . . . . . . . . . . . 12 (𝜑 (𝐺𝐶) ⊆ (V × On))
34 rnss 5781 . . . . . . . . . . . 12 ( (𝐺𝐶) ⊆ (V × On) → ran (𝐺𝐶) ⊆ ran (V × On))
3533, 34syl 17 . . . . . . . . . . 11 (𝜑 → ran (𝐺𝐶) ⊆ ran (V × On))
36 rnxpss 6002 . . . . . . . . . . 11 ran (V × On) ⊆ On
3735, 36sstrdi 3905 . . . . . . . . . 10 (𝜑 → ran (𝐺𝐶) ⊆ On)
38 ssonuni 7501 . . . . . . . . . 10 (ran (𝐺𝐶) ∈ V → (ran (𝐺𝐶) ⊆ On → ran (𝐺𝐶) ∈ On))
3910, 37, 38sylc 65 . . . . . . . . 9 (𝜑 ran (𝐺𝐶) ∈ On)
40 suceloni 7528 . . . . . . . . 9 ( ran (𝐺𝐶) ∈ On → suc ran (𝐺𝐶) ∈ On)
4139, 40syl 17 . . . . . . . 8 (𝜑 → suc ran (𝐺𝐶) ∈ On)
4241ad2antrr 726 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → suc ran (𝐺𝐶) ∈ On)
43 rankon 9250 . . . . . . 7 (rank‘𝑦) ∈ On
44 omcl 8172 . . . . . . 7 ((suc ran (𝐺𝐶) ∈ On ∧ (rank‘𝑦) ∈ On) → (suc ran (𝐺𝐶) ·o (rank‘𝑦)) ∈ On)
4542, 43, 44sylancl 590 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (suc ran (𝐺𝐶) ·o (rank‘𝑦)) ∈ On)
46 fveq2 6659 . . . . . . . . . . 11 (𝑧 = suc (rank‘𝑦) → (𝐺𝑧) = (𝐺‘suc (rank‘𝑦)))
47 f1eq1 6556 . . . . . . . . . . 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 6659 . . . . . . . . . . 11 (𝑧 = suc (rank‘𝑦) → (𝑅1𝑧) = (𝑅1‘suc (rank‘𝑦)))
50 f1eq2 6557 . . . . . . . . . . 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 282 . . . . . . . . 9 (𝑧 = suc (rank‘𝑦) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
5311ad2antrr 726 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On)
54 rankr1ai 9253 . . . . . . . . . . . 12 (𝑦 ∈ (𝑅1𝐶) → (rank‘𝑦) ∈ 𝐶)
5554ad2antlr 727 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ 𝐶)
56 simpr 489 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝐶 = 𝐶)
5755, 56eleqtrd 2855 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ 𝐶)
58 eloni 6180 . . . . . . . . . . . . 13 (𝐶 ∈ On → Ord 𝐶)
595, 58syl 17 . . . . . . . . . . . 12 (𝜑 → Ord 𝐶)
6059ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → Ord 𝐶)
61 ordsucuniel 7539 . . . . . . . . . . 11 (Ord 𝐶 → ((rank‘𝑦) ∈ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
6260, 61syl 17 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((rank‘𝑦) ∈ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
6357, 62mpbid 235 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → suc (rank‘𝑦) ∈ 𝐶)
6452, 53, 63rspcdva 3544 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
65 f1f 6561 . . . . . . . 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 9251 . . . . . . . . 9 (𝑦 ∈ (𝑅1𝐶) → 𝑦 (𝑅1 “ On))
6867ad2antlr 727 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝑦 (𝑅1 “ On))
69 rankidb 9255 . . . . . . . 8 (𝑦 (𝑅1 “ On) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
7068, 69syl 17 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
7166, 70ffvelrnd 6844 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On)
72 oacl 8171 . . . . . 6 (((suc ran (𝐺𝐶) ·o (rank‘𝑦)) ∈ On ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On) → ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
7345, 71, 72syl2anc 588 . . . . 5 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
74 dfac12.3 . . . . . . . 8 (𝜑𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On)
75 f1f 6561 . . . . . . . 8 (𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On → 𝐹:𝒫 (har‘(𝑅1𝐴))⟶On)
7674, 75syl 17 . . . . . . 7 (𝜑𝐹:𝒫 (har‘(𝑅1𝐴))⟶On)
7776ad2antrr 726 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐹:𝒫 (har‘(𝑅1𝐴))⟶On)
78 imassrn 5913 . . . . . . . 8 (𝐻𝑦) ⊆ ran 𝐻
79 fvex 6672 . . . . . . . . . . . . . . 15 (𝐺 𝐶) ∈ V
8079rnex 7623 . . . . . . . . . . . . . 14 ran (𝐺 𝐶) ∈ V
81 fveq2 6659 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝐶 → (𝐺𝑧) = (𝐺 𝐶))
82 f1eq1 6556 . . . . . . . . . . . . . . . . . . 19 ((𝐺𝑧) = (𝐺 𝐶) → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1𝑧)–1-1→On))
8381, 82syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝐶 → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1𝑧)–1-1→On))
84 fveq2 6659 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝐶 → (𝑅1𝑧) = (𝑅1 𝐶))
85 f1eq2 6557 . . . . . . . . . . . . . . . . . . 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 282 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝐶 → ((𝐺𝑧):(𝑅1𝑧)–1-1→On ↔ (𝐺 𝐶):(𝑅1 𝐶)–1-1→On))
8811ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ∀𝑧𝐶 (𝐺𝑧):(𝑅1𝑧)–1-1→On)
895ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 ∈ On)
90 onuni 7508 . . . . . . . . . . . . . . . . . . 19 (𝐶 ∈ On → 𝐶 ∈ On)
91 sucidg 6248 . . . . . . . . . . . . . . . . . . 19 ( 𝐶 ∈ On → 𝐶 ∈ suc 𝐶)
9289, 90, 913syl 18 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 ∈ suc 𝐶)
9359adantr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (𝑅1𝐶)) → Ord 𝐶)
94 orduniorsuc 7545 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝐶 → (𝐶 = 𝐶𝐶 = suc 𝐶))
9593, 94syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (𝑅1𝐶)) → (𝐶 = 𝐶𝐶 = suc 𝐶))
9695orcanai 1001 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 = suc 𝐶)
9792, 96eleqtrrd 2856 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐶)
9887, 88, 97rspcdva 3544 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐺 𝐶):(𝑅1 𝐶)–1-1→On)
99 f1f 6561 . . . . . . . . . . . . . . . 16 ((𝐺 𝐶):(𝑅1 𝐶)–1-1→On → (𝐺 𝐶):(𝑅1 𝐶)⟶On)
100 frn 6505 . . . . . . . . . . . . . . . 16 ((𝐺 𝐶):(𝑅1 𝐶)⟶On → ran (𝐺 𝐶) ⊆ On)
10198, 99, 1003syl 18 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran (𝐺 𝐶) ⊆ On)
102 epweon 7497 . . . . . . . . . . . . . . 15 E We On
103 wess 5512 . . . . . . . . . . . . . . 15 (ran (𝐺 𝐶) ⊆ On → ( E We On → E We ran (𝐺 𝐶)))
104101, 102, 103mpisyl 21 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → E We ran (𝐺 𝐶))
105 eqid 2759 . . . . . . . . . . . . . . 15 OrdIso( E , ran (𝐺 𝐶)) = OrdIso( E , ran (𝐺 𝐶))
106105oiiso 9027 . . . . . . . . . . . . . 14 ((ran (𝐺 𝐶) ∈ V ∧ E We ran (𝐺 𝐶)) → OrdIso( E , ran (𝐺 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺 𝐶)), ran (𝐺 𝐶)))
10780, 104, 106sylancr 591 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → OrdIso( E , ran (𝐺 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺 𝐶)), ran (𝐺 𝐶)))
108 isof1o 7071 . . . . . . . . . . . . 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 6615 . . . . . . . . . . . . 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 6602 . . . . . . . . . . . . 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 6614 . . . . . . . . . . . . 13 ((𝐺 𝐶):(𝑅1 𝐶)–1-1→On → (𝐺 𝐶):(𝑅1 𝐶)–1-1-onto→ran (𝐺 𝐶))
113 f1of1 6602 . . . . . . . . . . . . 13 ((𝐺 𝐶):(𝑅1 𝐶)–1-1-onto→ran (𝐺 𝐶) → (𝐺 𝐶):(𝑅1 𝐶)–1-1→ran (𝐺 𝐶))
11498, 112, 1133syl 18 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐺 𝐶):(𝑅1 𝐶)–1-1→ran (𝐺 𝐶))
115 f1co 6572 . . . . . . . . . . . 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 588 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶)):(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
117 dfac12.h . . . . . . . . . . . 12 𝐻 = (OrdIso( E , ran (𝐺 𝐶)) ∘ (𝐺 𝐶))
118 f1eq1 6556 . . . . . . . . . . . 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 237 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
121 f1f 6561 . . . . . . . . . 10 (𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) → 𝐻:(𝑅1 𝐶)⟶dom OrdIso( E , ran (𝐺 𝐶)))
122 frn 6505 . . . . . . . . . 10 (𝐻:(𝑅1 𝐶)⟶dom OrdIso( E , ran (𝐺 𝐶)) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺 𝐶)))
123120, 121, 1223syl 18 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺 𝐶)))
124 harcl 9049 . . . . . . . . . . 11 (har‘(𝑅1𝐴)) ∈ On
125124onordi 6275 . . . . . . . . . 10 Ord (har‘(𝑅1𝐴))
126105oion 9026 . . . . . . . . . . . 12 (ran (𝐺 𝐶) ∈ V → dom OrdIso( E , ran (𝐺 𝐶)) ∈ On)
12780, 126mp1i 13 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ∈ On)
128105oien 9028 . . . . . . . . . . . . 13 ((ran (𝐺 𝐶) ∈ V ∧ E We ran (𝐺 𝐶)) → dom OrdIso( E , ran (𝐺 𝐶)) ≈ ran (𝐺 𝐶))
12980, 104, 128sylancr 591 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ≈ ran (𝐺 𝐶))
130 fvex 6672 . . . . . . . . . . . . . . 15 (𝑅1 𝐶) ∈ V
131130f1oen 8549 . . . . . . . . . . . . . 14 ((𝐺 𝐶):(𝑅1 𝐶)–1-1-onto→ran (𝐺 𝐶) → (𝑅1 𝐶) ≈ ran (𝐺 𝐶))
132 ensym 8577 . . . . . . . . . . . . . 14 ((𝑅1 𝐶) ≈ ran (𝐺 𝐶) → ran (𝐺 𝐶) ≈ (𝑅1 𝐶))
13398, 112, 131, 1324syl 19 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran (𝐺 𝐶) ≈ (𝑅1 𝐶))
134 fvex 6672 . . . . . . . . . . . . . 14 (𝑅1𝐴) ∈ V
135 dfac12.1 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ On)
136135ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐴 ∈ On)
137 dfac12.6 . . . . . . . . . . . . . . . . 17 (𝜑𝐶𝐴)
138137ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐴)
139138, 97sseldd 3894 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐴)
140 r1ord2 9236 . . . . . . . . . . . . . . 15 (𝐴 ∈ On → ( 𝐶𝐴 → (𝑅1 𝐶) ⊆ (𝑅1𝐴)))
141136, 139, 140sylc 65 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1 𝐶) ⊆ (𝑅1𝐴))
142 ssdomg 8574 . . . . . . . . . . . . . 14 ((𝑅1𝐴) ∈ V → ((𝑅1 𝐶) ⊆ (𝑅1𝐴) → (𝑅1 𝐶) ≼ (𝑅1𝐴)))
143134, 141, 142mpsyl 68 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1 𝐶) ≼ (𝑅1𝐴))
144 endomtr 8586 . . . . . . . . . . . . 13 ((ran (𝐺 𝐶) ≈ (𝑅1 𝐶) ∧ (𝑅1 𝐶) ≼ (𝑅1𝐴)) → ran (𝐺 𝐶) ≼ (𝑅1𝐴))
145133, 143, 144syl2anc 588 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran (𝐺 𝐶) ≼ (𝑅1𝐴))
146 endomtr 8586 . . . . . . . . . . . 12 ((dom OrdIso( E , ran (𝐺 𝐶)) ≈ ran (𝐺 𝐶) ∧ ran (𝐺 𝐶) ≼ (𝑅1𝐴)) → dom OrdIso( E , ran (𝐺 𝐶)) ≼ (𝑅1𝐴))
147129, 145, 146syl2anc 588 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ≼ (𝑅1𝐴))
148 elharval 9051 . . . . . . . . . . 11 (dom OrdIso( E , ran (𝐺 𝐶)) ∈ (har‘(𝑅1𝐴)) ↔ (dom OrdIso( E , ran (𝐺 𝐶)) ∈ On ∧ dom OrdIso( E , ran (𝐺 𝐶)) ≼ (𝑅1𝐴)))
149127, 147, 148sylanbrc 587 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ∈ (har‘(𝑅1𝐴)))
150 ordelss 6186 . . . . . . . . . 10 ((Ord (har‘(𝑅1𝐴)) ∧ dom OrdIso( E , ran (𝐺 𝐶)) ∈ (har‘(𝑅1𝐴))) → dom OrdIso( E , ran (𝐺 𝐶)) ⊆ (har‘(𝑅1𝐴)))
151125, 149, 150sylancr 591 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → dom OrdIso( E , ran (𝐺 𝐶)) ⊆ (har‘(𝑅1𝐴)))
152123, 151sstrd 3903 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → ran 𝐻 ⊆ (har‘(𝑅1𝐴)))
15378, 152sstrid 3904 . . . . . . 7 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ⊆ (har‘(𝑅1𝐴)))
154 fvex 6672 . . . . . . . 8 (har‘(𝑅1𝐴)) ∈ V
155154elpw2 5216 . . . . . . 7 ((𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)) ↔ (𝐻𝑦) ⊆ (har‘(𝑅1𝐴)))
156153, 155sylibr 237 . . . . . 6 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)))
15777, 156ffvelrnd 6844 . . . . 5 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐹‘(𝐻𝑦)) ∈ On)
15873, 157ifclda 4456 . . . 4 ((𝜑𝑦 ∈ (𝑅1𝐶)) → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) ∈ On)
159158ex 417 . . 3 (𝜑 → (𝑦 ∈ (𝑅1𝐶) → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) ∈ On))
160 iftrue 4427 . . . . . . . 8 (𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)))
161 iftrue 4427 . . . . . . . 8 (𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) = ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)))
162160, 161eqeq12d 2775 . . . . . . 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 486 . . . . . 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 726 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → suc ran (𝐺𝐶) ∈ On)
165 nsuceq0 6250 . . . . . . . 8 suc ran (𝐺𝐶) ≠ ∅
166165a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → suc ran (𝐺𝐶) ≠ ∅)
16743a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (rank‘𝑦) ∈ On)
168 onsucuni 7543 . . . . . . . . . . 11 (ran (𝐺𝐶) ⊆ On → ran (𝐺𝐶) ⊆ suc ran (𝐺𝐶))
16937, 168syl 17 . . . . . . . . . 10 (𝜑 → ran (𝐺𝐶) ⊆ suc ran (𝐺𝐶))
170169ad2antrr 726 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ran (𝐺𝐶) ⊆ suc ran (𝐺𝐶))
17126ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → 𝐶 ⊆ On)
172 fnfvima 6988 . . . . . . . . . . . 12 ((𝐺 Fn On ∧ 𝐶 ⊆ On ∧ suc (rank‘𝑦) ∈ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺𝐶))
1732, 171, 63, 172mp3an2i 1464 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺𝐶))
174 elssuni 4831 . . . . . . . . . . 11 ((𝐺‘suc (rank‘𝑦)) ∈ (𝐺𝐶) → (𝐺‘suc (rank‘𝑦)) ⊆ (𝐺𝐶))
175 rnss 5781 . . . . . . . . . . 11 ((𝐺‘suc (rank‘𝑦)) ⊆ (𝐺𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran (𝐺𝐶))
176173, 174, 1753syl 18 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran (𝐺𝐶))
177 f1fn 6562 . . . . . . . . . . . 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 6840 . . . . . . . . . . 11 (((𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)) ∧ 𝑦 ∈ (𝑅1‘suc (rank‘𝑦))) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
180178, 70, 179syl2anc 588 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
181176, 180sseldd 3894 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺𝐶))
182170, 181sseldd 3894 . . . . . . . 8 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶))
183182adantlrr 721 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶))
184 rankon 9250 . . . . . . . 8 (rank‘𝑧) ∈ On
185184a1i 11 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (rank‘𝑧) ∈ On)
186 eleq1w 2835 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑦 ∈ (𝑅1𝐶) ↔ 𝑧 ∈ (𝑅1𝐶)))
187186anbi2d 632 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝜑𝑦 ∈ (𝑅1𝐶)) ↔ (𝜑𝑧 ∈ (𝑅1𝐶))))
188187anbi1d 633 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) ↔ ((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶)))
189 fveq2 6659 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (rank‘𝑦) = (rank‘𝑧))
190 suceq 6235 . . . . . . . . . . . . . 14 ((rank‘𝑦) = (rank‘𝑧) → suc (rank‘𝑦) = suc (rank‘𝑧))
191189, 190syl 17 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → suc (rank‘𝑦) = suc (rank‘𝑧))
192191fveq2d 6663 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
193 id 22 . . . . . . . . . . . 12 (𝑦 = 𝑧𝑦 = 𝑧)
194192, 193fveq12d 6666 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
195194eleq1d 2837 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶) ↔ ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶)))
196188, 195imbi12d 349 . . . . . . . . 9 (𝑦 = 𝑧 → ((((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ran (𝐺𝐶)) ↔ (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶))))
197196, 182chvarvv 2006 . . . . . . . 8 (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶))
198197adantlrl 720 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ran (𝐺𝐶))
199 omopth2 8221 . . . . . . 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 1384 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))))
201190adantl 486 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → suc (rank‘𝑦) = suc (rank‘𝑧))
202201fveq2d 6663 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
203202fveq1d 6661 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → ((𝐺‘suc (rank‘𝑦))‘𝑧) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
204203eqeq2d 2770 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
20564adantlrr 721 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
206205adantr 485 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
20770adantlrr 721 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
208207adantr 485 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
209 r1elwf 9251 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑅1𝐶) → 𝑧 (𝑅1 “ On))
210 rankidb 9255 . . . . . . . . . . . . . . 15 (𝑧 (𝑅1 “ On) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
211209, 210syl 17 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑅1𝐶) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
212211ad2antll 729 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
213212ad2antrr 726 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
214201fveq2d 6663 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝑅1‘suc (rank‘𝑦)) = (𝑅1‘suc (rank‘𝑧)))
215213, 214eleqtrrd 2856 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑦)))
216 f1fveq 7013 . . . . . . . . . . 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 284 . . . . . . . . 9 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) ↔ 𝑦 = 𝑧))
219218biimpd 232 . . . . . . . 8 ((((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) → 𝑦 = 𝑧))
220219expimpd 458 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) → 𝑦 = 𝑧))
221189, 194jca 516 . . . . . . 7 (𝑦 = 𝑧 → ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
222220, 221impbid1 228 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ 𝑦 = 𝑧))
223163, 200, 2223bitrd 309 . . . . 5 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ 𝐶 = 𝐶) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧))
224 iffalse 4430 . . . . . . . 8 𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = (𝐹‘(𝐻𝑦)))
225 iffalse 4430 . . . . . . . 8 𝐶 = 𝐶 → if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) = (𝐹‘(𝐻𝑧)))
226224, 225eqeq12d 2775 . . . . . . 7 𝐶 = 𝐶 → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ (𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧))))
227226adantl 486 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ (𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧))))
22874ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On)
229156adantlrr 721 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)))
230187anbi1d 633 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) ↔ ((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶)))
231 imaeq2 5898 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝐻𝑦) = (𝐻𝑧))
232231eleq1d 2837 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)) ↔ (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴))))
233230, 232imbi12d 349 . . . . . . . . 9 (𝑦 = 𝑧 → ((((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴))) ↔ (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))))
234233, 156chvarvv 2006 . . . . . . . 8 (((𝜑𝑧 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))
235234adantlrl 720 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))
236 f1fveq 7013 . . . . . . 7 ((𝐹:𝒫 (har‘(𝑅1𝐴))–1-1→On ∧ ((𝐻𝑦) ∈ 𝒫 (har‘(𝑅1𝐴)) ∧ (𝐻𝑧) ∈ 𝒫 (har‘(𝑅1𝐴)))) → ((𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧)) ↔ (𝐻𝑦) = (𝐻𝑧)))
237228, 229, 235, 236syl12anc 836 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → ((𝐹‘(𝐻𝑦)) = (𝐹‘(𝐻𝑧)) ↔ (𝐻𝑦) = (𝐻𝑧)))
238120adantlrr 721 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)))
239 simplrl 777 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑦 ∈ (𝑅1𝐶))
24096fveq2d 6663 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1𝐶) = (𝑅1‘suc 𝐶))
241 r1suc 9225 . . . . . . . . . . . 12 ( 𝐶 ∈ On → (𝑅1‘suc 𝐶) = 𝒫 (𝑅1 𝐶))
24289, 90, 2413syl 18 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1‘suc 𝐶) = 𝒫 (𝑅1 𝐶))
243240, 242eqtrd 2794 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝑅1𝐶)) ∧ ¬ 𝐶 = 𝐶) → (𝑅1𝐶) = 𝒫 (𝑅1 𝐶))
244243adantlrr 721 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (𝑅1𝐶) = 𝒫 (𝑅1 𝐶))
245239, 244eleqtrd 2855 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑦 ∈ 𝒫 (𝑅1 𝐶))
246245elpwid 4506 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑦 ⊆ (𝑅1 𝐶))
247 simplrr 778 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑧 ∈ (𝑅1𝐶))
248247, 244eleqtrd 2855 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑧 ∈ 𝒫 (𝑅1 𝐶))
249248elpwid 4506 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → 𝑧 ⊆ (𝑅1 𝐶))
250 f1imaeq 7016 . . . . . . 7 ((𝐻:(𝑅1 𝐶)–1-1→dom OrdIso( E , ran (𝐺 𝐶)) ∧ (𝑦 ⊆ (𝑅1 𝐶) ∧ 𝑧 ⊆ (𝑅1 𝐶))) → ((𝐻𝑦) = (𝐻𝑧) ↔ 𝑦 = 𝑧))
251238, 246, 249, 250syl12anc 836 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → ((𝐻𝑦) = (𝐻𝑧) ↔ 𝑦 = 𝑧))
252227, 237, 2513bitrd 309 . . . . 5 (((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) ∧ ¬ 𝐶 = 𝐶) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧))
253223, 252pm2.61dan 813 . . . 4 ((𝜑 ∧ (𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶))) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧))
254253ex 417 . . 3 (𝜑 → ((𝑦 ∈ (𝑅1𝐶) ∧ 𝑧 ∈ (𝑅1𝐶)) → (if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦))) = if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻𝑧))) ↔ 𝑦 = 𝑧)))
255159, 254dom2lem 8568 . 2 (𝜑 → (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))):(𝑅1𝐶)–1-1→On)
256135, 74, 1, 5, 117dfac12lem1 9596 . . 3 (𝜑 → (𝐺𝐶) = (𝑦 ∈ (𝑅1𝐶) ↦ if(𝐶 = 𝐶, ((suc ran (𝐺𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻𝑦)))))
257 f1eq1 6556 . . 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 260 1 (𝜑 → (𝐺𝐶):(𝑅1𝐶)–1-1→On)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 845   = wceq 1539   ∈ wcel 2112   ≠ wne 2952  ∀wral 3071  Vcvv 3410   ⊆ wss 3859  ∅c0 4226  ifcif 4421  𝒫 cpw 4495  ∪ cuni 4799   class class class wbr 5033   ↦ cmpt 5113   E cep 5435   We wwe 5483   × cxp 5523  ◡ccnv 5524  dom cdm 5525  ran crn 5526   “ cima 5528   ∘ ccom 5529  Ord word 6169  Oncon0 6170  suc csuc 6172  Fun wfun 6330   Fn wfn 6331  ⟶wf 6332  –1-1→wf1 6333  –1-1-onto→wf1o 6335  ‘cfv 6336   Isom wiso 6337  (class class class)co 7151  recscrecs 8018   +o coa 8110   ·o comu 8111   ≈ cen 8525   ≼ cdom 8526  OrdIsocoi 8999  harchar 9046  𝑅1cr1 9217  rankcrnk 9218 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-int 4840  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-se 5485  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-oadd 8117  df-omul 8118  df-er 8300  df-en 8529  df-dom 8530  df-oi 9000  df-har 9047  df-r1 9219  df-rank 9220 This theorem is referenced by:  dfac12lem3  9598
 Copyright terms: Public domain W3C validator