MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac12lem2 Structured version   Visualization version   GIF version
Theorem dfac12lem2 10141
Description: Lemma for dfac12 10146. (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 8399 . . . . . . . . . . . . 13 𝐺 Fn On
3 fnfun 6649 . . . . . . . . . . . . 13 (𝐺 Fn On β†’ Fun 𝐺)
42, 3ax-mp 5 . . . . . . . . . . . 12 Fun 𝐺
5 dfac12.5 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐢 ∈ On)
6 funimaexg 6634 . . . . . . . . . . . 12 ((Fun 𝐺 ∧ 𝐢 ∈ On) β†’ (𝐺 β€œ 𝐢) ∈ V)
74, 5, 6sylancr 587 . . . . . . . . . . 11 (πœ‘ β†’ (𝐺 β€œ 𝐢) ∈ V)
8 uniexg 7732 . . . . . . . . . . 11 ((𝐺 β€œ 𝐢) ∈ V β†’ βˆͺ (𝐺 β€œ 𝐢) ∈ V)
9 rnexg 7897 . . . . . . . . . . 11 (βˆͺ (𝐺 β€œ 𝐢) ∈ V β†’ ran βˆͺ (𝐺 β€œ 𝐢) ∈ V)
107, 8, 93syl 18 . . . . . . . . . 10 (πœ‘ β†’ ran βˆͺ (𝐺 β€œ 𝐢) ∈ V)
11 dfac12.8 . . . . . . . . . . . . . . 15 (πœ‘ β†’ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On)
12 f1f 6787 . . . . . . . . . . . . . . . . 17 ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On β†’ (πΊβ€˜π‘§):(𝑅1β€˜π‘§)⟢On)
13 fssxp 6745 . . . . . . . . . . . . . . . . 17 ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)⟢On β†’ (πΊβ€˜π‘§) βŠ† ((𝑅1β€˜π‘§) Γ— On))
14 ssv 4006 . . . . . . . . . . . . . . . . . . . 20 (𝑅1β€˜π‘§) βŠ† V
15 xpss1 5695 . . . . . . . . . . . . . . . . . . . 20 ((𝑅1β€˜π‘§) βŠ† V β†’ ((𝑅1β€˜π‘§) Γ— On) βŠ† (V Γ— On))
1614, 15ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑅1β€˜π‘§) Γ— On) βŠ† (V Γ— On)
17 sstr 3990 . . . . . . . . . . . . . . . . . . 19 (((πΊβ€˜π‘§) βŠ† ((𝑅1β€˜π‘§) Γ— On) ∧ ((𝑅1β€˜π‘§) Γ— On) βŠ† (V Γ— On)) β†’ (πΊβ€˜π‘§) βŠ† (V Γ— On))
1816, 17mpan2 689 . . . . . . . . . . . . . . . . . 18 ((πΊβ€˜π‘§) βŠ† ((𝑅1β€˜π‘§) Γ— On) β†’ (πΊβ€˜π‘§) βŠ† (V Γ— On))
19 fvex 6904 . . . . . . . . . . . . . . . . . . 19 (πΊβ€˜π‘§) ∈ V
2019elpw 4606 . . . . . . . . . . . . . . . . . 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 3083 . . . . . . . . . . . . . . 15 (βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On β†’ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§) ∈ 𝒫 (V Γ— On))
2411, 23syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§) ∈ 𝒫 (V Γ— On))
25 onss 7774 . . . . . . . . . . . . . . . . 17 (𝐢 ∈ On β†’ 𝐢 βŠ† On)
265, 25syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐢 βŠ† On)
272fndmi 6653 . . . . . . . . . . . . . . . 16 dom 𝐺 = On
2826, 27sseqtrrdi 4033 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐢 βŠ† dom 𝐺)
29 funimass4 6956 . . . . . . . . . . . . . . 15 ((Fun 𝐺 ∧ 𝐢 βŠ† dom 𝐺) β†’ ((𝐺 β€œ 𝐢) βŠ† 𝒫 (V Γ— On) ↔ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§) ∈ 𝒫 (V Γ— On)))
304, 28, 29sylancr 587 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝐺 β€œ 𝐢) βŠ† 𝒫 (V Γ— On) ↔ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§) ∈ 𝒫 (V Γ— On)))
3124, 30mpbird 256 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐺 β€œ 𝐢) βŠ† 𝒫 (V Γ— On))
32 sspwuni 5103 . . . . . . . . . . . . 13 ((𝐺 β€œ 𝐢) βŠ† 𝒫 (V Γ— On) ↔ βˆͺ (𝐺 β€œ 𝐢) βŠ† (V Γ— On))
3331, 32sylib 217 . . . . . . . . . . . 12 (πœ‘ β†’ βˆͺ (𝐺 β€œ 𝐢) βŠ† (V Γ— On))
34 rnss 5938 . . . . . . . . . . . 12 (βˆͺ (𝐺 β€œ 𝐢) βŠ† (V Γ— On) β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† ran (V Γ— On))
3533, 34syl 17 . . . . . . . . . . 11 (πœ‘ β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† ran (V Γ— On))
36 rnxpss 6171 . . . . . . . . . . 11 ran (V Γ— On) βŠ† On
3735, 36sstrdi 3994 . . . . . . . . . 10 (πœ‘ β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† On)
38 ssonuni 7769 . . . . . . . . . 10 (ran βˆͺ (𝐺 β€œ 𝐢) ∈ V β†’ (ran βˆͺ (𝐺 β€œ 𝐢) βŠ† On β†’ βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On))
3910, 37, 38sylc 65 . . . . . . . . 9 (πœ‘ β†’ βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
40 onsuc 7801 . . . . . . . . 9 (βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
4139, 40syl 17 . . . . . . . 8 (πœ‘ β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
4241ad2antrr 724 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
43 rankon 9792 . . . . . . 7 (rankβ€˜π‘¦) ∈ On
44 omcl 8538 . . . . . . 7 ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On ∧ (rankβ€˜π‘¦) ∈ On) β†’ (suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) ∈ On)
4542, 43, 44sylancl 586 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) ∈ On)
46 fveq2 6891 . . . . . . . . . . 11 (𝑧 = suc (rankβ€˜π‘¦) β†’ (πΊβ€˜π‘§) = (πΊβ€˜suc (rankβ€˜π‘¦)))
47 f1eq1 6782 . . . . . . . . . . 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 6891 . . . . . . . . . . 11 (𝑧 = suc (rankβ€˜π‘¦) β†’ (𝑅1β€˜π‘§) = (𝑅1β€˜suc (rankβ€˜π‘¦)))
50 f1eq2 6783 . . . . . . . . . . 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 278 . . . . . . . . 9 (𝑧 = suc (rankβ€˜π‘¦) β†’ ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On ↔ (πΊβ€˜suc (rankβ€˜π‘¦)):(𝑅1β€˜suc (rankβ€˜π‘¦))–1-1β†’On))
5311ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On)
54 rankr1ai 9795 . . . . . . . . . . . 12 (𝑦 ∈ (𝑅1β€˜πΆ) β†’ (rankβ€˜π‘¦) ∈ 𝐢)
5554ad2antlr 725 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (rankβ€˜π‘¦) ∈ 𝐢)
56 simpr 485 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 = βˆͺ 𝐢)
5755, 56eleqtrd 2835 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (rankβ€˜π‘¦) ∈ βˆͺ 𝐢)
58 eloni 6374 . . . . . . . . . . . . 13 (𝐢 ∈ On β†’ Ord 𝐢)
595, 58syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ Ord 𝐢)
6059ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ Ord 𝐢)
61 ordsucuniel 7814 . . . . . . . . . . 11 (Ord 𝐢 β†’ ((rankβ€˜π‘¦) ∈ βˆͺ 𝐢 ↔ suc (rankβ€˜π‘¦) ∈ 𝐢))
6260, 61syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((rankβ€˜π‘¦) ∈ βˆͺ 𝐢 ↔ suc (rankβ€˜π‘¦) ∈ 𝐢))
6357, 62mpbid 231 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ suc (rankβ€˜π‘¦) ∈ 𝐢)
6452, 53, 63rspcdva 3613 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)):(𝑅1β€˜suc (rankβ€˜π‘¦))–1-1β†’On)
65 f1f 6787 . . . . . . . 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 9793 . . . . . . . . 9 (𝑦 ∈ (𝑅1β€˜πΆ) β†’ 𝑦 ∈ βˆͺ (𝑅1 β€œ On))
6867ad2antlr 725 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 ∈ βˆͺ (𝑅1 β€œ On))
69 rankidb 9797 . . . . . . . 8 (𝑦 ∈ βˆͺ (𝑅1 β€œ On) β†’ 𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))
7068, 69syl 17 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))
7166, 70ffvelcdmd 7087 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ On)
72 oacl 8537 . . . . . 6 (((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) ∈ On ∧ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ On) β†’ ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)) ∈ On)
7345, 71, 72syl2anc 584 . . . . 5 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)) ∈ On)
74 dfac12.3 . . . . . . . 8 (πœ‘ β†’ 𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))–1-1β†’On)
75 f1f 6787 . . . . . . . 8 (𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))–1-1β†’On β†’ 𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))⟢On)
7674, 75syl 17 . . . . . . 7 (πœ‘ β†’ 𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))⟢On)
7776ad2antrr 724 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))⟢On)
78 imassrn 6070 . . . . . . . 8 (𝐻 β€œ 𝑦) βŠ† ran 𝐻
79 fvex 6904 . . . . . . . . . . . . . . 15 (πΊβ€˜βˆͺ 𝐢) ∈ V
8079rnex 7905 . . . . . . . . . . . . . 14 ran (πΊβ€˜βˆͺ 𝐢) ∈ V
81 fveq2 6891 . . . . . . . . . . . . . . . . . . 19 (𝑧 = βˆͺ 𝐢 β†’ (πΊβ€˜π‘§) = (πΊβ€˜βˆͺ 𝐢))
82 f1eq1 6782 . . . . . . . . . . . . . . . . . . 19 ((πΊβ€˜π‘§) = (πΊβ€˜βˆͺ 𝐢) β†’ ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On ↔ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜π‘§)–1-1β†’On))
8381, 82syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧 = βˆͺ 𝐢 β†’ ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On ↔ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜π‘§)–1-1β†’On))
84 fveq2 6891 . . . . . . . . . . . . . . . . . . 19 (𝑧 = βˆͺ 𝐢 β†’ (𝑅1β€˜π‘§) = (𝑅1β€˜βˆͺ 𝐢))
85 f1eq2 6783 . . . . . . . . . . . . . . . . . . 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 278 . . . . . . . . . . . . . . . . 17 (𝑧 = βˆͺ 𝐢 β†’ ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On ↔ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’On))
8811ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On)
895ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 ∈ On)
90 onuni 7778 . . . . . . . . . . . . . . . . . . 19 (𝐢 ∈ On β†’ βˆͺ 𝐢 ∈ On)
91 sucidg 6445 . . . . . . . . . . . . . . . . . . 19 (βˆͺ 𝐢 ∈ On β†’ βˆͺ 𝐢 ∈ suc βˆͺ 𝐢)
9289, 90, 913syl 18 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ suc βˆͺ 𝐢)
9359adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) β†’ Ord 𝐢)
94 orduniorsuc 7820 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝐢 β†’ (𝐢 = βˆͺ 𝐢 ∨ 𝐢 = suc βˆͺ 𝐢))
9593, 94syl 17 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) β†’ (𝐢 = βˆͺ 𝐢 ∨ 𝐢 = suc βˆͺ 𝐢))
9695orcanai 1001 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 = suc βˆͺ 𝐢)
9792, 96eleqtrrd 2836 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ 𝐢)
9887, 88, 97rspcdva 3613 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’On)
99 f1f 6787 . . . . . . . . . . . . . . . 16 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’On β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)⟢On)
100 frn 6724 . . . . . . . . . . . . . . . 16 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)⟢On β†’ ran (πΊβ€˜βˆͺ 𝐢) βŠ† On)
10198, 99, 1003syl 18 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran (πΊβ€˜βˆͺ 𝐢) βŠ† On)
102 epweon 7764 . . . . . . . . . . . . . . 15 E We On
103 wess 5663 . . . . . . . . . . . . . . 15 (ran (πΊβ€˜βˆͺ 𝐢) βŠ† On β†’ ( E We On β†’ E We ran (πΊβ€˜βˆͺ 𝐢)))
104101, 102, 103mpisyl 21 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ E We ran (πΊβ€˜βˆͺ 𝐢))
105 eqid 2732 . . . . . . . . . . . . . . 15 OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) = OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢))
106105oiiso 9534 . . . . . . . . . . . . . 14 ((ran (πΊβ€˜βˆͺ 𝐢) ∈ V ∧ E We ran (πΊβ€˜βˆͺ 𝐢)) β†’ OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) Isom E , E (dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)), ran (πΊβ€˜βˆͺ 𝐢)))
10780, 104, 106sylancr 587 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) Isom E , E (dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)), ran (πΊβ€˜βˆͺ 𝐢)))
108 isof1o 7322 . . . . . . . . . . . . 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 6845 . . . . . . . . . . . . 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 6832 . . . . . . . . . . . . 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 6844 . . . . . . . . . . . . 13 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’On β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1-ontoβ†’ran (πΊβ€˜βˆͺ 𝐢))
113 f1of1 6832 . . . . . . . . . . . . 13 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1-ontoβ†’ran (πΊβ€˜βˆͺ 𝐢) β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’ran (πΊβ€˜βˆͺ 𝐢))
11498, 112, 1133syl 18 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’ran (πΊβ€˜βˆͺ 𝐢))
115 f1co 6799 . . . . . . . . . . . 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 584 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (β—‘OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∘ (πΊβ€˜βˆͺ 𝐢)):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)))
117 dfac12.h . . . . . . . . . . . 12 𝐻 = (β—‘OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∘ (πΊβ€˜βˆͺ 𝐢))
118 f1eq1 6782 . . . . . . . . . . . 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 6787 . . . . . . . . . 10 (𝐻:(𝑅1β€˜βˆͺ 𝐢)–1-1β†’dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β†’ 𝐻:(𝑅1β€˜βˆͺ 𝐢)⟢dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)))
122 frn 6724 . . . . . . . . . 10 (𝐻:(𝑅1β€˜βˆͺ 𝐢)⟢dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β†’ ran 𝐻 βŠ† dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)))
123120, 121, 1223syl 18 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran 𝐻 βŠ† dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)))
124 harcl 9556 . . . . . . . . . . 11 (harβ€˜(𝑅1β€˜π΄)) ∈ On
125124onordi 6475 . . . . . . . . . 10 Ord (harβ€˜(𝑅1β€˜π΄))
126105oion 9533 . . . . . . . . . . . 12 (ran (πΊβ€˜βˆͺ 𝐢) ∈ V β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ On)
12780, 126mp1i 13 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ On)
128105oien 9535 . . . . . . . . . . . . 13 ((ran (πΊβ€˜βˆͺ 𝐢) ∈ V ∧ E We ran (πΊβ€˜βˆͺ 𝐢)) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢))
12980, 104, 128sylancr 587 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢))
130 fvex 6904 . . . . . . . . . . . . . . 15 (𝑅1β€˜βˆͺ 𝐢) ∈ V
131130f1oen 8971 . . . . . . . . . . . . . 14 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1-ontoβ†’ran (πΊβ€˜βˆͺ 𝐢) β†’ (𝑅1β€˜βˆͺ 𝐢) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢))
132 ensym 9001 . . . . . . . . . . . . . 14 ((𝑅1β€˜βˆͺ 𝐢) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢) β†’ ran (πΊβ€˜βˆͺ 𝐢) β‰ˆ (𝑅1β€˜βˆͺ 𝐢))
13398, 112, 131, 1324syl 19 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran (πΊβ€˜βˆͺ 𝐢) β‰ˆ (𝑅1β€˜βˆͺ 𝐢))
134 fvex 6904 . . . . . . . . . . . . . 14 (𝑅1β€˜π΄) ∈ V
135 dfac12.1 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐴 ∈ On)
136135ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐴 ∈ On)
137 dfac12.6 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐢 βŠ† 𝐴)
138137ad2antrr 724 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 βŠ† 𝐴)
139138, 97sseldd 3983 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ 𝐴)
140 r1ord2 9778 . . . . . . . . . . . . . . 15 (𝐴 ∈ On β†’ (βˆͺ 𝐢 ∈ 𝐴 β†’ (𝑅1β€˜βˆͺ 𝐢) βŠ† (𝑅1β€˜π΄)))
141136, 139, 140sylc 65 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜βˆͺ 𝐢) βŠ† (𝑅1β€˜π΄))
142 ssdomg 8998 . . . . . . . . . . . . . 14 ((𝑅1β€˜π΄) ∈ V β†’ ((𝑅1β€˜βˆͺ 𝐢) βŠ† (𝑅1β€˜π΄) β†’ (𝑅1β€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄)))
143134, 141, 142mpsyl 68 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄))
144 endomtr 9010 . . . . . . . . . . . . 13 ((ran (πΊβ€˜βˆͺ 𝐢) β‰ˆ (𝑅1β€˜βˆͺ 𝐢) ∧ (𝑅1β€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄)) β†’ ran (πΊβ€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄))
145133, 143, 144syl2anc 584 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran (πΊβ€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄))
146 endomtr 9010 . . . . . . . . . . . 12 ((dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢) ∧ ran (πΊβ€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄)) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰Ό (𝑅1β€˜π΄))
147129, 145, 146syl2anc 584 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰Ό (𝑅1β€˜π΄))
148 elharval 9558 . . . . . . . . . . 11 (dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ (harβ€˜(𝑅1β€˜π΄)) ↔ (dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ On ∧ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰Ό (𝑅1β€˜π΄)))
149127, 147, 148sylanbrc 583 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ (harβ€˜(𝑅1β€˜π΄)))
150 ordelss 6380 . . . . . . . . . 10 ((Ord (harβ€˜(𝑅1β€˜π΄)) ∧ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ (harβ€˜(𝑅1β€˜π΄))) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) βŠ† (harβ€˜(𝑅1β€˜π΄)))
151125, 149, 150sylancr 587 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) βŠ† (harβ€˜(𝑅1β€˜π΄)))
152123, 151sstrd 3992 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran 𝐻 βŠ† (harβ€˜(𝑅1β€˜π΄)))
15378, 152sstrid 3993 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑦) βŠ† (harβ€˜(𝑅1β€˜π΄)))
154 fvex 6904 . . . . . . . 8 (harβ€˜(𝑅1β€˜π΄)) ∈ V
155154elpw2 5345 . . . . . . 7 ((𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)) ↔ (𝐻 β€œ 𝑦) βŠ† (harβ€˜(𝑅1β€˜π΄)))
156153, 155sylibr 233 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)))
15777, 156ffvelcdmd 7087 . . . . 5 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (πΉβ€˜(𝐻 β€œ 𝑦)) ∈ On)
15873, 157ifclda 4563 . . . 4 ((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) ∈ On)
159158ex 413 . . 3 (πœ‘ β†’ (𝑦 ∈ (𝑅1β€˜πΆ) β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) ∈ On))
160 iftrue 4534 . . . . . . . 8 (𝐢 = βˆͺ 𝐢 β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)))
161 iftrue 4534 . . . . . . . 8 (𝐢 = βˆͺ 𝐢 β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) = ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)))
162160, 161eqeq12d 2748 . . . . . . 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 482 . . . . . 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 724 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
165 nsuceq0 6447 . . . . . . . 8 suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) β‰  βˆ…
166165a1i 11 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) β‰  βˆ…)
16743a1i 11 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (rankβ€˜π‘¦) ∈ On)
168 onsucuni 7818 . . . . . . . . . . 11 (ran βˆͺ (𝐺 β€œ 𝐢) βŠ† On β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
16937, 168syl 17 . . . . . . . . . 10 (πœ‘ β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
170169ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
17126ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 βŠ† On)
172 fnfvima 7237 . . . . . . . . . . . 12 ((𝐺 Fn On ∧ 𝐢 βŠ† On ∧ suc (rankβ€˜π‘¦) ∈ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) ∈ (𝐺 β€œ 𝐢))
1732, 171, 63, 172mp3an2i 1466 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) ∈ (𝐺 β€œ 𝐢))
174 elssuni 4941 . . . . . . . . . . 11 ((πΊβ€˜suc (rankβ€˜π‘¦)) ∈ (𝐺 β€œ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) βŠ† βˆͺ (𝐺 β€œ 𝐢))
175 rnss 5938 . . . . . . . . . . 11 ((πΊβ€˜suc (rankβ€˜π‘¦)) βŠ† βˆͺ (𝐺 β€œ 𝐢) β†’ ran (πΊβ€˜suc (rankβ€˜π‘¦)) βŠ† ran βˆͺ (𝐺 β€œ 𝐢))
176173, 174, 1753syl 18 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ran (πΊβ€˜suc (rankβ€˜π‘¦)) βŠ† ran βˆͺ (𝐺 β€œ 𝐢))
177 f1fn 6788 . . . . . . . . . . . 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 7082 . . . . . . . . . . 11 (((πΊβ€˜suc (rankβ€˜π‘¦)) Fn (𝑅1β€˜suc (rankβ€˜π‘¦)) ∧ 𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦))) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ ran (πΊβ€˜suc (rankβ€˜π‘¦)))
180178, 70, 179syl2anc 584 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ ran (πΊβ€˜suc (rankβ€˜π‘¦)))
181176, 180sseldd 3983 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ ran βˆͺ (𝐺 β€œ 𝐢))
182170, 181sseldd 3983 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
183182adantlrr 719 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
184 rankon 9792 . . . . . . . 8 (rankβ€˜π‘§) ∈ On
185184a1i 11 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (rankβ€˜π‘§) ∈ On)
186 eleq1w 2816 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ (𝑦 ∈ (𝑅1β€˜πΆ) ↔ 𝑧 ∈ (𝑅1β€˜πΆ)))
187186anbi2d 629 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ ((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ↔ (πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ))))
188187anbi1d 630 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) ↔ ((πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢)))
189 fveq2 6891 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 β†’ (rankβ€˜π‘¦) = (rankβ€˜π‘§))
190 suceq 6430 . . . . . . . . . . . . . 14 ((rankβ€˜π‘¦) = (rankβ€˜π‘§) β†’ suc (rankβ€˜π‘¦) = suc (rankβ€˜π‘§))
191189, 190syl 17 . . . . . . . . . . . . 13 (𝑦 = 𝑧 β†’ suc (rankβ€˜π‘¦) = suc (rankβ€˜π‘§))
192191fveq2d 6895 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) = (πΊβ€˜suc (rankβ€˜π‘§)))
193 id 22 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ 𝑦 = 𝑧)
194192, 193fveq12d 6898 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§))
195194eleq1d 2818 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ (((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ↔ ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢)))
196188, 195imbi12d 344 . . . . . . . . 9 (𝑦 = 𝑧 β†’ ((((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢)) ↔ (((πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))))
197196, 182chvarvv 2002 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
198197adantlrl 718 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
199 omopth2 8586 . . . . . . 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 1386 . . . . . 6 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)) = ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)) ↔ ((rankβ€˜π‘¦) = (rankβ€˜π‘§) ∧ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§))))
201190adantl 482 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ suc (rankβ€˜π‘¦) = suc (rankβ€˜π‘§))
202201fveq2d 6895 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) = (πΊβ€˜suc (rankβ€˜π‘§)))
203202fveq1d 6893 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘§) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§))
204203eqeq2d 2743 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ (((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘§) ↔ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)))
20564adantlrr 719 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)):(𝑅1β€˜suc (rankβ€˜π‘¦))–1-1β†’On)
206205adantr 481 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)):(𝑅1β€˜suc (rankβ€˜π‘¦))–1-1β†’On)
20770adantlrr 719 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))
208207adantr 481 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ 𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))
209 r1elwf 9793 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑅1β€˜πΆ) β†’ 𝑧 ∈ βˆͺ (𝑅1 β€œ On))
210 rankidb 9797 . . . . . . . . . . . . . . 15 (𝑧 ∈ βˆͺ (𝑅1 β€œ On) β†’ 𝑧 ∈ (𝑅1β€˜suc (rankβ€˜π‘§)))
211209, 210syl 17 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑅1β€˜πΆ) β†’ 𝑧 ∈ (𝑅1β€˜suc (rankβ€˜π‘§)))
212211ad2antll 727 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) β†’ 𝑧 ∈ (𝑅1β€˜suc (rankβ€˜π‘§)))
213212ad2antrr 724 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ 𝑧 ∈ (𝑅1β€˜suc (rankβ€˜π‘§)))
214201fveq2d 6895 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ (𝑅1β€˜suc (rankβ€˜π‘¦)) = (𝑅1β€˜suc (rankβ€˜π‘§)))
215213, 214eleqtrrd 2836 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ 𝑧 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))
216 f1fveq 7263 . . . . . . . . . . 11 (((πΊβ€˜suc (rankβ€˜π‘¦)):(𝑅1β€˜suc (rankβ€˜π‘¦))–1-1β†’On ∧ (𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)) ∧ 𝑧 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))) β†’ (((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘§) ↔ 𝑦 = 𝑧))
217206, 208, 215, 216syl12anc 835 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ (((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘§) ↔ 𝑦 = 𝑧))
218204, 217bitr3d 280 . . . . . . . . 9 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ (((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§) ↔ 𝑦 = 𝑧))
219218biimpd 228 . . . . . . . 8 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ (((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§) β†’ 𝑦 = 𝑧))
220219expimpd 454 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (((rankβ€˜π‘¦) = (rankβ€˜π‘§) ∧ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)) β†’ 𝑦 = 𝑧))
221189, 194jca 512 . . . . . . 7 (𝑦 = 𝑧 β†’ ((rankβ€˜π‘¦) = (rankβ€˜π‘§) ∧ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)))
222220, 221impbid1 224 . . . . . 6 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (((rankβ€˜π‘¦) = (rankβ€˜π‘§) ∧ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)) ↔ 𝑦 = 𝑧))
223163, 200, 2223bitrd 304 . . . . 5 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) ↔ 𝑦 = 𝑧))
224 iffalse 4537 . . . . . . . 8 (Β¬ 𝐢 = βˆͺ 𝐢 β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = (πΉβ€˜(𝐻 β€œ 𝑦)))
225 iffalse 4537 . . . . . . . 8 (Β¬ 𝐢 = βˆͺ 𝐢 β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) = (πΉβ€˜(𝐻 β€œ 𝑧)))
226224, 225eqeq12d 2748 . . . . . . 7 (Β¬ 𝐢 = βˆͺ 𝐢 β†’ (if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) ↔ (πΉβ€˜(𝐻 β€œ 𝑦)) = (πΉβ€˜(𝐻 β€œ 𝑧))))
227226adantl 482 . . . . . 6 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) ↔ (πΉβ€˜(𝐻 β€œ 𝑦)) = (πΉβ€˜(𝐻 β€œ 𝑧))))
22874ad2antrr 724 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))–1-1β†’On)
229156adantlrr 719 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)))
230187anbi1d 630 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) ↔ ((πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢)))
231 imaeq2 6055 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ (𝐻 β€œ 𝑦) = (𝐻 β€œ 𝑧))
232231eleq1d 2818 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ ((𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)) ↔ (𝐻 β€œ 𝑧) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄))))
233230, 232imbi12d 344 . . . . . . . . 9 (𝑦 = 𝑧 β†’ ((((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄))) ↔ (((πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑧) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)))))
234233, 156chvarvv 2002 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑧) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)))
235234adantlrl 718 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑧) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)))
236 f1fveq 7263 . . . . . . 7 ((𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))–1-1β†’On ∧ ((𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)) ∧ (𝐻 β€œ 𝑧) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)))) β†’ ((πΉβ€˜(𝐻 β€œ 𝑦)) = (πΉβ€˜(𝐻 β€œ 𝑧)) ↔ (𝐻 β€œ 𝑦) = (𝐻 β€œ 𝑧)))
237228, 229, 235, 236syl12anc 835 . . . . . 6 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ((πΉβ€˜(𝐻 β€œ 𝑦)) = (πΉβ€˜(𝐻 β€œ 𝑧)) ↔ (𝐻 β€œ 𝑦) = (𝐻 β€œ 𝑧)))
238120adantlrr 719 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐻:(𝑅1β€˜βˆͺ 𝐢)–1-1β†’dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)))
239 simplrl 775 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 ∈ (𝑅1β€˜πΆ))
24096fveq2d 6895 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜πΆ) = (𝑅1β€˜suc βˆͺ 𝐢))
241 r1suc 9767 . . . . . . . . . . . 12 (βˆͺ 𝐢 ∈ On β†’ (𝑅1β€˜suc βˆͺ 𝐢) = 𝒫 (𝑅1β€˜βˆͺ 𝐢))
24289, 90, 2413syl 18 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜suc βˆͺ 𝐢) = 𝒫 (𝑅1β€˜βˆͺ 𝐢))
243240, 242eqtrd 2772 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜πΆ) = 𝒫 (𝑅1β€˜βˆͺ 𝐢))
244243adantlrr 719 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜πΆ) = 𝒫 (𝑅1β€˜βˆͺ 𝐢))
245239, 244eleqtrd 2835 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 ∈ 𝒫 (𝑅1β€˜βˆͺ 𝐢))
246245elpwid 4611 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 βŠ† (𝑅1β€˜βˆͺ 𝐢))
247 simplrr 776 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑧 ∈ (𝑅1β€˜πΆ))
248247, 244eleqtrd 2835 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑧 ∈ 𝒫 (𝑅1β€˜βˆͺ 𝐢))
249248elpwid 4611 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑧 βŠ† (𝑅1β€˜βˆͺ 𝐢))
250 f1imaeq 7266 . . . . . . 7 ((𝐻:(𝑅1β€˜βˆͺ 𝐢)–1-1β†’dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∧ (𝑦 βŠ† (𝑅1β€˜βˆͺ 𝐢) ∧ 𝑧 βŠ† (𝑅1β€˜βˆͺ 𝐢))) β†’ ((𝐻 β€œ 𝑦) = (𝐻 β€œ 𝑧) ↔ 𝑦 = 𝑧))
251238, 246, 249, 250syl12anc 835 . . . . . 6 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ((𝐻 β€œ 𝑦) = (𝐻 β€œ 𝑧) ↔ 𝑦 = 𝑧))
252227, 237, 2513bitrd 304 . . . . 5 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) ↔ 𝑦 = 𝑧))
253223, 252pm2.61dan 811 . . . 4 ((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) β†’ (if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) ↔ 𝑦 = 𝑧))
254253ex 413 . . 3 (πœ‘ β†’ ((𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) β†’ (if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) ↔ 𝑦 = 𝑧)))
255159, 254dom2lem 8990 . 2 (πœ‘ β†’ (𝑦 ∈ (𝑅1β€˜πΆ) ↦ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦)))):(𝑅1β€˜πΆ)–1-1β†’On)
256135, 74, 1, 5, 117dfac12lem1 10140 . . 3 (πœ‘ β†’ (πΊβ€˜πΆ) = (𝑦 ∈ (𝑅1β€˜πΆ) ↦ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦)))))
257 f1eq1 6782 . . 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 256 1 (πœ‘ β†’ (πΊβ€˜πΆ):(𝑅1β€˜πΆ)–1-1β†’On)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  Vcvv 3474   βŠ† wss 3948  βˆ…c0 4322  ifcif 4528  π’« cpw 4602  βˆͺ cuni 4908   class class class wbr 5148   ↦ cmpt 5231   E cep 5579   We wwe 5630   Γ— cxp 5674  β—‘ccnv 5675  dom cdm 5676  ran crn 5677   β€œ cima 5679   ∘ ccom 5680  Ord word 6363  Oncon0 6364  suc csuc 6366  Fun wfun 6537   Fn wfn 6538  βŸΆwf 6539  β€“1-1β†’wf1 6540  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543   Isom wiso 6544  (class class class)co 7411  recscrecs 8372   +o coa 8465   Β·o comu 8466   β‰ˆ cen 8938   β‰Ό cdom 8939  OrdIsocoi 9506  harchar 9553  π‘…1cr1 9759  rankcrnk 9760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-oadd 8472  df-omul 8473  df-er 8705  df-en 8942  df-dom 8943  df-oi 9507  df-har 9554  df-r1 9761  df-rank 9762
This theorem is referenced by:  dfac12lem3  10142
  Copyright terms: Public domain W3C validator