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

Theorem dfac12lem2 10081
Description: Lemma for dfac12 10086. (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 8344 . . . . . . . . . . . . 13 𝐺 Fn On
3 fnfun 6603 . . . . . . . . . . . . 13 (𝐺 Fn On β†’ Fun 𝐺)
42, 3ax-mp 5 . . . . . . . . . . . 12 Fun 𝐺
5 dfac12.5 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐢 ∈ On)
6 funimaexg 6588 . . . . . . . . . . . 12 ((Fun 𝐺 ∧ 𝐢 ∈ On) β†’ (𝐺 β€œ 𝐢) ∈ V)
74, 5, 6sylancr 588 . . . . . . . . . . 11 (πœ‘ β†’ (𝐺 β€œ 𝐢) ∈ V)
8 uniexg 7678 . . . . . . . . . . 11 ((𝐺 β€œ 𝐢) ∈ V β†’ βˆͺ (𝐺 β€œ 𝐢) ∈ V)
9 rnexg 7842 . . . . . . . . . . 11 (βˆͺ (𝐺 β€œ 𝐢) ∈ V β†’ ran βˆͺ (𝐺 β€œ 𝐢) ∈ V)
107, 8, 93syl 18 . . . . . . . . . 10 (πœ‘ β†’ ran βˆͺ (𝐺 β€œ 𝐢) ∈ V)
11 dfac12.8 . . . . . . . . . . . . . . 15 (πœ‘ β†’ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On)
12 f1f 6739 . . . . . . . . . . . . . . . . 17 ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On β†’ (πΊβ€˜π‘§):(𝑅1β€˜π‘§)⟢On)
13 fssxp 6697 . . . . . . . . . . . . . . . . 17 ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)⟢On β†’ (πΊβ€˜π‘§) βŠ† ((𝑅1β€˜π‘§) Γ— On))
14 ssv 3969 . . . . . . . . . . . . . . . . . . . 20 (𝑅1β€˜π‘§) βŠ† V
15 xpss1 5653 . . . . . . . . . . . . . . . . . . . 20 ((𝑅1β€˜π‘§) βŠ† V β†’ ((𝑅1β€˜π‘§) Γ— On) βŠ† (V Γ— On))
1614, 15ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑅1β€˜π‘§) Γ— On) βŠ† (V Γ— On)
17 sstr 3953 . . . . . . . . . . . . . . . . . . 19 (((πΊβ€˜π‘§) βŠ† ((𝑅1β€˜π‘§) Γ— On) ∧ ((𝑅1β€˜π‘§) Γ— On) βŠ† (V Γ— On)) β†’ (πΊβ€˜π‘§) βŠ† (V Γ— On))
1816, 17mpan2 690 . . . . . . . . . . . . . . . . . 18 ((πΊβ€˜π‘§) βŠ† ((𝑅1β€˜π‘§) Γ— On) β†’ (πΊβ€˜π‘§) βŠ† (V Γ— On))
19 fvex 6856 . . . . . . . . . . . . . . . . . . 19 (πΊβ€˜π‘§) ∈ V
2019elpw 4565 . . . . . . . . . . . . . . . . . 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 3087 . . . . . . . . . . . . . . 15 (βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On β†’ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§) ∈ 𝒫 (V Γ— On))
2411, 23syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§) ∈ 𝒫 (V Γ— On))
25 onss 7720 . . . . . . . . . . . . . . . . 17 (𝐢 ∈ On β†’ 𝐢 βŠ† On)
265, 25syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐢 βŠ† On)
272fndmi 6607 . . . . . . . . . . . . . . . 16 dom 𝐺 = On
2826, 27sseqtrrdi 3996 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐢 βŠ† dom 𝐺)
29 funimass4 6908 . . . . . . . . . . . . . . 15 ((Fun 𝐺 ∧ 𝐢 βŠ† dom 𝐺) β†’ ((𝐺 β€œ 𝐢) βŠ† 𝒫 (V Γ— On) ↔ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§) ∈ 𝒫 (V Γ— On)))
304, 28, 29sylancr 588 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝐺 β€œ 𝐢) βŠ† 𝒫 (V Γ— On) ↔ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§) ∈ 𝒫 (V Γ— On)))
3124, 30mpbird 257 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐺 β€œ 𝐢) βŠ† 𝒫 (V Γ— On))
32 sspwuni 5061 . . . . . . . . . . . . 13 ((𝐺 β€œ 𝐢) βŠ† 𝒫 (V Γ— On) ↔ βˆͺ (𝐺 β€œ 𝐢) βŠ† (V Γ— On))
3331, 32sylib 217 . . . . . . . . . . . 12 (πœ‘ β†’ βˆͺ (𝐺 β€œ 𝐢) βŠ† (V Γ— On))
34 rnss 5895 . . . . . . . . . . . 12 (βˆͺ (𝐺 β€œ 𝐢) βŠ† (V Γ— On) β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† ran (V Γ— On))
3533, 34syl 17 . . . . . . . . . . 11 (πœ‘ β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† ran (V Γ— On))
36 rnxpss 6125 . . . . . . . . . . 11 ran (V Γ— On) βŠ† On
3735, 36sstrdi 3957 . . . . . . . . . 10 (πœ‘ β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† On)
38 ssonuni 7715 . . . . . . . . . 10 (ran βˆͺ (𝐺 β€œ 𝐢) ∈ V β†’ (ran βˆͺ (𝐺 β€œ 𝐢) βŠ† On β†’ βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On))
3910, 37, 38sylc 65 . . . . . . . . 9 (πœ‘ β†’ βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
40 onsuc 7747 . . . . . . . . 9 (βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
4139, 40syl 17 . . . . . . . 8 (πœ‘ β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
4241ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
43 rankon 9732 . . . . . . 7 (rankβ€˜π‘¦) ∈ On
44 omcl 8483 . . . . . . 7 ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On ∧ (rankβ€˜π‘¦) ∈ On) β†’ (suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) ∈ On)
4542, 43, 44sylancl 587 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) ∈ On)
46 fveq2 6843 . . . . . . . . . . 11 (𝑧 = suc (rankβ€˜π‘¦) β†’ (πΊβ€˜π‘§) = (πΊβ€˜suc (rankβ€˜π‘¦)))
47 f1eq1 6734 . . . . . . . . . . 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 6843 . . . . . . . . . . 11 (𝑧 = suc (rankβ€˜π‘¦) β†’ (𝑅1β€˜π‘§) = (𝑅1β€˜suc (rankβ€˜π‘¦)))
50 f1eq2 6735 . . . . . . . . . . 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 9735 . . . . . . . . . . . 12 (𝑦 ∈ (𝑅1β€˜πΆ) β†’ (rankβ€˜π‘¦) ∈ 𝐢)
5554ad2antlr 726 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (rankβ€˜π‘¦) ∈ 𝐢)
56 simpr 486 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 = βˆͺ 𝐢)
5755, 56eleqtrd 2840 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (rankβ€˜π‘¦) ∈ βˆͺ 𝐢)
58 eloni 6328 . . . . . . . . . . . . 13 (𝐢 ∈ On β†’ Ord 𝐢)
595, 58syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ Ord 𝐢)
6059ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ Ord 𝐢)
61 ordsucuniel 7760 . . . . . . . . . . 11 (Ord 𝐢 β†’ ((rankβ€˜π‘¦) ∈ βˆͺ 𝐢 ↔ suc (rankβ€˜π‘¦) ∈ 𝐢))
6260, 61syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((rankβ€˜π‘¦) ∈ βˆͺ 𝐢 ↔ suc (rankβ€˜π‘¦) ∈ 𝐢))
6357, 62mpbid 231 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ suc (rankβ€˜π‘¦) ∈ 𝐢)
6452, 53, 63rspcdva 3583 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)):(𝑅1β€˜suc (rankβ€˜π‘¦))–1-1β†’On)
65 f1f 6739 . . . . . . . 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 9733 . . . . . . . . 9 (𝑦 ∈ (𝑅1β€˜πΆ) β†’ 𝑦 ∈ βˆͺ (𝑅1 β€œ On))
6867ad2antlr 726 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 ∈ βˆͺ (𝑅1 β€œ On))
69 rankidb 9737 . . . . . . . 8 (𝑦 ∈ βˆͺ (𝑅1 β€œ On) β†’ 𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))
7068, 69syl 17 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))
7166, 70ffvelcdmd 7037 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ On)
72 oacl 8482 . . . . . 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 6739 . . . . . . . 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 6025 . . . . . . . 8 (𝐻 β€œ 𝑦) βŠ† ran 𝐻
79 fvex 6856 . . . . . . . . . . . . . . 15 (πΊβ€˜βˆͺ 𝐢) ∈ V
8079rnex 7850 . . . . . . . . . . . . . 14 ran (πΊβ€˜βˆͺ 𝐢) ∈ V
81 fveq2 6843 . . . . . . . . . . . . . . . . . . 19 (𝑧 = βˆͺ 𝐢 β†’ (πΊβ€˜π‘§) = (πΊβ€˜βˆͺ 𝐢))
82 f1eq1 6734 . . . . . . . . . . . . . . . . . . 19 ((πΊβ€˜π‘§) = (πΊβ€˜βˆͺ 𝐢) β†’ ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On ↔ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜π‘§)–1-1β†’On))
8381, 82syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧 = βˆͺ 𝐢 β†’ ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On ↔ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜π‘§)–1-1β†’On))
84 fveq2 6843 . . . . . . . . . . . . . . . . . . 19 (𝑧 = βˆͺ 𝐢 β†’ (𝑅1β€˜π‘§) = (𝑅1β€˜βˆͺ 𝐢))
85 f1eq2 6735 . . . . . . . . . . . . . . . . . . 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 7724 . . . . . . . . . . . . . . . . . . 19 (𝐢 ∈ On β†’ βˆͺ 𝐢 ∈ On)
91 sucidg 6399 . . . . . . . . . . . . . . . . . . 19 (βˆͺ 𝐢 ∈ On β†’ βˆͺ 𝐢 ∈ suc βˆͺ 𝐢)
9289, 90, 913syl 18 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ suc βˆͺ 𝐢)
9359adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) β†’ Ord 𝐢)
94 orduniorsuc 7766 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝐢 β†’ (𝐢 = βˆͺ 𝐢 ∨ 𝐢 = suc βˆͺ 𝐢))
9593, 94syl 17 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) β†’ (𝐢 = βˆͺ 𝐢 ∨ 𝐢 = suc βˆͺ 𝐢))
9695orcanai 1002 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 = suc βˆͺ 𝐢)
9792, 96eleqtrrd 2841 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ 𝐢)
9887, 88, 97rspcdva 3583 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’On)
99 f1f 6739 . . . . . . . . . . . . . . . 16 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’On β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)⟢On)
100 frn 6676 . . . . . . . . . . . . . . . 16 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)⟢On β†’ ran (πΊβ€˜βˆͺ 𝐢) βŠ† On)
10198, 99, 1003syl 18 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran (πΊβ€˜βˆͺ 𝐢) βŠ† On)
102 epweon 7710 . . . . . . . . . . . . . . 15 E We On
103 wess 5621 . . . . . . . . . . . . . . 15 (ran (πΊβ€˜βˆͺ 𝐢) βŠ† On β†’ ( E We On β†’ E We ran (πΊβ€˜βˆͺ 𝐢)))
104101, 102, 103mpisyl 21 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ E We ran (πΊβ€˜βˆͺ 𝐢))
105 eqid 2737 . . . . . . . . . . . . . . 15 OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) = OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢))
106105oiiso 9474 . . . . . . . . . . . . . 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 7269 . . . . . . . . . . . . 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 6797 . . . . . . . . . . . . 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 6784 . . . . . . . . . . . . 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 6796 . . . . . . . . . . . . 13 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’On β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1-ontoβ†’ran (πΊβ€˜βˆͺ 𝐢))
113 f1of1 6784 . . . . . . . . . . . . 13 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1-ontoβ†’ran (πΊβ€˜βˆͺ 𝐢) β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’ran (πΊβ€˜βˆͺ 𝐢))
11498, 112, 1133syl 18 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’ran (πΊβ€˜βˆͺ 𝐢))
115 f1co 6751 . . . . . . . . . . . 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 6734 . . . . . . . . . . . 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 6739 . . . . . . . . . 10 (𝐻:(𝑅1β€˜βˆͺ 𝐢)–1-1β†’dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β†’ 𝐻:(𝑅1β€˜βˆͺ 𝐢)⟢dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)))
122 frn 6676 . . . . . . . . . 10 (𝐻:(𝑅1β€˜βˆͺ 𝐢)⟢dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β†’ ran 𝐻 βŠ† dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)))
123120, 121, 1223syl 18 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran 𝐻 βŠ† dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)))
124 harcl 9496 . . . . . . . . . . 11 (harβ€˜(𝑅1β€˜π΄)) ∈ On
125124onordi 6429 . . . . . . . . . 10 Ord (harβ€˜(𝑅1β€˜π΄))
126105oion 9473 . . . . . . . . . . . 12 (ran (πΊβ€˜βˆͺ 𝐢) ∈ V β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ On)
12780, 126mp1i 13 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ On)
128105oien 9475 . . . . . . . . . . . . 13 ((ran (πΊβ€˜βˆͺ 𝐢) ∈ V ∧ E We ran (πΊβ€˜βˆͺ 𝐢)) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢))
12980, 104, 128sylancr 588 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢))
130 fvex 6856 . . . . . . . . . . . . . . 15 (𝑅1β€˜βˆͺ 𝐢) ∈ V
131130f1oen 8914 . . . . . . . . . . . . . 14 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1-ontoβ†’ran (πΊβ€˜βˆͺ 𝐢) β†’ (𝑅1β€˜βˆͺ 𝐢) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢))
132 ensym 8944 . . . . . . . . . . . . . 14 ((𝑅1β€˜βˆͺ 𝐢) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢) β†’ ran (πΊβ€˜βˆͺ 𝐢) β‰ˆ (𝑅1β€˜βˆͺ 𝐢))
13398, 112, 131, 1324syl 19 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran (πΊβ€˜βˆͺ 𝐢) β‰ˆ (𝑅1β€˜βˆͺ 𝐢))
134 fvex 6856 . . . . . . . . . . . . . 14 (𝑅1β€˜π΄) ∈ V
135 dfac12.1 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐴 ∈ On)
136135ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐴 ∈ On)
137 dfac12.6 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐢 βŠ† 𝐴)
138137ad2antrr 725 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 βŠ† 𝐴)
139138, 97sseldd 3946 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ 𝐴)
140 r1ord2 9718 . . . . . . . . . . . . . . 15 (𝐴 ∈ On β†’ (βˆͺ 𝐢 ∈ 𝐴 β†’ (𝑅1β€˜βˆͺ 𝐢) βŠ† (𝑅1β€˜π΄)))
141136, 139, 140sylc 65 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜βˆͺ 𝐢) βŠ† (𝑅1β€˜π΄))
142 ssdomg 8941 . . . . . . . . . . . . . 14 ((𝑅1β€˜π΄) ∈ V β†’ ((𝑅1β€˜βˆͺ 𝐢) βŠ† (𝑅1β€˜π΄) β†’ (𝑅1β€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄)))
143134, 141, 142mpsyl 68 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄))
144 endomtr 8953 . . . . . . . . . . . . 13 ((ran (πΊβ€˜βˆͺ 𝐢) β‰ˆ (𝑅1β€˜βˆͺ 𝐢) ∧ (𝑅1β€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄)) β†’ ran (πΊβ€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄))
145133, 143, 144syl2anc 585 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran (πΊβ€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄))
146 endomtr 8953 . . . . . . . . . . . 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 9498 . . . . . . . . . . 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 6334 . . . . . . . . . 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 3955 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran 𝐻 βŠ† (harβ€˜(𝑅1β€˜π΄)))
15378, 152sstrid 3956 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑦) βŠ† (harβ€˜(𝑅1β€˜π΄)))
154 fvex 6856 . . . . . . . 8 (harβ€˜(𝑅1β€˜π΄)) ∈ V
155154elpw2 5303 . . . . . . 7 ((𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)) ↔ (𝐻 β€œ 𝑦) βŠ† (harβ€˜(𝑅1β€˜π΄)))
156153, 155sylibr 233 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)))
15777, 156ffvelcdmd 7037 . . . . 5 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (πΉβ€˜(𝐻 β€œ 𝑦)) ∈ On)
15873, 157ifclda 4522 . . . 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 4493 . . . . . . . 8 (𝐢 = βˆͺ 𝐢 β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)))
161 iftrue 4493 . . . . . . . 8 (𝐢 = βˆͺ 𝐢 β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) = ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)))
162160, 161eqeq12d 2753 . . . . . . 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 6401 . . . . . . . 8 suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) β‰  βˆ…
166165a1i 11 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) β‰  βˆ…)
16743a1i 11 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (rankβ€˜π‘¦) ∈ On)
168 onsucuni 7764 . . . . . . . . . . 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 7184 . . . . . . . . . . . 12 ((𝐺 Fn On ∧ 𝐢 βŠ† On ∧ suc (rankβ€˜π‘¦) ∈ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) ∈ (𝐺 β€œ 𝐢))
1732, 171, 63, 172mp3an2i 1467 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) ∈ (𝐺 β€œ 𝐢))
174 elssuni 4899 . . . . . . . . . . 11 ((πΊβ€˜suc (rankβ€˜π‘¦)) ∈ (𝐺 β€œ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) βŠ† βˆͺ (𝐺 β€œ 𝐢))
175 rnss 5895 . . . . . . . . . . 11 ((πΊβ€˜suc (rankβ€˜π‘¦)) βŠ† βˆͺ (𝐺 β€œ 𝐢) β†’ ran (πΊβ€˜suc (rankβ€˜π‘¦)) βŠ† ran βˆͺ (𝐺 β€œ 𝐢))
176173, 174, 1753syl 18 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ran (πΊβ€˜suc (rankβ€˜π‘¦)) βŠ† ran βˆͺ (𝐺 β€œ 𝐢))
177 f1fn 6740 . . . . . . . . . . . 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 7032 . . . . . . . . . . 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 3946 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ ran βˆͺ (𝐺 β€œ 𝐢))
182170, 181sseldd 3946 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
183182adantlrr 720 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
184 rankon 9732 . . . . . . . 8 (rankβ€˜π‘§) ∈ On
185184a1i 11 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (rankβ€˜π‘§) ∈ On)
186 eleq1w 2821 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ (𝑦 ∈ (𝑅1β€˜πΆ) ↔ 𝑧 ∈ (𝑅1β€˜πΆ)))
187186anbi2d 630 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ ((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ↔ (πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ))))
188187anbi1d 631 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) ↔ ((πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢)))
189 fveq2 6843 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 β†’ (rankβ€˜π‘¦) = (rankβ€˜π‘§))
190 suceq 6384 . . . . . . . . . . . . . 14 ((rankβ€˜π‘¦) = (rankβ€˜π‘§) β†’ suc (rankβ€˜π‘¦) = suc (rankβ€˜π‘§))
191189, 190syl 17 . . . . . . . . . . . . 13 (𝑦 = 𝑧 β†’ suc (rankβ€˜π‘¦) = suc (rankβ€˜π‘§))
192191fveq2d 6847 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) = (πΊβ€˜suc (rankβ€˜π‘§)))
193 id 22 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ 𝑦 = 𝑧)
194192, 193fveq12d 6850 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§))
195194eleq1d 2823 . . . . . . . . . 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 8532 . . . . . . 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 6847 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) = (πΊβ€˜suc (rankβ€˜π‘§)))
203202fveq1d 6845 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘§) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§))
204203eqeq2d 2748 . . . . . . . . . 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 9733 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑅1β€˜πΆ) β†’ 𝑧 ∈ βˆͺ (𝑅1 β€œ On))
210 rankidb 9737 . . . . . . . . . . . . . . 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 6847 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ (𝑅1β€˜suc (rankβ€˜π‘¦)) = (𝑅1β€˜suc (rankβ€˜π‘§)))
215213, 214eleqtrrd 2841 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ 𝑧 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))
216 f1fveq 7210 . . . . . . . . . . 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 4496 . . . . . . . 8 (Β¬ 𝐢 = βˆͺ 𝐢 β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = (πΉβ€˜(𝐻 β€œ 𝑦)))
225 iffalse 4496 . . . . . . . 8 (Β¬ 𝐢 = βˆͺ 𝐢 β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) = (πΉβ€˜(𝐻 β€œ 𝑧)))
226224, 225eqeq12d 2753 . . . . . . 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 6010 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ (𝐻 β€œ 𝑦) = (𝐻 β€œ 𝑧))
232231eleq1d 2823 . . . . . . . . . 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 7210 . . . . . . 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 6847 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜πΆ) = (𝑅1β€˜suc βˆͺ 𝐢))
241 r1suc 9707 . . . . . . . . . . . 12 (βˆͺ 𝐢 ∈ On β†’ (𝑅1β€˜suc βˆͺ 𝐢) = 𝒫 (𝑅1β€˜βˆͺ 𝐢))
24289, 90, 2413syl 18 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜suc βˆͺ 𝐢) = 𝒫 (𝑅1β€˜βˆͺ 𝐢))
243240, 242eqtrd 2777 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜πΆ) = 𝒫 (𝑅1β€˜βˆͺ 𝐢))
244243adantlrr 720 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜πΆ) = 𝒫 (𝑅1β€˜βˆͺ 𝐢))
245239, 244eleqtrd 2840 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 ∈ 𝒫 (𝑅1β€˜βˆͺ 𝐢))
246245elpwid 4570 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 βŠ† (𝑅1β€˜βˆͺ 𝐢))
247 simplrr 777 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑧 ∈ (𝑅1β€˜πΆ))
248247, 244eleqtrd 2840 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑧 ∈ 𝒫 (𝑅1β€˜βˆͺ 𝐢))
249248elpwid 4570 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑧 βŠ† (𝑅1β€˜βˆͺ 𝐢))
250 f1imaeq 7213 . . . . . . 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 8933 . 2 (πœ‘ β†’ (𝑦 ∈ (𝑅1β€˜πΆ) ↦ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦)))):(𝑅1β€˜πΆ)–1-1β†’On)
256135, 74, 1, 5, 117dfac12lem1 10080 . . 3 (πœ‘ β†’ (πΊβ€˜πΆ) = (𝑦 ∈ (𝑅1β€˜πΆ) ↦ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦)))))
257 f1eq1 6734 . . 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 2944  βˆ€wral 3065  Vcvv 3446   βŠ† wss 3911  βˆ…c0 4283  ifcif 4487  π’« cpw 4561  βˆͺ cuni 4866   class class class wbr 5106   ↦ cmpt 5189   E cep 5537   We wwe 5588   Γ— cxp 5632  β—‘ccnv 5633  dom cdm 5634  ran crn 5635   β€œ cima 5637   ∘ ccom 5638  Ord word 6317  Oncon0 6318  suc csuc 6320  Fun wfun 6491   Fn wfn 6492  βŸΆwf 6493  β€“1-1β†’wf1 6494  β€“1-1-ontoβ†’wf1o 6496  β€˜cfv 6497   Isom wiso 6498  (class class class)co 7358  recscrecs 8317   +o coa 8410   Β·o comu 8411   β‰ˆ cen 8881   β‰Ό cdom 8882  OrdIsocoi 9446  harchar 9493  π‘…1cr1 9699  rankcrnk 9700
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 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-oadd 8417  df-omul 8418  df-er 8649  df-en 8885  df-dom 8886  df-oi 9447  df-har 9494  df-r1 9701  df-rank 9702
This theorem is referenced by:  dfac12lem3  10082
  Copyright terms: Public domain W3C validator