MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  domtriomlem Structured version   Visualization version   GIF version
Theorem domtriomlem 10433
Description: Lemma for domtriom 10434. (Contributed by Mario Carneiro, 9-Feb-2013.)
Hypotheses
Ref Expression
domtriomlem.1 𝐴 ∈ V
domtriomlem.2 𝐡 = {𝑦 ∣ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛)}
domtriomlem.3 𝐢 = (𝑛 ∈ Ο‰ ↦ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)))
Assertion
Ref Expression
domtriomlem (Β¬ 𝐴 ∈ Fin β†’ Ο‰ β‰Ό 𝐴)
Distinct variable groups:   𝐴,𝑏,𝑛,𝑦   𝐡,𝑏   𝐢,π‘˜,𝑛   π‘˜,𝑏   𝑦,𝑏
Allowed substitution hints:   𝐴(π‘˜)   𝐡(𝑦,π‘˜,𝑛)   𝐢(𝑦,𝑏)
Proof of Theorem domtriomlem
Dummy variables 𝑐 π‘š 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 domtriomlem.2 . . . . 5 𝐡 = {𝑦 ∣ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛)}
2 domtriomlem.1 . . . . . . 7 𝐴 ∈ V
32pwex 5377 . . . . . 6 𝒫 𝐴 ∈ V
4 simpl 483 . . . . . . . 8 ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛) β†’ 𝑦 βŠ† 𝐴)
54ss2abi 4062 . . . . . . 7 {𝑦 ∣ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛)} βŠ† {𝑦 ∣ 𝑦 βŠ† 𝐴}
6 df-pw 4603 . . . . . . 7 𝒫 𝐴 = {𝑦 ∣ 𝑦 βŠ† 𝐴}
75, 6sseqtrri 4018 . . . . . 6 {𝑦 ∣ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛)} βŠ† 𝒫 𝐴
83, 7ssexi 5321 . . . . 5 {𝑦 ∣ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛)} ∈ V
91, 8eqeltri 2829 . . . 4 𝐡 ∈ V
10 omex 9634 . . . . 5 Ο‰ ∈ V
1110enref 8977 . . . 4 Ο‰ β‰ˆ Ο‰
129, 11axcc3 10429 . . 3 βˆƒπ‘(𝑏 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (𝐡 β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ 𝐡))
13 nfv 1917 . . . . . . . 8 Ⅎ𝑛 Β¬ 𝐴 ∈ Fin
14 nfra1 3281 . . . . . . . 8 β„²π‘›βˆ€π‘› ∈ Ο‰ (𝐡 β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ 𝐡)
1513, 14nfan 1902 . . . . . . 7 Ⅎ𝑛(Β¬ 𝐴 ∈ Fin ∧ βˆ€π‘› ∈ Ο‰ (𝐡 β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ 𝐡))
16 nnfi 9163 . . . . . . . . . . . . . 14 (𝑛 ∈ Ο‰ β†’ 𝑛 ∈ Fin)
17 pwfi 9174 . . . . . . . . . . . . . 14 (𝑛 ∈ Fin ↔ 𝒫 𝑛 ∈ Fin)
1816, 17sylib 217 . . . . . . . . . . . . 13 (𝑛 ∈ Ο‰ β†’ 𝒫 𝑛 ∈ Fin)
19 ficardom 9952 . . . . . . . . . . . . 13 (𝒫 𝑛 ∈ Fin β†’ (cardβ€˜π’« 𝑛) ∈ Ο‰)
20 isinf 9256 . . . . . . . . . . . . . 14 (Β¬ 𝐴 ∈ Fin β†’ βˆ€π‘š ∈ Ο‰ βˆƒπ‘¦(𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ π‘š))
21 breq2 5151 . . . . . . . . . . . . . . . . 17 (π‘š = (cardβ€˜π’« 𝑛) β†’ (𝑦 β‰ˆ π‘š ↔ 𝑦 β‰ˆ (cardβ€˜π’« 𝑛)))
2221anbi2d 629 . . . . . . . . . . . . . . . 16 (π‘š = (cardβ€˜π’« 𝑛) β†’ ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ π‘š) ↔ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ (cardβ€˜π’« 𝑛))))
2322exbidv 1924 . . . . . . . . . . . . . . 15 (π‘š = (cardβ€˜π’« 𝑛) β†’ (βˆƒπ‘¦(𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ π‘š) ↔ βˆƒπ‘¦(𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ (cardβ€˜π’« 𝑛))))
2423rspcv 3608 . . . . . . . . . . . . . 14 ((cardβ€˜π’« 𝑛) ∈ Ο‰ β†’ (βˆ€π‘š ∈ Ο‰ βˆƒπ‘¦(𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ π‘š) β†’ βˆƒπ‘¦(𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ (cardβ€˜π’« 𝑛))))
2520, 24syl5 34 . . . . . . . . . . . . 13 ((cardβ€˜π’« 𝑛) ∈ Ο‰ β†’ (Β¬ 𝐴 ∈ Fin β†’ βˆƒπ‘¦(𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ (cardβ€˜π’« 𝑛))))
2618, 19, 253syl 18 . . . . . . . . . . . 12 (𝑛 ∈ Ο‰ β†’ (Β¬ 𝐴 ∈ Fin β†’ βˆƒπ‘¦(𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ (cardβ€˜π’« 𝑛))))
27 finnum 9939 . . . . . . . . . . . . . . 15 (𝒫 𝑛 ∈ Fin β†’ 𝒫 𝑛 ∈ dom card)
28 cardid2 9944 . . . . . . . . . . . . . . 15 (𝒫 𝑛 ∈ dom card β†’ (cardβ€˜π’« 𝑛) β‰ˆ 𝒫 𝑛)
29 entr 8998 . . . . . . . . . . . . . . . 16 ((𝑦 β‰ˆ (cardβ€˜π’« 𝑛) ∧ (cardβ€˜π’« 𝑛) β‰ˆ 𝒫 𝑛) β†’ 𝑦 β‰ˆ 𝒫 𝑛)
3029expcom 414 . . . . . . . . . . . . . . 15 ((cardβ€˜π’« 𝑛) β‰ˆ 𝒫 𝑛 β†’ (𝑦 β‰ˆ (cardβ€˜π’« 𝑛) β†’ 𝑦 β‰ˆ 𝒫 𝑛))
3118, 27, 28, 304syl 19 . . . . . . . . . . . . . 14 (𝑛 ∈ Ο‰ β†’ (𝑦 β‰ˆ (cardβ€˜π’« 𝑛) β†’ 𝑦 β‰ˆ 𝒫 𝑛))
3231anim2d 612 . . . . . . . . . . . . 13 (𝑛 ∈ Ο‰ β†’ ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ (cardβ€˜π’« 𝑛)) β†’ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛)))
3332eximdv 1920 . . . . . . . . . . . 12 (𝑛 ∈ Ο‰ β†’ (βˆƒπ‘¦(𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ (cardβ€˜π’« 𝑛)) β†’ βˆƒπ‘¦(𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛)))
3426, 33syld 47 . . . . . . . . . . 11 (𝑛 ∈ Ο‰ β†’ (Β¬ 𝐴 ∈ Fin β†’ βˆƒπ‘¦(𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛)))
351neeq1i 3005 . . . . . . . . . . . 12 (𝐡 β‰  βˆ… ↔ {𝑦 ∣ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛)} β‰  βˆ…)
36 abn0 4379 . . . . . . . . . . . 12 ({𝑦 ∣ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛)} β‰  βˆ… ↔ βˆƒπ‘¦(𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛))
3735, 36bitri 274 . . . . . . . . . . 11 (𝐡 β‰  βˆ… ↔ βˆƒπ‘¦(𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛))
3834, 37syl6ibr 251 . . . . . . . . . 10 (𝑛 ∈ Ο‰ β†’ (Β¬ 𝐴 ∈ Fin β†’ 𝐡 β‰  βˆ…))
3938com12 32 . . . . . . . . 9 (Β¬ 𝐴 ∈ Fin β†’ (𝑛 ∈ Ο‰ β†’ 𝐡 β‰  βˆ…))
4039adantr 481 . . . . . . . 8 ((Β¬ 𝐴 ∈ Fin ∧ βˆ€π‘› ∈ Ο‰ (𝐡 β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ 𝐡)) β†’ (𝑛 ∈ Ο‰ β†’ 𝐡 β‰  βˆ…))
41 rsp 3244 . . . . . . . . 9 (βˆ€π‘› ∈ Ο‰ (𝐡 β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ 𝐡) β†’ (𝑛 ∈ Ο‰ β†’ (𝐡 β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ 𝐡)))
4241adantl 482 . . . . . . . 8 ((Β¬ 𝐴 ∈ Fin ∧ βˆ€π‘› ∈ Ο‰ (𝐡 β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ 𝐡)) β†’ (𝑛 ∈ Ο‰ β†’ (𝐡 β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ 𝐡)))
4340, 42mpdd 43 . . . . . . 7 ((Β¬ 𝐴 ∈ Fin ∧ βˆ€π‘› ∈ Ο‰ (𝐡 β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ 𝐡)) β†’ (𝑛 ∈ Ο‰ β†’ (π‘β€˜π‘›) ∈ 𝐡))
4415, 43ralrimi 3254 . . . . . 6 ((Β¬ 𝐴 ∈ Fin ∧ βˆ€π‘› ∈ Ο‰ (𝐡 β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ 𝐡)) β†’ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡)
45443adant2 1131 . . . . 5 ((Β¬ 𝐴 ∈ Fin ∧ 𝑏 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (𝐡 β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ 𝐡)) β†’ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡)
46453expib 1122 . . . 4 (Β¬ 𝐴 ∈ Fin β†’ ((𝑏 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (𝐡 β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ 𝐡)) β†’ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡))
4746eximdv 1920 . . 3 (Β¬ 𝐴 ∈ Fin β†’ (βˆƒπ‘(𝑏 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (𝐡 β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ 𝐡)) β†’ βˆƒπ‘βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡))
4812, 47mpi 20 . 2 (Β¬ 𝐴 ∈ Fin β†’ βˆƒπ‘βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡)
49 axcc2 10428 . . . . 5 βˆƒπ‘(𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)))
50 simp2 1137 . . . . . . . 8 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ 𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))) β†’ 𝑐 Fn Ο‰)
51 nfra1 3281 . . . . . . . . . . 11 β„²π‘›βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡
52 nfra1 3281 . . . . . . . . . . 11 β„²π‘›βˆ€π‘› ∈ Ο‰ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))
5351, 52nfan 1902 . . . . . . . . . 10 Ⅎ𝑛(βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ βˆ€π‘› ∈ Ο‰ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)))
54 fvex 6901 . . . . . . . . . . . . . . . 16 (π‘β€˜π‘›) ∈ V
55 sseq1 4006 . . . . . . . . . . . . . . . . 17 (𝑦 = (π‘β€˜π‘›) β†’ (𝑦 βŠ† 𝐴 ↔ (π‘β€˜π‘›) βŠ† 𝐴))
56 breq1 5150 . . . . . . . . . . . . . . . . 17 (𝑦 = (π‘β€˜π‘›) β†’ (𝑦 β‰ˆ 𝒫 𝑛 ↔ (π‘β€˜π‘›) β‰ˆ 𝒫 𝑛))
5755, 56anbi12d 631 . . . . . . . . . . . . . . . 16 (𝑦 = (π‘β€˜π‘›) β†’ ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝒫 𝑛) ↔ ((π‘β€˜π‘›) βŠ† 𝐴 ∧ (π‘β€˜π‘›) β‰ˆ 𝒫 𝑛)))
5854, 57, 1elab2 3671 . . . . . . . . . . . . . . 15 ((π‘β€˜π‘›) ∈ 𝐡 ↔ ((π‘β€˜π‘›) βŠ† 𝐴 ∧ (π‘β€˜π‘›) β‰ˆ 𝒫 𝑛))
5958simprbi 497 . . . . . . . . . . . . . 14 ((π‘β€˜π‘›) ∈ 𝐡 β†’ (π‘β€˜π‘›) β‰ˆ 𝒫 𝑛)
6059ralimi 3083 . . . . . . . . . . . . 13 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) β‰ˆ 𝒫 𝑛)
61 fveq2 6888 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘˜ β†’ (π‘β€˜π‘›) = (π‘β€˜π‘˜))
62 pweq 4615 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘˜ β†’ 𝒫 𝑛 = 𝒫 π‘˜)
6361, 62breq12d 5160 . . . . . . . . . . . . . . . 16 (𝑛 = π‘˜ β†’ ((π‘β€˜π‘›) β‰ˆ 𝒫 𝑛 ↔ (π‘β€˜π‘˜) β‰ˆ 𝒫 π‘˜))
6463cbvralvw 3234 . . . . . . . . . . . . . . 15 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) β‰ˆ 𝒫 𝑛 ↔ βˆ€π‘˜ ∈ Ο‰ (π‘β€˜π‘˜) β‰ˆ 𝒫 π‘˜)
65 peano2 7877 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ Ο‰ β†’ suc 𝑛 ∈ Ο‰)
66 omelon 9637 . . . . . . . . . . . . . . . . . . 19 Ο‰ ∈ On
6766onelssi 6476 . . . . . . . . . . . . . . . . . 18 (suc 𝑛 ∈ Ο‰ β†’ suc 𝑛 βŠ† Ο‰)
68 ssralv 4049 . . . . . . . . . . . . . . . . . 18 (suc 𝑛 βŠ† Ο‰ β†’ (βˆ€π‘˜ ∈ Ο‰ (π‘β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆ€π‘˜ ∈ suc 𝑛(π‘β€˜π‘˜) β‰ˆ 𝒫 π‘˜))
6965, 67, 683syl 18 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘˜ ∈ Ο‰ (π‘β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆ€π‘˜ ∈ suc 𝑛(π‘β€˜π‘˜) β‰ˆ 𝒫 π‘˜))
70 pwsdompw 10195 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc 𝑛(π‘β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜) β‰Ί (π‘β€˜π‘›))
7170ex 413 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘˜ ∈ suc 𝑛(π‘β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜) β‰Ί (π‘β€˜π‘›)))
7269, 71syld 47 . . . . . . . . . . . . . . . 16 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘˜ ∈ Ο‰ (π‘β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜) β‰Ί (π‘β€˜π‘›)))
73 sdomdif 9121 . . . . . . . . . . . . . . . 16 (βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜) β‰Ί (π‘β€˜π‘›) β†’ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)) β‰  βˆ…)
7472, 73syl6 35 . . . . . . . . . . . . . . 15 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘˜ ∈ Ο‰ (π‘β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)) β‰  βˆ…))
7564, 74biimtrid 241 . . . . . . . . . . . . . 14 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) β‰ˆ 𝒫 𝑛 β†’ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)) β‰  βˆ…))
7654difexi 5327 . . . . . . . . . . . . . . . 16 ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)) ∈ V
77 domtriomlem.3 . . . . . . . . . . . . . . . . 17 𝐢 = (𝑛 ∈ Ο‰ ↦ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)))
7877fvmpt2 7006 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ Ο‰ ∧ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)) ∈ V) β†’ (πΆβ€˜π‘›) = ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)))
7976, 78mpan2 689 . . . . . . . . . . . . . . 15 (𝑛 ∈ Ο‰ β†’ (πΆβ€˜π‘›) = ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)))
8079neeq1d 3000 . . . . . . . . . . . . . 14 (𝑛 ∈ Ο‰ β†’ ((πΆβ€˜π‘›) β‰  βˆ… ↔ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)) β‰  βˆ…))
8175, 80sylibrd 258 . . . . . . . . . . . . 13 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) β‰ˆ 𝒫 𝑛 β†’ (πΆβ€˜π‘›) β‰  βˆ…))
8260, 81syl5com 31 . . . . . . . . . . . 12 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ (𝑛 ∈ Ο‰ β†’ (πΆβ€˜π‘›) β‰  βˆ…))
8382adantr 481 . . . . . . . . . . 11 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ βˆ€π‘› ∈ Ο‰ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))) β†’ (𝑛 ∈ Ο‰ β†’ (πΆβ€˜π‘›) β‰  βˆ…))
84 rsp 3244 . . . . . . . . . . . 12 (βˆ€π‘› ∈ Ο‰ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ (𝑛 ∈ Ο‰ β†’ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))))
8584adantl 482 . . . . . . . . . . 11 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ βˆ€π‘› ∈ Ο‰ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))) β†’ (𝑛 ∈ Ο‰ β†’ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))))
8683, 85mpdd 43 . . . . . . . . . 10 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ βˆ€π‘› ∈ Ο‰ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))) β†’ (𝑛 ∈ Ο‰ β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)))
8753, 86ralrimi 3254 . . . . . . . . 9 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ βˆ€π‘› ∈ Ο‰ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))) β†’ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))
88873adant2 1131 . . . . . . . 8 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ 𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))) β†’ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))
8950, 88jca 512 . . . . . . 7 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ 𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))) β†’ (𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)))
90893expib 1122 . . . . . 6 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ ((𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))) β†’ (𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))))
9190eximdv 1920 . . . . 5 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ (βˆƒπ‘(𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ ((πΆβ€˜π‘›) β‰  βˆ… β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))) β†’ βˆƒπ‘(𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))))
9249, 91mpi 20 . . . 4 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ βˆƒπ‘(𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)))
93 simp2 1137 . . . . . . . . . 10 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ 𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ 𝑐 Fn Ο‰)
94 nfra1 3281 . . . . . . . . . . . . 13 β„²π‘›βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)
9551, 94nfan 1902 . . . . . . . . . . . 12 Ⅎ𝑛(βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›))
96 rsp 3244 . . . . . . . . . . . . . . . 16 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (𝑛 ∈ Ο‰ β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)))
9796com12 32 . . . . . . . . . . . . . . 15 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)))
98 rsp 3244 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ (𝑛 ∈ Ο‰ β†’ (π‘β€˜π‘›) ∈ 𝐡))
9998com12 32 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ (π‘β€˜π‘›) ∈ 𝐡))
10079eleq2d 2819 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ Ο‰ β†’ ((π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) ↔ (π‘β€˜π‘›) ∈ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜))))
101 eldifi 4125 . . . . . . . . . . . . . . . . . . 19 ((π‘β€˜π‘›) ∈ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)) β†’ (π‘β€˜π‘›) ∈ (π‘β€˜π‘›))
102100, 101syl6bi 252 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ Ο‰ β†’ ((π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (π‘β€˜π‘›) ∈ (π‘β€˜π‘›)))
10358simplbi 498 . . . . . . . . . . . . . . . . . . 19 ((π‘β€˜π‘›) ∈ 𝐡 β†’ (π‘β€˜π‘›) βŠ† 𝐴)
104103sseld 3980 . . . . . . . . . . . . . . . . . 18 ((π‘β€˜π‘›) ∈ 𝐡 β†’ ((π‘β€˜π‘›) ∈ (π‘β€˜π‘›) β†’ (π‘β€˜π‘›) ∈ 𝐴))
105102, 104syl9 77 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ Ο‰ β†’ ((π‘β€˜π‘›) ∈ 𝐡 β†’ ((π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (π‘β€˜π‘›) ∈ 𝐴)))
10699, 105syld 47 . . . . . . . . . . . . . . . 16 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ ((π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (π‘β€˜π‘›) ∈ 𝐴)))
107106com23 86 . . . . . . . . . . . . . . 15 (𝑛 ∈ Ο‰ β†’ ((π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ (π‘β€˜π‘›) ∈ 𝐴)))
10897, 107syld 47 . . . . . . . . . . . . . 14 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ (π‘β€˜π‘›) ∈ 𝐴)))
109108com13 88 . . . . . . . . . . . . 13 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (𝑛 ∈ Ο‰ β†’ (π‘β€˜π‘›) ∈ 𝐴)))
110109imp 407 . . . . . . . . . . . 12 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ (𝑛 ∈ Ο‰ β†’ (π‘β€˜π‘›) ∈ 𝐴))
11195, 110ralrimi 3254 . . . . . . . . . . 11 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐴)
1121113adant2 1131 . . . . . . . . . 10 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ 𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐴)
113 ffnfv 7114 . . . . . . . . . 10 (𝑐:Ο‰βŸΆπ΄ ↔ (𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐴))
11493, 112, 113sylanbrc 583 . . . . . . . . 9 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ 𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ 𝑐:Ο‰βŸΆπ΄)
115 nfv 1917 . . . . . . . . . . . 12 Ⅎ𝑛 π‘˜ ∈ Ο‰
116 nnord 7859 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ Ο‰ β†’ Ord π‘˜)
117 nnord 7859 . . . . . . . . . . . . . . . 16 (𝑛 ∈ Ο‰ β†’ Ord 𝑛)
118 ordtri3or 6393 . . . . . . . . . . . . . . . 16 ((Ord π‘˜ ∧ Ord 𝑛) β†’ (π‘˜ ∈ 𝑛 ∨ π‘˜ = 𝑛 ∨ 𝑛 ∈ π‘˜))
119116, 117, 118syl2an 596 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰) β†’ (π‘˜ ∈ 𝑛 ∨ π‘˜ = 𝑛 ∨ 𝑛 ∈ π‘˜))
120 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = π‘˜ β†’ (π‘β€˜π‘›) = (π‘β€˜π‘˜))
121 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘˜ = 𝑗 β†’ (π‘β€˜π‘˜) = (π‘β€˜π‘—))
122121cbviunv 5042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜) = βˆͺ 𝑗 ∈ 𝑛 (π‘β€˜π‘—)
123 iuneq1 5012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = π‘˜ β†’ βˆͺ 𝑗 ∈ 𝑛 (π‘β€˜π‘—) = βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—))
124122, 123eqtrid 2784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜) = βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—))
12561, 124difeq12d 4122 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = π‘˜ β†’ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)) = ((π‘β€˜π‘˜) βˆ– βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)))
126120, 125eleq12d 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = π‘˜ β†’ ((π‘β€˜π‘›) ∈ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)) ↔ (π‘β€˜π‘˜) ∈ ((π‘β€˜π‘˜) βˆ– βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—))))
127126rspccv 3609 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)) β†’ (π‘˜ ∈ Ο‰ β†’ (π‘β€˜π‘˜) ∈ ((π‘β€˜π‘˜) βˆ– βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—))))
12896, 100mpbidi 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (𝑛 ∈ Ο‰ β†’ (π‘β€˜π‘›) ∈ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜))))
12994, 128ralrimi 3254 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)))
130127, 129syl11 33 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ ∈ Ο‰ β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (π‘β€˜π‘˜) ∈ ((π‘β€˜π‘˜) βˆ– βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—))))
1311303ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (π‘β€˜π‘˜) ∈ ((π‘β€˜π‘˜) βˆ– βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—))))
132 eldifi 4125 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘β€˜π‘˜) ∈ ((π‘β€˜π‘˜) βˆ– βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)) β†’ (π‘β€˜π‘˜) ∈ (π‘β€˜π‘˜))
133 eleq1 2821 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘β€˜π‘˜) = (π‘β€˜π‘›) β†’ ((π‘β€˜π‘˜) ∈ (π‘β€˜π‘˜) ↔ (π‘β€˜π‘›) ∈ (π‘β€˜π‘˜)))
134132, 133imbitrid 243 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘β€˜π‘˜) = (π‘β€˜π‘›) β†’ ((π‘β€˜π‘˜) ∈ ((π‘β€˜π‘˜) βˆ– βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)) β†’ (π‘β€˜π‘›) ∈ (π‘β€˜π‘˜)))
1351343ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) β†’ ((π‘β€˜π‘˜) ∈ ((π‘β€˜π‘˜) βˆ– βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)) β†’ (π‘β€˜π‘›) ∈ (π‘β€˜π‘˜)))
136131, 135syld 47 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (π‘β€˜π‘›) ∈ (π‘β€˜π‘˜)))
137136imp 407 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ (π‘β€˜π‘›) ∈ (π‘β€˜π‘˜))
138 ssiun2 5049 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ ∈ 𝑛 β†’ (π‘β€˜π‘˜) βŠ† βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜))
139138sseld 3980 . . . . . . . . . . . . . . . . . . . . . 22 (π‘˜ ∈ 𝑛 β†’ ((π‘β€˜π‘›) ∈ (π‘β€˜π‘˜) β†’ (π‘β€˜π‘›) ∈ βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)))
140137, 139syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ ∈ 𝑛 β†’ (((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ (π‘β€˜π‘›) ∈ βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)))
1411403impib 1116 . . . . . . . . . . . . . . . . . . . 20 ((π‘˜ ∈ 𝑛 ∧ (π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ (π‘β€˜π‘›) ∈ βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜))
142128com12 32 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (π‘β€˜π‘›) ∈ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜))))
1431423ad2ant2 1134 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (π‘β€˜π‘›) ∈ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜))))
144143imp 407 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ (π‘β€˜π‘›) ∈ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)))
145144eldifbd 3960 . . . . . . . . . . . . . . . . . . . . 21 (((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ Β¬ (π‘β€˜π‘›) ∈ βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜))
1461453adant1 1130 . . . . . . . . . . . . . . . . . . . 20 ((π‘˜ ∈ 𝑛 ∧ (π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ Β¬ (π‘β€˜π‘›) ∈ βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜))
147141, 146pm2.21dd 194 . . . . . . . . . . . . . . . . . . 19 ((π‘˜ ∈ 𝑛 ∧ (π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ π‘˜ = 𝑛)
1481473exp 1119 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ 𝑛 β†’ ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ π‘˜ = 𝑛)))
149 2a1 28 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑛 β†’ ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ π‘˜ = 𝑛)))
150 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑛 β†’ (π‘β€˜π‘—) = (π‘β€˜π‘›))
151150ssiun2s 5050 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ π‘˜ β†’ (π‘β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—))
152151sseld 3980 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ π‘˜ β†’ ((π‘β€˜π‘›) ∈ (π‘β€˜π‘›) β†’ (π‘β€˜π‘›) ∈ βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)))
153101, 152syl5 34 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ π‘˜ β†’ ((π‘β€˜π‘›) ∈ ((π‘β€˜π‘›) βˆ– βˆͺ π‘˜ ∈ 𝑛 (π‘β€˜π‘˜)) β†’ (π‘β€˜π‘›) ∈ βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)))
154144, 153syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ π‘˜ β†’ (((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ (π‘β€˜π‘›) ∈ βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)))
1551543impib 1116 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ π‘˜ ∧ (π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ (π‘β€˜π‘›) ∈ βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—))
156 eleq1 2821 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘β€˜π‘˜) = (π‘β€˜π‘›) β†’ ((π‘β€˜π‘˜) ∈ ((π‘β€˜π‘˜) βˆ– βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)) ↔ (π‘β€˜π‘›) ∈ ((π‘β€˜π‘˜) βˆ– βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—))))
157 eldifn 4126 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘β€˜π‘›) ∈ ((π‘β€˜π‘˜) βˆ– βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)) β†’ Β¬ (π‘β€˜π‘›) ∈ βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—))
158156, 157syl6bi 252 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘β€˜π‘˜) = (π‘β€˜π‘›) β†’ ((π‘β€˜π‘˜) ∈ ((π‘β€˜π‘˜) βˆ– βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)) β†’ Β¬ (π‘β€˜π‘›) ∈ βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)))
1591583ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) β†’ ((π‘β€˜π‘˜) ∈ ((π‘β€˜π‘˜) βˆ– βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)) β†’ Β¬ (π‘β€˜π‘›) ∈ βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)))
160131, 159syld 47 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ Β¬ (π‘β€˜π‘›) ∈ βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—)))
161160a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ π‘˜ β†’ ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ Β¬ (π‘β€˜π‘›) ∈ βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—))))
1621613imp 1111 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ π‘˜ ∧ (π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ Β¬ (π‘β€˜π‘›) ∈ βˆͺ 𝑗 ∈ π‘˜ (π‘β€˜π‘—))
163155, 162pm2.21dd 194 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ π‘˜ ∧ (π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ π‘˜ = 𝑛)
1641633exp 1119 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ π‘˜ β†’ ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ π‘˜ = 𝑛)))
165148, 149, 1643jaoi 1427 . . . . . . . . . . . . . . . . 17 ((π‘˜ ∈ 𝑛 ∨ π‘˜ = 𝑛 ∨ 𝑛 ∈ π‘˜) β†’ ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ π‘˜ = 𝑛)))
166165com12 32 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰ ∧ (π‘β€˜π‘˜) = (π‘β€˜π‘›)) β†’ ((π‘˜ ∈ 𝑛 ∨ π‘˜ = 𝑛 ∨ 𝑛 ∈ π‘˜) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ π‘˜ = 𝑛)))
1671663expia 1121 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰) β†’ ((π‘β€˜π‘˜) = (π‘β€˜π‘›) β†’ ((π‘˜ ∈ 𝑛 ∨ π‘˜ = 𝑛 ∨ 𝑛 ∈ π‘˜) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ π‘˜ = 𝑛))))
168119, 167mpid 44 . . . . . . . . . . . . . 14 ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰) β†’ ((π‘β€˜π‘˜) = (π‘β€˜π‘›) β†’ (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ π‘˜ = 𝑛)))
169168com3r 87 . . . . . . . . . . . . 13 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ ((π‘˜ ∈ Ο‰ ∧ 𝑛 ∈ Ο‰) β†’ ((π‘β€˜π‘˜) = (π‘β€˜π‘›) β†’ π‘˜ = 𝑛)))
170169expd 416 . . . . . . . . . . . 12 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (π‘˜ ∈ Ο‰ β†’ (𝑛 ∈ Ο‰ β†’ ((π‘β€˜π‘˜) = (π‘β€˜π‘›) β†’ π‘˜ = 𝑛))))
17194, 115, 170ralrimd 3261 . . . . . . . . . . 11 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ (π‘˜ ∈ Ο‰ β†’ βˆ€π‘› ∈ Ο‰ ((π‘β€˜π‘˜) = (π‘β€˜π‘›) β†’ π‘˜ = 𝑛)))
172171ralrimiv 3145 . . . . . . . . . 10 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›) β†’ βˆ€π‘˜ ∈ Ο‰ βˆ€π‘› ∈ Ο‰ ((π‘β€˜π‘˜) = (π‘β€˜π‘›) β†’ π‘˜ = 𝑛))
1731723ad2ant3 1135 . . . . . . . . 9 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ 𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ βˆ€π‘˜ ∈ Ο‰ βˆ€π‘› ∈ Ο‰ ((π‘β€˜π‘˜) = (π‘β€˜π‘›) β†’ π‘˜ = 𝑛))
174 dff13 7250 . . . . . . . . 9 (𝑐:ω–1-1→𝐴 ↔ (𝑐:Ο‰βŸΆπ΄ ∧ βˆ€π‘˜ ∈ Ο‰ βˆ€π‘› ∈ Ο‰ ((π‘β€˜π‘˜) = (π‘β€˜π‘›) β†’ π‘˜ = 𝑛)))
175114, 173, 174sylanbrc 583 . . . . . . . 8 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ 𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ 𝑐:ω–1-1→𝐴)
17617519.8ad 2175 . . . . . . 7 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ 𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ βˆƒπ‘ 𝑐:ω–1-1→𝐴)
1772brdom 8952 . . . . . . 7 (Ο‰ β‰Ό 𝐴 ↔ βˆƒπ‘ 𝑐:ω–1-1→𝐴)
178176, 177sylibr 233 . . . . . 6 ((βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 ∧ 𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ Ο‰ β‰Ό 𝐴)
1791783expib 1122 . . . . 5 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ ((𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ Ο‰ β‰Ό 𝐴))
180179exlimdv 1936 . . . 4 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ (βˆƒπ‘(𝑐 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ (πΆβ€˜π‘›)) β†’ Ο‰ β‰Ό 𝐴))
18192, 180mpd 15 . . 3 (βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ Ο‰ β‰Ό 𝐴)
182181exlimiv 1933 . 2 (βˆƒπ‘βˆ€π‘› ∈ Ο‰ (π‘β€˜π‘›) ∈ 𝐡 β†’ Ο‰ β‰Ό 𝐴)
18348, 182syl 17 1 (Β¬ 𝐴 ∈ Fin β†’ Ο‰ β‰Ό 𝐴)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 396   ∨ w3o 1086   ∧ w3a 1087   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  {cab 2709   β‰  wne 2940  βˆ€wral 3061  Vcvv 3474   βˆ– cdif 3944   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  βˆͺ ciun 4996   class class class wbr 5147   ↦ cmpt 5230  dom cdm 5675  Ord word 6360  suc csuc 6363   Fn wfn 6535  βŸΆwf 6536  β€“1-1β†’wf1 6537  β€˜cfv 6540  Ο‰com 7851   β‰ˆ cen 8932   β‰Ό cdom 8933   β‰Ί csdm 8934  Fincfn 8935  cardccrd 9926
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 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cc 10426
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 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-oadd 8466  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-dju 9892  df-card 9930
This theorem is referenced by:  domtriom  10434
  Copyright terms: Public domain W3C validator