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

Theorem pwsdompw 10202
Description: Lemma for domtriom 10441. This is the equinumerosity version of the algebraic identity Ξ£π‘˜ ∈ 𝑛(2β†‘π‘˜) = (2↑𝑛) βˆ’ 1. (Contributed by Mario Carneiro, 7-Feb-2013.)
Assertion
Ref Expression
pwsdompw ((𝑛 ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›))
Distinct variable group:   𝐡,π‘˜,𝑛

Proof of Theorem pwsdompw
Dummy variable π‘š is distinct from all other variables.
StepHypRef Expression
1 suceq 6430 . . . . 5 (𝑛 = βˆ… β†’ suc 𝑛 = suc βˆ…)
21raleqdv 3324 . . . 4 (𝑛 = βˆ… β†’ (βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜))
3 iuneq1 5013 . . . . 5 (𝑛 = βˆ… β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) = βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜))
4 fveq2 6891 . . . . 5 (𝑛 = βˆ… β†’ (π΅β€˜π‘›) = (π΅β€˜βˆ…))
53, 4breq12d 5161 . . . 4 (𝑛 = βˆ… β†’ (βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›) ↔ βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜) β‰Ί (π΅β€˜βˆ…)))
62, 5imbi12d 344 . . 3 (𝑛 = βˆ… β†’ ((βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›)) ↔ (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜) β‰Ί (π΅β€˜βˆ…))))
7 suceq 6430 . . . . 5 (𝑛 = π‘š β†’ suc 𝑛 = suc π‘š)
87raleqdv 3324 . . . 4 (𝑛 = π‘š β†’ (βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜))
9 iuneq1 5013 . . . . 5 (𝑛 = π‘š β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) = βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜))
10 fveq2 6891 . . . . 5 (𝑛 = π‘š β†’ (π΅β€˜π‘›) = (π΅β€˜π‘š))
119, 10breq12d 5161 . . . 4 (𝑛 = π‘š β†’ (βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›) ↔ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)))
128, 11imbi12d 344 . . 3 (𝑛 = π‘š β†’ ((βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›)) ↔ (βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š))))
13 suceq 6430 . . . . 5 (𝑛 = suc π‘š β†’ suc 𝑛 = suc suc π‘š)
1413raleqdv 3324 . . . 4 (𝑛 = suc π‘š β†’ (βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜))
15 iuneq1 5013 . . . . 5 (𝑛 = suc π‘š β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) = βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜))
16 fveq2 6891 . . . . 5 (𝑛 = suc π‘š β†’ (π΅β€˜π‘›) = (π΅β€˜suc π‘š))
1715, 16breq12d 5161 . . . 4 (𝑛 = suc π‘š β†’ (βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›) ↔ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
1814, 17imbi12d 344 . . 3 (𝑛 = suc π‘š β†’ ((βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›)) ↔ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))))
19 0iun 5066 . . . 4 βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜) = βˆ…
20 0ex 5307 . . . . . . 7 βˆ… ∈ V
2120sucid 6446 . . . . . 6 βˆ… ∈ suc βˆ…
22 fveq2 6891 . . . . . . . 8 (π‘˜ = βˆ… β†’ (π΅β€˜π‘˜) = (π΅β€˜βˆ…))
23 pweq 4616 . . . . . . . 8 (π‘˜ = βˆ… β†’ 𝒫 π‘˜ = 𝒫 βˆ…)
2422, 23breq12d 5161 . . . . . . 7 (π‘˜ = βˆ… β†’ ((π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ (π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ…))
2524rspcv 3608 . . . . . 6 (βˆ… ∈ suc βˆ… β†’ (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ…))
2621, 25ax-mp 5 . . . . 5 (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ…)
2720canth2 9133 . . . . . 6 βˆ… β‰Ί 𝒫 βˆ…
28 ensym 9002 . . . . . 6 ((π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ… β†’ 𝒫 βˆ… β‰ˆ (π΅β€˜βˆ…))
29 sdomentr 9114 . . . . . 6 ((βˆ… β‰Ί 𝒫 βˆ… ∧ 𝒫 βˆ… β‰ˆ (π΅β€˜βˆ…)) β†’ βˆ… β‰Ί (π΅β€˜βˆ…))
3027, 28, 29sylancr 586 . . . . 5 ((π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ… β†’ βˆ… β‰Ί (π΅β€˜βˆ…))
3126, 30syl 17 . . . 4 (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆ… β‰Ί (π΅β€˜βˆ…))
3219, 31eqbrtrid 5183 . . 3 (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜) β‰Ί (π΅β€˜βˆ…))
33 sssucid 6444 . . . . . . . . 9 suc π‘š βŠ† suc suc π‘š
34 ssralv 4050 . . . . . . . . 9 (suc π‘š βŠ† suc suc π‘š β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜))
3533, 34ax-mp 5 . . . . . . . 8 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜)
36 pm2.27 42 . . . . . . . 8 (βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)))
3735, 36syl 17 . . . . . . 7 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)))
3837adantl 481 . . . . . 6 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)))
39 vex 3477 . . . . . . . . . . . . 13 π‘š ∈ V
4039sucid 6446 . . . . . . . . . . . 12 π‘š ∈ suc π‘š
41 elelsuc 6437 . . . . . . . . . . . 12 (π‘š ∈ suc π‘š β†’ π‘š ∈ suc suc π‘š)
42 fveq2 6891 . . . . . . . . . . . . . 14 (π‘˜ = π‘š β†’ (π΅β€˜π‘˜) = (π΅β€˜π‘š))
43 pweq 4616 . . . . . . . . . . . . . 14 (π‘˜ = π‘š β†’ 𝒫 π‘˜ = 𝒫 π‘š)
4442, 43breq12d 5161 . . . . . . . . . . . . 13 (π‘˜ = π‘š β†’ ((π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ (π΅β€˜π‘š) β‰ˆ 𝒫 π‘š))
4544rspcv 3608 . . . . . . . . . . . 12 (π‘š ∈ suc suc π‘š β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜π‘š) β‰ˆ 𝒫 π‘š))
4640, 41, 45mp2b 10 . . . . . . . . . . 11 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜π‘š) β‰ˆ 𝒫 π‘š)
47 djuen 10167 . . . . . . . . . . 11 (((π΅β€˜π‘š) β‰ˆ 𝒫 π‘š ∧ (π΅β€˜π‘š) β‰ˆ 𝒫 π‘š) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (𝒫 π‘š βŠ” 𝒫 π‘š))
4846, 46, 47syl2anc 583 . . . . . . . . . 10 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (𝒫 π‘š βŠ” 𝒫 π‘š))
49 pwdju1 10188 . . . . . . . . . . 11 (π‘š ∈ Ο‰ β†’ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 (π‘š βŠ” 1o))
50 nnord 7866 . . . . . . . . . . . . . 14 (π‘š ∈ Ο‰ β†’ Ord π‘š)
51 ordirr 6382 . . . . . . . . . . . . . 14 (Ord π‘š β†’ Β¬ π‘š ∈ π‘š)
5250, 51syl 17 . . . . . . . . . . . . 13 (π‘š ∈ Ο‰ β†’ Β¬ π‘š ∈ π‘š)
53 dju1en 10169 . . . . . . . . . . . . 13 ((π‘š ∈ Ο‰ ∧ Β¬ π‘š ∈ π‘š) β†’ (π‘š βŠ” 1o) β‰ˆ suc π‘š)
5452, 53mpdan 684 . . . . . . . . . . . 12 (π‘š ∈ Ο‰ β†’ (π‘š βŠ” 1o) β‰ˆ suc π‘š)
55 pwen 9153 . . . . . . . . . . . 12 ((π‘š βŠ” 1o) β‰ˆ suc π‘š β†’ 𝒫 (π‘š βŠ” 1o) β‰ˆ 𝒫 suc π‘š)
5654, 55syl 17 . . . . . . . . . . 11 (π‘š ∈ Ο‰ β†’ 𝒫 (π‘š βŠ” 1o) β‰ˆ 𝒫 suc π‘š)
57 entr 9005 . . . . . . . . . . 11 (((𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 (π‘š βŠ” 1o) ∧ 𝒫 (π‘š βŠ” 1o) β‰ˆ 𝒫 suc π‘š) β†’ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 suc π‘š)
5849, 56, 57syl2anc 583 . . . . . . . . . 10 (π‘š ∈ Ο‰ β†’ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 suc π‘š)
59 entr 9005 . . . . . . . . . 10 ((((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (𝒫 π‘š βŠ” 𝒫 π‘š) ∧ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 suc π‘š) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ 𝒫 suc π‘š)
6048, 58, 59syl2an 595 . . . . . . . . 9 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ 𝒫 suc π‘š)
6139sucex 7797 . . . . . . . . . . . . 13 suc π‘š ∈ V
6261sucid 6446 . . . . . . . . . . . 12 suc π‘š ∈ suc suc π‘š
63 fveq2 6891 . . . . . . . . . . . . . 14 (π‘˜ = suc π‘š β†’ (π΅β€˜π‘˜) = (π΅β€˜suc π‘š))
64 pweq 4616 . . . . . . . . . . . . . 14 (π‘˜ = suc π‘š β†’ 𝒫 π‘˜ = 𝒫 suc π‘š)
6563, 64breq12d 5161 . . . . . . . . . . . . 13 (π‘˜ = suc π‘š β†’ ((π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ (π΅β€˜suc π‘š) β‰ˆ 𝒫 suc π‘š))
6665rspcv 3608 . . . . . . . . . . . 12 (suc π‘š ∈ suc suc π‘š β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜suc π‘š) β‰ˆ 𝒫 suc π‘š))
6762, 66ax-mp 5 . . . . . . . . . . 11 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜suc π‘š) β‰ˆ 𝒫 suc π‘š)
6867ensymd 9004 . . . . . . . . . 10 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ 𝒫 suc π‘š β‰ˆ (π΅β€˜suc π‘š))
6968adantr 480 . . . . . . . . 9 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ 𝒫 suc π‘š β‰ˆ (π΅β€˜suc π‘š))
70 entr 9005 . . . . . . . . 9 ((((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ 𝒫 suc π‘š ∧ 𝒫 suc π‘š β‰ˆ (π΅β€˜suc π‘š)) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š))
7160, 69, 70syl2anc 583 . . . . . . . 8 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š))
7271ancoms 458 . . . . . . 7 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š))
73 nnfi 9170 . . . . . . . . . . . 12 (π‘š ∈ Ο‰ β†’ π‘š ∈ Fin)
74 pwfi 9181 . . . . . . . . . . . . 13 (π‘š ∈ Fin ↔ 𝒫 π‘š ∈ Fin)
75 isfinite 9650 . . . . . . . . . . . . 13 (𝒫 π‘š ∈ Fin ↔ 𝒫 π‘š β‰Ί Ο‰)
7674, 75bitri 275 . . . . . . . . . . . 12 (π‘š ∈ Fin ↔ 𝒫 π‘š β‰Ί Ο‰)
7773, 76sylib 217 . . . . . . . . . . 11 (π‘š ∈ Ο‰ β†’ 𝒫 π‘š β‰Ί Ο‰)
78 ensdomtr 9116 . . . . . . . . . . 11 (((π΅β€˜π‘š) β‰ˆ 𝒫 π‘š ∧ 𝒫 π‘š β‰Ί Ο‰) β†’ (π΅β€˜π‘š) β‰Ί Ο‰)
7946, 77, 78syl2an 595 . . . . . . . . . 10 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ (π΅β€˜π‘š) β‰Ί Ο‰)
80 isfinite 9650 . . . . . . . . . 10 ((π΅β€˜π‘š) ∈ Fin ↔ (π΅β€˜π‘š) β‰Ί Ο‰)
8179, 80sylibr 233 . . . . . . . . 9 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ (π΅β€˜π‘š) ∈ Fin)
8281ancoms 458 . . . . . . . 8 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ (π΅β€˜π‘š) ∈ Fin)
8339, 42iunsuc 6449 . . . . . . . . . . 11 βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) = (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βˆͺ (π΅β€˜π‘š))
84 fvex 6904 . . . . . . . . . . . . 13 (π΅β€˜π‘˜) ∈ V
8539, 84iunex 7958 . . . . . . . . . . . 12 βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ V
86 fvex 6904 . . . . . . . . . . . 12 (π΅β€˜π‘š) ∈ V
87 undjudom 10165 . . . . . . . . . . . 12 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ V ∧ (π΅β€˜π‘š) ∈ V) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βˆͺ (π΅β€˜π‘š)) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)))
8885, 86, 87mp2an 689 . . . . . . . . . . 11 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βˆͺ (π΅β€˜π‘š)) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š))
8983, 88eqbrtri 5169 . . . . . . . . . 10 βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š))
90 sdomtr 9118 . . . . . . . . . . . . . . . 16 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) β‰Ί Ο‰) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί Ο‰)
9180, 90sylan2b 593 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί Ο‰)
92 isfinite 9650 . . . . . . . . . . . . . . 15 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin ↔ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί Ο‰)
9391, 92sylibr 233 . . . . . . . . . . . . . 14 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin)
94 finnum 9946 . . . . . . . . . . . . . 14 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card)
9593, 94syl 17 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card)
96 finnum 9946 . . . . . . . . . . . . . 14 ((π΅β€˜π‘š) ∈ Fin β†’ (π΅β€˜π‘š) ∈ dom card)
9796adantl 481 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (π΅β€˜π‘š) ∈ dom card)
98 cardadju 10192 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card ∧ (π΅β€˜π‘š) ∈ dom card) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))))
9995, 97, 98syl2anc 583 . . . . . . . . . . . 12 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))))
100 ficardom 9959 . . . . . . . . . . . . . . . 16 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰)
10193, 100syl 17 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰)
102 ficardom 9959 . . . . . . . . . . . . . . . 16 ((π΅β€˜π‘š) ∈ Fin β†’ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰)
103102adantl 481 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰)
104 cardid2 9951 . . . . . . . . . . . . . . . . . 18 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜))
10593, 94, 1043syl 18 . . . . . . . . . . . . . . . . 17 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜))
106 simpl 482 . . . . . . . . . . . . . . . . 17 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š))
107 cardid2 9951 . . . . . . . . . . . . . . . . . . 19 ((π΅β€˜π‘š) ∈ dom card β†’ (cardβ€˜(π΅β€˜π‘š)) β‰ˆ (π΅β€˜π‘š))
108 ensym 9002 . . . . . . . . . . . . . . . . . . 19 ((cardβ€˜(π΅β€˜π‘š)) β‰ˆ (π΅β€˜π‘š) β†’ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š)))
10996, 107, 1083syl 18 . . . . . . . . . . . . . . . . . 18 ((π΅β€˜π‘š) ∈ Fin β†’ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š)))
110109adantl 481 . . . . . . . . . . . . . . . . 17 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š)))
111 ensdomtr 9116 . . . . . . . . . . . . . . . . . 18 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∧ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (π΅β€˜π‘š))
112 sdomentr 9114 . . . . . . . . . . . . . . . . . 18 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š))) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)))
113111, 112sylan 579 . . . . . . . . . . . . . . . . 17 ((((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∧ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) ∧ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š))) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)))
114105, 106, 110, 113syl21anc 835 . . . . . . . . . . . . . . . 16 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)))
115 cardon 9942 . . . . . . . . . . . . . . . . . 18 (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ On
116 cardon 9942 . . . . . . . . . . . . . . . . . . 19 (cardβ€˜(π΅β€˜π‘š)) ∈ On
117 onenon 9947 . . . . . . . . . . . . . . . . . . 19 ((cardβ€˜(π΅β€˜π‘š)) ∈ On β†’ (cardβ€˜(π΅β€˜π‘š)) ∈ dom card)
118116, 117ax-mp 5 . . . . . . . . . . . . . . . . . 18 (cardβ€˜(π΅β€˜π‘š)) ∈ dom card
119 cardsdomel 9972 . . . . . . . . . . . . . . . . . 18 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ On ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ dom card) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(cardβ€˜(π΅β€˜π‘š)))))
120115, 118, 119mp2an 689 . . . . . . . . . . . . . . . . 17 ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(cardβ€˜(π΅β€˜π‘š))))
121 cardidm 9957 . . . . . . . . . . . . . . . . . 18 (cardβ€˜(cardβ€˜(π΅β€˜π‘š))) = (cardβ€˜(π΅β€˜π‘š))
122121eleq2i 2824 . . . . . . . . . . . . . . . . 17 ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(cardβ€˜(π΅β€˜π‘š))) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)))
123120, 122bitri 275 . . . . . . . . . . . . . . . 16 ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)))
124114, 123sylib 217 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)))
125 nnaordr 8623 . . . . . . . . . . . . . . . 16 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)) ↔ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))))
126125biimpa 476 . . . . . . . . . . . . . . 15 ((((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰) ∧ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š))) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
127101, 103, 103, 124, 126syl31anc 1372 . . . . . . . . . . . . . 14 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
128 nnacl 8614 . . . . . . . . . . . . . . . . 17 (((cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰) β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ Ο‰)
129102, 102, 128syl2anc 583 . . . . . . . . . . . . . . . 16 ((π΅β€˜π‘š) ∈ Fin β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ Ο‰)
130 cardnn 9961 . . . . . . . . . . . . . . . 16 (((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ Ο‰ β†’ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) = ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
131129, 130syl 17 . . . . . . . . . . . . . . 15 ((π΅β€˜π‘š) ∈ Fin β†’ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) = ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
132131adantl 481 . . . . . . . . . . . . . 14 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) = ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
133127, 132eleqtrrd 2835 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))))
134 cardsdomelir 9971 . . . . . . . . . . . . 13 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
135133, 134syl 17 . . . . . . . . . . . 12 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
136 ensdomtr 9116 . . . . . . . . . . . 12 (((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∧ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
13799, 135, 136syl2anc 583 . . . . . . . . . . 11 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
138 cardadju 10192 . . . . . . . . . . . . . 14 (((π΅β€˜π‘š) ∈ dom card ∧ (π΅β€˜π‘š) ∈ dom card) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
13996, 96, 138syl2anc 583 . . . . . . . . . . . . 13 ((π΅β€˜π‘š) ∈ Fin β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
140139ensymd 9004 . . . . . . . . . . . 12 ((π΅β€˜π‘š) ∈ Fin β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) β‰ˆ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
141140adantl 481 . . . . . . . . . . 11 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) β‰ˆ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
142 sdomentr 9114 . . . . . . . . . . 11 (((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∧ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) β‰ˆ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
143137, 141, 142syl2anc 583 . . . . . . . . . 10 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
144 domsdomtr 9115 . . . . . . . . . 10 ((βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) ∧ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
14589, 143, 144sylancr 586 . . . . . . . . 9 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
146145expcom 413 . . . . . . . 8 ((π΅β€˜π‘š) ∈ Fin β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))))
14782, 146syl 17 . . . . . . 7 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))))
148 sdomentr 9114 . . . . . . . 8 ((βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) ∧ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))
149148expcom 413 . . . . . . 7 (((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š) β†’ (βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
15072, 147, 149sylsyld 61 . . . . . 6 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
15138, 150syld 47 . . . . 5 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
152151ex 412 . . . 4 (π‘š ∈ Ο‰ β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))))
153152com23 86 . . 3 (π‘š ∈ Ο‰ β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))))
1546, 12, 18, 32, 153finds1 7895 . 2 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›)))
155154imp 406 1 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  βˆ€wral 3060  Vcvv 3473   βˆͺ cun 3946   βŠ† wss 3948  βˆ…c0 4322  π’« cpw 4602  βˆͺ ciun 4997   class class class wbr 5148  dom cdm 5676  Ord word 6363  Oncon0 6364  suc csuc 6366  β€˜cfv 6543  (class class class)co 7412  Ο‰com 7858  1oc1o 8462   +o coa 8466   β‰ˆ cen 8939   β‰Ό cdom 8940   β‰Ί csdm 8941  Fincfn 8942   βŠ” cdju 9896  cardccrd 9933
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 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7728  ax-inf2 9639
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 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-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-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-1st 7978  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-1o 8469  df-2o 8470  df-oadd 8473  df-er 8706  df-map 8825  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-dju 9899  df-card 9937
This theorem is referenced by:  domtriomlem  10440
  Copyright terms: Public domain W3C validator