MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac12lem2 Structured version   Visualization version   GIF version
Theorem dfac12lem2 10142
Description: Lemma for dfac12 10147. (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 8400 . . . . . . . . . . . . 13 𝐺 Fn On
3 fnfun 6650 . . . . . . . . . . . . 13 (𝐺 Fn On β†’ Fun 𝐺)
42, 3ax-mp 5 . . . . . . . . . . . 12 Fun 𝐺
5 dfac12.5 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐢 ∈ On)
6 funimaexg 6635 . . . . . . . . . . . 12 ((Fun 𝐺 ∧ 𝐢 ∈ On) β†’ (𝐺 β€œ 𝐢) ∈ V)
74, 5, 6sylancr 586 . . . . . . . . . . 11 (πœ‘ β†’ (𝐺 β€œ 𝐢) ∈ V)
8 uniexg 7733 . . . . . . . . . . 11 ((𝐺 β€œ 𝐢) ∈ V β†’ βˆͺ (𝐺 β€œ 𝐢) ∈ V)
9 rnexg 7898 . . . . . . . . . . 11 (βˆͺ (𝐺 β€œ 𝐢) ∈ V β†’ ran βˆͺ (𝐺 β€œ 𝐢) ∈ V)
107, 8, 93syl 18 . . . . . . . . . 10 (πœ‘ β†’ ran βˆͺ (𝐺 β€œ 𝐢) ∈ V)
11 dfac12.8 . . . . . . . . . . . . . . 15 (πœ‘ β†’ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On)
12 f1f 6788 . . . . . . . . . . . . . . . . 17 ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On β†’ (πΊβ€˜π‘§):(𝑅1β€˜π‘§)⟢On)
13 fssxp 6746 . . . . . . . . . . . . . . . . 17 ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)⟢On β†’ (πΊβ€˜π‘§) βŠ† ((𝑅1β€˜π‘§) Γ— On))
14 ssv 4007 . . . . . . . . . . . . . . . . . . . 20 (𝑅1β€˜π‘§) βŠ† V
15 xpss1 5696 . . . . . . . . . . . . . . . . . . . 20 ((𝑅1β€˜π‘§) βŠ† V β†’ ((𝑅1β€˜π‘§) Γ— On) βŠ† (V Γ— On))
1614, 15ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑅1β€˜π‘§) Γ— On) βŠ† (V Γ— On)
17 sstr 3991 . . . . . . . . . . . . . . . . . . 19 (((πΊβ€˜π‘§) βŠ† ((𝑅1β€˜π‘§) Γ— On) ∧ ((𝑅1β€˜π‘§) Γ— On) βŠ† (V Γ— On)) β†’ (πΊβ€˜π‘§) βŠ† (V Γ— On))
1816, 17mpan2 688 . . . . . . . . . . . . . . . . . 18 ((πΊβ€˜π‘§) βŠ† ((𝑅1β€˜π‘§) Γ— On) β†’ (πΊβ€˜π‘§) βŠ† (V Γ— On))
19 fvex 6905 . . . . . . . . . . . . . . . . . . 19 (πΊβ€˜π‘§) ∈ V
2019elpw 4607 . . . . . . . . . . . . . . . . . 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 3082 . . . . . . . . . . . . . . 15 (βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On β†’ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§) ∈ 𝒫 (V Γ— On))
2411, 23syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§) ∈ 𝒫 (V Γ— On))
25 onss 7775 . . . . . . . . . . . . . . . . 17 (𝐢 ∈ On β†’ 𝐢 βŠ† On)
265, 25syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐢 βŠ† On)
272fndmi 6654 . . . . . . . . . . . . . . . 16 dom 𝐺 = On
2826, 27sseqtrrdi 4034 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐢 βŠ† dom 𝐺)
29 funimass4 6957 . . . . . . . . . . . . . . 15 ((Fun 𝐺 ∧ 𝐢 βŠ† dom 𝐺) β†’ ((𝐺 β€œ 𝐢) βŠ† 𝒫 (V Γ— On) ↔ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§) ∈ 𝒫 (V Γ— On)))
304, 28, 29sylancr 586 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝐺 β€œ 𝐢) βŠ† 𝒫 (V Γ— On) ↔ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§) ∈ 𝒫 (V Γ— On)))
3124, 30mpbird 256 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐺 β€œ 𝐢) βŠ† 𝒫 (V Γ— On))
32 sspwuni 5104 . . . . . . . . . . . . 13 ((𝐺 β€œ 𝐢) βŠ† 𝒫 (V Γ— On) ↔ βˆͺ (𝐺 β€œ 𝐢) βŠ† (V Γ— On))
3331, 32sylib 217 . . . . . . . . . . . 12 (πœ‘ β†’ βˆͺ (𝐺 β€œ 𝐢) βŠ† (V Γ— On))
34 rnss 5939 . . . . . . . . . . . 12 (βˆͺ (𝐺 β€œ 𝐢) βŠ† (V Γ— On) β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† ran (V Γ— On))
3533, 34syl 17 . . . . . . . . . . 11 (πœ‘ β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† ran (V Γ— On))
36 rnxpss 6172 . . . . . . . . . . 11 ran (V Γ— On) βŠ† On
3735, 36sstrdi 3995 . . . . . . . . . 10 (πœ‘ β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† On)
38 ssonuni 7770 . . . . . . . . . 10 (ran βˆͺ (𝐺 β€œ 𝐢) ∈ V β†’ (ran βˆͺ (𝐺 β€œ 𝐢) βŠ† On β†’ βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On))
3910, 37, 38sylc 65 . . . . . . . . 9 (πœ‘ β†’ βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
40 onsuc 7802 . . . . . . . . 9 (βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
4139, 40syl 17 . . . . . . . 8 (πœ‘ β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
4241ad2antrr 723 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
43 rankon 9793 . . . . . . 7 (rankβ€˜π‘¦) ∈ On
44 omcl 8539 . . . . . . 7 ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On ∧ (rankβ€˜π‘¦) ∈ On) β†’ (suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) ∈ On)
4542, 43, 44sylancl 585 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) ∈ On)
46 fveq2 6892 . . . . . . . . . . 11 (𝑧 = suc (rankβ€˜π‘¦) β†’ (πΊβ€˜π‘§) = (πΊβ€˜suc (rankβ€˜π‘¦)))
47 f1eq1 6783 . . . . . . . . . . 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 6892 . . . . . . . . . . 11 (𝑧 = suc (rankβ€˜π‘¦) β†’ (𝑅1β€˜π‘§) = (𝑅1β€˜suc (rankβ€˜π‘¦)))
50 f1eq2 6784 . . . . . . . . . . 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 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On)
54 rankr1ai 9796 . . . . . . . . . . . 12 (𝑦 ∈ (𝑅1β€˜πΆ) β†’ (rankβ€˜π‘¦) ∈ 𝐢)
5554ad2antlr 724 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (rankβ€˜π‘¦) ∈ 𝐢)
56 simpr 484 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 = βˆͺ 𝐢)
5755, 56eleqtrd 2834 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (rankβ€˜π‘¦) ∈ βˆͺ 𝐢)
58 eloni 6375 . . . . . . . . . . . . 13 (𝐢 ∈ On β†’ Ord 𝐢)
595, 58syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ Ord 𝐢)
6059ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ Ord 𝐢)
61 ordsucuniel 7815 . . . . . . . . . . 11 (Ord 𝐢 β†’ ((rankβ€˜π‘¦) ∈ βˆͺ 𝐢 ↔ suc (rankβ€˜π‘¦) ∈ 𝐢))
6260, 61syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((rankβ€˜π‘¦) ∈ βˆͺ 𝐢 ↔ suc (rankβ€˜π‘¦) ∈ 𝐢))
6357, 62mpbid 231 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ suc (rankβ€˜π‘¦) ∈ 𝐢)
6452, 53, 63rspcdva 3614 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)):(𝑅1β€˜suc (rankβ€˜π‘¦))–1-1β†’On)
65 f1f 6788 . . . . . . . 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 9794 . . . . . . . . 9 (𝑦 ∈ (𝑅1β€˜πΆ) β†’ 𝑦 ∈ βˆͺ (𝑅1 β€œ On))
6867ad2antlr 724 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 ∈ βˆͺ (𝑅1 β€œ On))
69 rankidb 9798 . . . . . . . 8 (𝑦 ∈ βˆͺ (𝑅1 β€œ On) β†’ 𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))
7068, 69syl 17 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))
7166, 70ffvelcdmd 7088 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ On)
72 oacl 8538 . . . . . 6 (((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) ∈ On ∧ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ On) β†’ ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)) ∈ On)
7345, 71, 72syl2anc 583 . . . . 5 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)) ∈ On)
74 dfac12.3 . . . . . . . 8 (πœ‘ β†’ 𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))–1-1β†’On)
75 f1f 6788 . . . . . . . 8 (𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))–1-1β†’On β†’ 𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))⟢On)
7674, 75syl 17 . . . . . . 7 (πœ‘ β†’ 𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))⟢On)
7776ad2antrr 723 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))⟢On)
78 imassrn 6071 . . . . . . . 8 (𝐻 β€œ 𝑦) βŠ† ran 𝐻
79 fvex 6905 . . . . . . . . . . . . . . 15 (πΊβ€˜βˆͺ 𝐢) ∈ V
8079rnex 7906 . . . . . . . . . . . . . 14 ran (πΊβ€˜βˆͺ 𝐢) ∈ V
81 fveq2 6892 . . . . . . . . . . . . . . . . . . 19 (𝑧 = βˆͺ 𝐢 β†’ (πΊβ€˜π‘§) = (πΊβ€˜βˆͺ 𝐢))
82 f1eq1 6783 . . . . . . . . . . . . . . . . . . 19 ((πΊβ€˜π‘§) = (πΊβ€˜βˆͺ 𝐢) β†’ ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On ↔ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜π‘§)–1-1β†’On))
8381, 82syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧 = βˆͺ 𝐢 β†’ ((πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On ↔ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜π‘§)–1-1β†’On))
84 fveq2 6892 . . . . . . . . . . . . . . . . . . 19 (𝑧 = βˆͺ 𝐢 β†’ (𝑅1β€˜π‘§) = (𝑅1β€˜βˆͺ 𝐢))
85 f1eq2 6784 . . . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆ€π‘§ ∈ 𝐢 (πΊβ€˜π‘§):(𝑅1β€˜π‘§)–1-1β†’On)
895ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 ∈ On)
90 onuni 7779 . . . . . . . . . . . . . . . . . . 19 (𝐢 ∈ On β†’ βˆͺ 𝐢 ∈ On)
91 sucidg 6446 . . . . . . . . . . . . . . . . . . 19 (βˆͺ 𝐢 ∈ On β†’ βˆͺ 𝐢 ∈ suc βˆͺ 𝐢)
9289, 90, 913syl 18 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ suc βˆͺ 𝐢)
9359adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) β†’ Ord 𝐢)
94 orduniorsuc 7821 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝐢 β†’ (𝐢 = βˆͺ 𝐢 ∨ 𝐢 = suc βˆͺ 𝐢))
9593, 94syl 17 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) β†’ (𝐢 = βˆͺ 𝐢 ∨ 𝐢 = suc βˆͺ 𝐢))
9695orcanai 1000 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 = suc βˆͺ 𝐢)
9792, 96eleqtrrd 2835 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ 𝐢)
9887, 88, 97rspcdva 3614 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’On)
99 f1f 6788 . . . . . . . . . . . . . . . 16 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’On β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)⟢On)
100 frn 6725 . . . . . . . . . . . . . . . 16 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)⟢On β†’ ran (πΊβ€˜βˆͺ 𝐢) βŠ† On)
10198, 99, 1003syl 18 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran (πΊβ€˜βˆͺ 𝐢) βŠ† On)
102 epweon 7765 . . . . . . . . . . . . . . 15 E We On
103 wess 5664 . . . . . . . . . . . . . . 15 (ran (πΊβ€˜βˆͺ 𝐢) βŠ† On β†’ ( E We On β†’ E We ran (πΊβ€˜βˆͺ 𝐢)))
104101, 102, 103mpisyl 21 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ E We ran (πΊβ€˜βˆͺ 𝐢))
105 eqid 2731 . . . . . . . . . . . . . . 15 OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) = OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢))
106105oiiso 9535 . . . . . . . . . . . . . 14 ((ran (πΊβ€˜βˆͺ 𝐢) ∈ V ∧ E We ran (πΊβ€˜βˆͺ 𝐢)) β†’ OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) Isom E , E (dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)), ran (πΊβ€˜βˆͺ 𝐢)))
10780, 104, 106sylancr 586 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) Isom E , E (dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)), ran (πΊβ€˜βˆͺ 𝐢)))
108 isof1o 7323 . . . . . . . . . . . . 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 6846 . . . . . . . . . . . . 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 6833 . . . . . . . . . . . . 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 6845 . . . . . . . . . . . . 13 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’On β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1-ontoβ†’ran (πΊβ€˜βˆͺ 𝐢))
113 f1of1 6833 . . . . . . . . . . . . 13 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1-ontoβ†’ran (πΊβ€˜βˆͺ 𝐢) β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’ran (πΊβ€˜βˆͺ 𝐢))
11498, 112, 1133syl 18 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’ran (πΊβ€˜βˆͺ 𝐢))
115 f1co 6800 . . . . . . . . . . . 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 583 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (β—‘OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∘ (πΊβ€˜βˆͺ 𝐢)):(𝑅1β€˜βˆͺ 𝐢)–1-1β†’dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)))
117 dfac12.h . . . . . . . . . . . 12 𝐻 = (β—‘OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∘ (πΊβ€˜βˆͺ 𝐢))
118 f1eq1 6783 . . . . . . . . . . . 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 6788 . . . . . . . . . 10 (𝐻:(𝑅1β€˜βˆͺ 𝐢)–1-1β†’dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β†’ 𝐻:(𝑅1β€˜βˆͺ 𝐢)⟢dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)))
122 frn 6725 . . . . . . . . . 10 (𝐻:(𝑅1β€˜βˆͺ 𝐢)⟢dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β†’ ran 𝐻 βŠ† dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)))
123120, 121, 1223syl 18 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran 𝐻 βŠ† dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)))
124 harcl 9557 . . . . . . . . . . 11 (harβ€˜(𝑅1β€˜π΄)) ∈ On
125124onordi 6476 . . . . . . . . . 10 Ord (harβ€˜(𝑅1β€˜π΄))
126105oion 9534 . . . . . . . . . . . 12 (ran (πΊβ€˜βˆͺ 𝐢) ∈ V β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ On)
12780, 126mp1i 13 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ On)
128105oien 9536 . . . . . . . . . . . . 13 ((ran (πΊβ€˜βˆͺ 𝐢) ∈ V ∧ E We ran (πΊβ€˜βˆͺ 𝐢)) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢))
12980, 104, 128sylancr 586 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢))
130 fvex 6905 . . . . . . . . . . . . . . 15 (𝑅1β€˜βˆͺ 𝐢) ∈ V
131130f1oen 8972 . . . . . . . . . . . . . 14 ((πΊβ€˜βˆͺ 𝐢):(𝑅1β€˜βˆͺ 𝐢)–1-1-ontoβ†’ran (πΊβ€˜βˆͺ 𝐢) β†’ (𝑅1β€˜βˆͺ 𝐢) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢))
132 ensym 9002 . . . . . . . . . . . . . 14 ((𝑅1β€˜βˆͺ 𝐢) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢) β†’ ran (πΊβ€˜βˆͺ 𝐢) β‰ˆ (𝑅1β€˜βˆͺ 𝐢))
13398, 112, 131, 1324syl 19 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran (πΊβ€˜βˆͺ 𝐢) β‰ˆ (𝑅1β€˜βˆͺ 𝐢))
134 fvex 6905 . . . . . . . . . . . . . 14 (𝑅1β€˜π΄) ∈ V
135 dfac12.1 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐴 ∈ On)
136135ad2antrr 723 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐴 ∈ On)
137 dfac12.6 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐢 βŠ† 𝐴)
138137ad2antrr 723 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 βŠ† 𝐴)
139138, 97sseldd 3984 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ βˆͺ 𝐢 ∈ 𝐴)
140 r1ord2 9779 . . . . . . . . . . . . . . 15 (𝐴 ∈ On β†’ (βˆͺ 𝐢 ∈ 𝐴 β†’ (𝑅1β€˜βˆͺ 𝐢) βŠ† (𝑅1β€˜π΄)))
141136, 139, 140sylc 65 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜βˆͺ 𝐢) βŠ† (𝑅1β€˜π΄))
142 ssdomg 8999 . . . . . . . . . . . . . 14 ((𝑅1β€˜π΄) ∈ V β†’ ((𝑅1β€˜βˆͺ 𝐢) βŠ† (𝑅1β€˜π΄) β†’ (𝑅1β€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄)))
143134, 141, 142mpsyl 68 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄))
144 endomtr 9011 . . . . . . . . . . . . 13 ((ran (πΊβ€˜βˆͺ 𝐢) β‰ˆ (𝑅1β€˜βˆͺ 𝐢) ∧ (𝑅1β€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄)) β†’ ran (πΊβ€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄))
145133, 143, 144syl2anc 583 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran (πΊβ€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄))
146 endomtr 9011 . . . . . . . . . . . 12 ((dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰ˆ ran (πΊβ€˜βˆͺ 𝐢) ∧ ran (πΊβ€˜βˆͺ 𝐢) β‰Ό (𝑅1β€˜π΄)) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰Ό (𝑅1β€˜π΄))
147129, 145, 146syl2anc 583 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰Ό (𝑅1β€˜π΄))
148 elharval 9559 . . . . . . . . . . 11 (dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ (harβ€˜(𝑅1β€˜π΄)) ↔ (dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ On ∧ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) β‰Ό (𝑅1β€˜π΄)))
149127, 147, 148sylanbrc 582 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ (harβ€˜(𝑅1β€˜π΄)))
150 ordelss 6381 . . . . . . . . . 10 ((Ord (harβ€˜(𝑅1β€˜π΄)) ∧ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∈ (harβ€˜(𝑅1β€˜π΄))) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) βŠ† (harβ€˜(𝑅1β€˜π΄)))
151125, 149, 150sylancr 586 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) βŠ† (harβ€˜(𝑅1β€˜π΄)))
152123, 151sstrd 3993 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ran 𝐻 βŠ† (harβ€˜(𝑅1β€˜π΄)))
15378, 152sstrid 3994 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑦) βŠ† (harβ€˜(𝑅1β€˜π΄)))
154 fvex 6905 . . . . . . . 8 (harβ€˜(𝑅1β€˜π΄)) ∈ V
155154elpw2 5346 . . . . . . 7 ((𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)) ↔ (𝐻 β€œ 𝑦) βŠ† (harβ€˜(𝑅1β€˜π΄)))
156153, 155sylibr 233 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)))
15777, 156ffvelcdmd 7088 . . . . 5 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (πΉβ€˜(𝐻 β€œ 𝑦)) ∈ On)
15873, 157ifclda 4564 . . . 4 ((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) ∈ On)
159158ex 412 . . 3 (πœ‘ β†’ (𝑦 ∈ (𝑅1β€˜πΆ) β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) ∈ On))
160 iftrue 4535 . . . . . . . 8 (𝐢 = βˆͺ 𝐢 β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)))
161 iftrue 4535 . . . . . . . 8 (𝐢 = βˆͺ 𝐢 β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) = ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)))
162160, 161eqeq12d 2747 . . . . . . 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 481 . . . . . 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 723 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ∈ On)
165 nsuceq0 6448 . . . . . . . 8 suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) β‰  βˆ…
166165a1i 11 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) β‰  βˆ…)
16743a1i 11 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (rankβ€˜π‘¦) ∈ On)
168 onsucuni 7819 . . . . . . . . . . 11 (ran βˆͺ (𝐺 β€œ 𝐢) βŠ† On β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
16937, 168syl 17 . . . . . . . . . 10 (πœ‘ β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
170169ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ran βˆͺ (𝐺 β€œ 𝐢) βŠ† suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
17126ad2antrr 723 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ 𝐢 βŠ† On)
172 fnfvima 7238 . . . . . . . . . . . 12 ((𝐺 Fn On ∧ 𝐢 βŠ† On ∧ suc (rankβ€˜π‘¦) ∈ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) ∈ (𝐺 β€œ 𝐢))
1732, 171, 63, 172mp3an2i 1465 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) ∈ (𝐺 β€œ 𝐢))
174 elssuni 4942 . . . . . . . . . . 11 ((πΊβ€˜suc (rankβ€˜π‘¦)) ∈ (𝐺 β€œ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) βŠ† βˆͺ (𝐺 β€œ 𝐢))
175 rnss 5939 . . . . . . . . . . 11 ((πΊβ€˜suc (rankβ€˜π‘¦)) βŠ† βˆͺ (𝐺 β€œ 𝐢) β†’ ran (πΊβ€˜suc (rankβ€˜π‘¦)) βŠ† ran βˆͺ (𝐺 β€œ 𝐢))
176173, 174, 1753syl 18 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ran (πΊβ€˜suc (rankβ€˜π‘¦)) βŠ† ran βˆͺ (𝐺 β€œ 𝐢))
177 f1fn 6789 . . . . . . . . . . . 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 7083 . . . . . . . . . . 11 (((πΊβ€˜suc (rankβ€˜π‘¦)) Fn (𝑅1β€˜suc (rankβ€˜π‘¦)) ∧ 𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦))) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ ran (πΊβ€˜suc (rankβ€˜π‘¦)))
180178, 70, 179syl2anc 583 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ ran (πΊβ€˜suc (rankβ€˜π‘¦)))
181176, 180sseldd 3984 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ ran βˆͺ (𝐺 β€œ 𝐢))
182170, 181sseldd 3984 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
183182adantlrr 718 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
184 rankon 9793 . . . . . . . 8 (rankβ€˜π‘§) ∈ On
185184a1i 11 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (rankβ€˜π‘§) ∈ On)
186 eleq1w 2815 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ (𝑦 ∈ (𝑅1β€˜πΆ) ↔ 𝑧 ∈ (𝑅1β€˜πΆ)))
187186anbi2d 628 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ ((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ↔ (πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ))))
188187anbi1d 629 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) ↔ ((πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢)))
189 fveq2 6892 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 β†’ (rankβ€˜π‘¦) = (rankβ€˜π‘§))
190 suceq 6431 . . . . . . . . . . . . . 14 ((rankβ€˜π‘¦) = (rankβ€˜π‘§) β†’ suc (rankβ€˜π‘¦) = suc (rankβ€˜π‘§))
191189, 190syl 17 . . . . . . . . . . . . 13 (𝑦 = 𝑧 β†’ suc (rankβ€˜π‘¦) = suc (rankβ€˜π‘§))
192191fveq2d 6896 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) = (πΊβ€˜suc (rankβ€˜π‘§)))
193 id 22 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ 𝑦 = 𝑧)
194192, 193fveq12d 6899 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§))
195194eleq1d 2817 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ (((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) ↔ ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢)))
196188, 195imbi12d 343 . . . . . . . . 9 (𝑦 = 𝑧 β†’ ((((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢)) ↔ (((πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))))
197196, 182chvarvv 2001 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
198197adantlrl 717 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§) ∈ suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢))
199 omopth2 8587 . . . . . . 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 1385 . . . . . 6 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)) = ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)) ↔ ((rankβ€˜π‘¦) = (rankβ€˜π‘§) ∧ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§))))
201190adantl 481 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ suc (rankβ€˜π‘¦) = suc (rankβ€˜π‘§))
202201fveq2d 6896 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)) = (πΊβ€˜suc (rankβ€˜π‘§)))
203202fveq1d 6894 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘§) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§))
204203eqeq2d 2742 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ (((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘§) ↔ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)))
20564adantlrr 718 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)):(𝑅1β€˜suc (rankβ€˜π‘¦))–1-1β†’On)
206205adantr 480 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ (πΊβ€˜suc (rankβ€˜π‘¦)):(𝑅1β€˜suc (rankβ€˜π‘¦))–1-1β†’On)
20770adantlrr 718 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))
208207adantr 480 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ 𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))
209 r1elwf 9794 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑅1β€˜πΆ) β†’ 𝑧 ∈ βˆͺ (𝑅1 β€œ On))
210 rankidb 9798 . . . . . . . . . . . . . . 15 (𝑧 ∈ βˆͺ (𝑅1 β€œ On) β†’ 𝑧 ∈ (𝑅1β€˜suc (rankβ€˜π‘§)))
211209, 210syl 17 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑅1β€˜πΆ) β†’ 𝑧 ∈ (𝑅1β€˜suc (rankβ€˜π‘§)))
212211ad2antll 726 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) β†’ 𝑧 ∈ (𝑅1β€˜suc (rankβ€˜π‘§)))
213212ad2antrr 723 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ 𝑧 ∈ (𝑅1β€˜suc (rankβ€˜π‘§)))
214201fveq2d 6896 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ (𝑅1β€˜suc (rankβ€˜π‘¦)) = (𝑅1β€˜suc (rankβ€˜π‘§)))
215213, 214eleqtrrd 2835 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) ∧ (rankβ€˜π‘¦) = (rankβ€˜π‘§)) β†’ 𝑧 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))
216 f1fveq 7264 . . . . . . . . . . 11 (((πΊβ€˜suc (rankβ€˜π‘¦)):(𝑅1β€˜suc (rankβ€˜π‘¦))–1-1β†’On ∧ (𝑦 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)) ∧ 𝑧 ∈ (𝑅1β€˜suc (rankβ€˜π‘¦)))) β†’ (((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘§) ↔ 𝑦 = 𝑧))
217206, 208, 215, 216syl12anc 834 . . . . . . . . . 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 453 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ 𝐢 = βˆͺ 𝐢) β†’ (((rankβ€˜π‘¦) = (rankβ€˜π‘§) ∧ ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)) β†’ 𝑦 = 𝑧))
221189, 194jca 511 . . . . . . 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 4538 . . . . . . . 8 (Β¬ 𝐢 = βˆͺ 𝐢 β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = (πΉβ€˜(𝐻 β€œ 𝑦)))
225 iffalse 4538 . . . . . . . 8 (Β¬ 𝐢 = βˆͺ 𝐢 β†’ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) = (πΉβ€˜(𝐻 β€œ 𝑧)))
226224, 225eqeq12d 2747 . . . . . . 7 (Β¬ 𝐢 = βˆͺ 𝐢 β†’ (if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) ↔ (πΉβ€˜(𝐻 β€œ 𝑦)) = (πΉβ€˜(𝐻 β€œ 𝑧))))
227226adantl 481 . . . . . 6 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) ↔ (πΉβ€˜(𝐻 β€œ 𝑦)) = (πΉβ€˜(𝐻 β€œ 𝑧))))
22874ad2antrr 723 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))–1-1β†’On)
229156adantlrr 718 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)))
230187anbi1d 629 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) ↔ ((πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢)))
231 imaeq2 6056 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ (𝐻 β€œ 𝑦) = (𝐻 β€œ 𝑧))
232231eleq1d 2817 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ ((𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)) ↔ (𝐻 β€œ 𝑧) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄))))
233230, 232imbi12d 343 . . . . . . . . 9 (𝑦 = 𝑧 β†’ ((((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄))) ↔ (((πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑧) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)))))
234233, 156chvarvv 2001 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑧) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)))
235234adantlrl 717 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝐻 β€œ 𝑧) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)))
236 f1fveq 7264 . . . . . . 7 ((𝐹:𝒫 (harβ€˜(𝑅1β€˜π΄))–1-1β†’On ∧ ((𝐻 β€œ 𝑦) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)) ∧ (𝐻 β€œ 𝑧) ∈ 𝒫 (harβ€˜(𝑅1β€˜π΄)))) β†’ ((πΉβ€˜(𝐻 β€œ 𝑦)) = (πΉβ€˜(𝐻 β€œ 𝑧)) ↔ (𝐻 β€œ 𝑦) = (𝐻 β€œ 𝑧)))
237228, 229, 235, 236syl12anc 834 . . . . . 6 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ ((πΉβ€˜(𝐻 β€œ 𝑦)) = (πΉβ€˜(𝐻 β€œ 𝑧)) ↔ (𝐻 β€œ 𝑦) = (𝐻 β€œ 𝑧)))
238120adantlrr 718 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝐻:(𝑅1β€˜βˆͺ 𝐢)–1-1β†’dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)))
239 simplrl 774 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 ∈ (𝑅1β€˜πΆ))
24096fveq2d 6896 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜πΆ) = (𝑅1β€˜suc βˆͺ 𝐢))
241 r1suc 9768 . . . . . . . . . . . 12 (βˆͺ 𝐢 ∈ On β†’ (𝑅1β€˜suc βˆͺ 𝐢) = 𝒫 (𝑅1β€˜βˆͺ 𝐢))
24289, 90, 2413syl 18 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜suc βˆͺ 𝐢) = 𝒫 (𝑅1β€˜βˆͺ 𝐢))
243240, 242eqtrd 2771 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝑅1β€˜πΆ)) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜πΆ) = 𝒫 (𝑅1β€˜βˆͺ 𝐢))
244243adantlrr 718 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ (𝑅1β€˜πΆ) = 𝒫 (𝑅1β€˜βˆͺ 𝐢))
245239, 244eleqtrd 2834 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 ∈ 𝒫 (𝑅1β€˜βˆͺ 𝐢))
246245elpwid 4612 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑦 βŠ† (𝑅1β€˜βˆͺ 𝐢))
247 simplrr 775 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑧 ∈ (𝑅1β€˜πΆ))
248247, 244eleqtrd 2834 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑧 ∈ 𝒫 (𝑅1β€˜βˆͺ 𝐢))
249248elpwid 4612 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) ∧ Β¬ 𝐢 = βˆͺ 𝐢) β†’ 𝑧 βŠ† (𝑅1β€˜βˆͺ 𝐢))
250 f1imaeq 7267 . . . . . . 7 ((𝐻:(𝑅1β€˜βˆͺ 𝐢)–1-1β†’dom OrdIso( E , ran (πΊβ€˜βˆͺ 𝐢)) ∧ (𝑦 βŠ† (𝑅1β€˜βˆͺ 𝐢) ∧ 𝑧 βŠ† (𝑅1β€˜βˆͺ 𝐢))) β†’ ((𝐻 β€œ 𝑦) = (𝐻 β€œ 𝑧) ↔ 𝑦 = 𝑧))
251238, 246, 249, 250syl12anc 834 . . . . . 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 810 . . . 4 ((πœ‘ ∧ (𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ))) β†’ (if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) ↔ 𝑦 = 𝑧))
254253ex 412 . . 3 (πœ‘ β†’ ((𝑦 ∈ (𝑅1β€˜πΆ) ∧ 𝑧 ∈ (𝑅1β€˜πΆ)) β†’ (if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦))) = if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘§)) +o ((πΊβ€˜suc (rankβ€˜π‘§))β€˜π‘§)), (πΉβ€˜(𝐻 β€œ 𝑧))) ↔ 𝑦 = 𝑧)))
255159, 254dom2lem 8991 . 2 (πœ‘ β†’ (𝑦 ∈ (𝑅1β€˜πΆ) ↦ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦)))):(𝑅1β€˜πΆ)–1-1β†’On)
256135, 74, 1, 5, 117dfac12lem1 10141 . . 3 (πœ‘ β†’ (πΊβ€˜πΆ) = (𝑦 ∈ (𝑅1β€˜πΆ) ↦ if(𝐢 = βˆͺ 𝐢, ((suc βˆͺ ran βˆͺ (𝐺 β€œ 𝐢) Β·o (rankβ€˜π‘¦)) +o ((πΊβ€˜suc (rankβ€˜π‘¦))β€˜π‘¦)), (πΉβ€˜(𝐻 β€œ 𝑦)))))
257 f1eq1 6783 . . 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 395   ∨ wo 844   = wceq 1540   ∈ wcel 2105   β‰  wne 2939  βˆ€wral 3060  Vcvv 3473   βŠ† wss 3949  βˆ…c0 4323  ifcif 4529  π’« cpw 4603  βˆͺ cuni 4909   class class class wbr 5149   ↦ cmpt 5232   E cep 5580   We wwe 5631   Γ— cxp 5675  β—‘ccnv 5676  dom cdm 5677  ran crn 5678   β€œ cima 5680   ∘ ccom 5681  Ord word 6364  Oncon0 6365  suc csuc 6367  Fun wfun 6538   Fn wfn 6539  βŸΆwf 6540  β€“1-1β†’wf1 6541  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544   Isom wiso 6545  (class class class)co 7412  recscrecs 8373   +o coa 8466   Β·o comu 8467   β‰ˆ cen 8939   β‰Ό cdom 8940  OrdIsocoi 9507  harchar 9554  π‘…1cr1 9760  rankcrnk 9761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-oadd 8473  df-omul 8474  df-er 8706  df-en 8943  df-dom 8944  df-oi 9508  df-har 9555  df-r1 9762  df-rank 9763
This theorem is referenced by:  dfac12lem3  10143
  Copyright terms: Public domain W3C validator