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

Theorem pwsdompw 10198
Description: Lemma for domtriom 10437. 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 3325 . . . 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 3325 . . . 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 3325 . . . 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 9129 . . . . . 6 βˆ… β‰Ί 𝒫 βˆ…
28 ensym 8998 . . . . . 6 ((π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ… β†’ 𝒫 βˆ… β‰ˆ (π΅β€˜βˆ…))
29 sdomentr 9110 . . . . . 6 ((βˆ… β‰Ί 𝒫 βˆ… ∧ 𝒫 βˆ… β‰ˆ (π΅β€˜βˆ…)) β†’ βˆ… β‰Ί (π΅β€˜βˆ…))
3027, 28, 29sylancr 587 . . . . 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 482 . . . . . 6 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)))
39 vex 3478 . . . . . . . . . . . . 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 10163 . . . . . . . . . . 11 (((π΅β€˜π‘š) β‰ˆ 𝒫 π‘š ∧ (π΅β€˜π‘š) β‰ˆ 𝒫 π‘š) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (𝒫 π‘š βŠ” 𝒫 π‘š))
4846, 46, 47syl2anc 584 . . . . . . . . . 10 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (𝒫 π‘š βŠ” 𝒫 π‘š))
49 pwdju1 10184 . . . . . . . . . . 11 (π‘š ∈ Ο‰ β†’ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 (π‘š βŠ” 1o))
50 nnord 7862 . . . . . . . . . . . . . 14 (π‘š ∈ Ο‰ β†’ Ord π‘š)
51 ordirr 6382 . . . . . . . . . . . . . 14 (Ord π‘š β†’ Β¬ π‘š ∈ π‘š)
5250, 51syl 17 . . . . . . . . . . . . 13 (π‘š ∈ Ο‰ β†’ Β¬ π‘š ∈ π‘š)
53 dju1en 10165 . . . . . . . . . . . . 13 ((π‘š ∈ Ο‰ ∧ Β¬ π‘š ∈ π‘š) β†’ (π‘š βŠ” 1o) β‰ˆ suc π‘š)
5452, 53mpdan 685 . . . . . . . . . . . 12 (π‘š ∈ Ο‰ β†’ (π‘š βŠ” 1o) β‰ˆ suc π‘š)
55 pwen 9149 . . . . . . . . . . . 12 ((π‘š βŠ” 1o) β‰ˆ suc π‘š β†’ 𝒫 (π‘š βŠ” 1o) β‰ˆ 𝒫 suc π‘š)
5654, 55syl 17 . . . . . . . . . . 11 (π‘š ∈ Ο‰ β†’ 𝒫 (π‘š βŠ” 1o) β‰ˆ 𝒫 suc π‘š)
57 entr 9001 . . . . . . . . . . 11 (((𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 (π‘š βŠ” 1o) ∧ 𝒫 (π‘š βŠ” 1o) β‰ˆ 𝒫 suc π‘š) β†’ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 suc π‘š)
5849, 56, 57syl2anc 584 . . . . . . . . . 10 (π‘š ∈ Ο‰ β†’ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 suc π‘š)
59 entr 9001 . . . . . . . . . 10 ((((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (𝒫 π‘š βŠ” 𝒫 π‘š) ∧ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 suc π‘š) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ 𝒫 suc π‘š)
6048, 58, 59syl2an 596 . . . . . . . . 9 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ 𝒫 suc π‘š)
6139sucex 7793 . . . . . . . . . . . . 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 9000 . . . . . . . . . 10 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ 𝒫 suc π‘š β‰ˆ (π΅β€˜suc π‘š))
6968adantr 481 . . . . . . . . 9 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ 𝒫 suc π‘š β‰ˆ (π΅β€˜suc π‘š))
70 entr 9001 . . . . . . . . 9 ((((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ 𝒫 suc π‘š ∧ 𝒫 suc π‘š β‰ˆ (π΅β€˜suc π‘š)) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š))
7160, 69, 70syl2anc 584 . . . . . . . 8 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š))
7271ancoms 459 . . . . . . 7 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š))
73 nnfi 9166 . . . . . . . . . . . 12 (π‘š ∈ Ο‰ β†’ π‘š ∈ Fin)
74 pwfi 9177 . . . . . . . . . . . . 13 (π‘š ∈ Fin ↔ 𝒫 π‘š ∈ Fin)
75 isfinite 9646 . . . . . . . . . . . . 13 (𝒫 π‘š ∈ Fin ↔ 𝒫 π‘š β‰Ί Ο‰)
7674, 75bitri 274 . . . . . . . . . . . 12 (π‘š ∈ Fin ↔ 𝒫 π‘š β‰Ί Ο‰)
7773, 76sylib 217 . . . . . . . . . . 11 (π‘š ∈ Ο‰ β†’ 𝒫 π‘š β‰Ί Ο‰)
78 ensdomtr 9112 . . . . . . . . . . 11 (((π΅β€˜π‘š) β‰ˆ 𝒫 π‘š ∧ 𝒫 π‘š β‰Ί Ο‰) β†’ (π΅β€˜π‘š) β‰Ί Ο‰)
7946, 77, 78syl2an 596 . . . . . . . . . 10 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ (π΅β€˜π‘š) β‰Ί Ο‰)
80 isfinite 9646 . . . . . . . . . 10 ((π΅β€˜π‘š) ∈ Fin ↔ (π΅β€˜π‘š) β‰Ί Ο‰)
8179, 80sylibr 233 . . . . . . . . 9 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ (π΅β€˜π‘š) ∈ Fin)
8281ancoms 459 . . . . . . . 8 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ (π΅β€˜π‘š) ∈ Fin)
8339, 42iunsuc 6449 . . . . . . . . . . 11 βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) = (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βˆͺ (π΅β€˜π‘š))
84 fvex 6904 . . . . . . . . . . . . 13 (π΅β€˜π‘˜) ∈ V
8539, 84iunex 7954 . . . . . . . . . . . 12 βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ V
86 fvex 6904 . . . . . . . . . . . 12 (π΅β€˜π‘š) ∈ V
87 undjudom 10161 . . . . . . . . . . . 12 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ V ∧ (π΅β€˜π‘š) ∈ V) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βˆͺ (π΅β€˜π‘š)) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)))
8885, 86, 87mp2an 690 . . . . . . . . . . 11 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βˆͺ (π΅β€˜π‘š)) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š))
8983, 88eqbrtri 5169 . . . . . . . . . 10 βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š))
90 sdomtr 9114 . . . . . . . . . . . . . . . 16 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) β‰Ί Ο‰) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί Ο‰)
9180, 90sylan2b 594 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί Ο‰)
92 isfinite 9646 . . . . . . . . . . . . . . 15 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin ↔ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί Ο‰)
9391, 92sylibr 233 . . . . . . . . . . . . . 14 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin)
94 finnum 9942 . . . . . . . . . . . . . 14 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card)
9593, 94syl 17 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card)
96 finnum 9942 . . . . . . . . . . . . . 14 ((π΅β€˜π‘š) ∈ Fin β†’ (π΅β€˜π‘š) ∈ dom card)
9796adantl 482 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (π΅β€˜π‘š) ∈ dom card)
98 cardadju 10188 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card ∧ (π΅β€˜π‘š) ∈ dom card) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))))
9995, 97, 98syl2anc 584 . . . . . . . . . . . 12 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))))
100 ficardom 9955 . . . . . . . . . . . . . . . 16 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰)
10193, 100syl 17 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰)
102 ficardom 9955 . . . . . . . . . . . . . . . 16 ((π΅β€˜π‘š) ∈ Fin β†’ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰)
103102adantl 482 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰)
104 cardid2 9947 . . . . . . . . . . . . . . . . . 18 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜))
10593, 94, 1043syl 18 . . . . . . . . . . . . . . . . 17 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜))
106 simpl 483 . . . . . . . . . . . . . . . . 17 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š))
107 cardid2 9947 . . . . . . . . . . . . . . . . . . 19 ((π΅β€˜π‘š) ∈ dom card β†’ (cardβ€˜(π΅β€˜π‘š)) β‰ˆ (π΅β€˜π‘š))
108 ensym 8998 . . . . . . . . . . . . . . . . . . 19 ((cardβ€˜(π΅β€˜π‘š)) β‰ˆ (π΅β€˜π‘š) β†’ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š)))
10996, 107, 1083syl 18 . . . . . . . . . . . . . . . . . 18 ((π΅β€˜π‘š) ∈ Fin β†’ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š)))
110109adantl 482 . . . . . . . . . . . . . . . . 17 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š)))
111 ensdomtr 9112 . . . . . . . . . . . . . . . . . 18 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∧ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (π΅β€˜π‘š))
112 sdomentr 9110 . . . . . . . . . . . . . . . . . 18 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š))) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)))
113111, 112sylan 580 . . . . . . . . . . . . . . . . 17 ((((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∧ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) ∧ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š))) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)))
114105, 106, 110, 113syl21anc 836 . . . . . . . . . . . . . . . 16 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)))
115 cardon 9938 . . . . . . . . . . . . . . . . . 18 (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ On
116 cardon 9938 . . . . . . . . . . . . . . . . . . 19 (cardβ€˜(π΅β€˜π‘š)) ∈ On
117 onenon 9943 . . . . . . . . . . . . . . . . . . 19 ((cardβ€˜(π΅β€˜π‘š)) ∈ On β†’ (cardβ€˜(π΅β€˜π‘š)) ∈ dom card)
118116, 117ax-mp 5 . . . . . . . . . . . . . . . . . 18 (cardβ€˜(π΅β€˜π‘š)) ∈ dom card
119 cardsdomel 9968 . . . . . . . . . . . . . . . . . 18 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ On ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ dom card) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(cardβ€˜(π΅β€˜π‘š)))))
120115, 118, 119mp2an 690 . . . . . . . . . . . . . . . . 17 ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(cardβ€˜(π΅β€˜π‘š))))
121 cardidm 9953 . . . . . . . . . . . . . . . . . 18 (cardβ€˜(cardβ€˜(π΅β€˜π‘š))) = (cardβ€˜(π΅β€˜π‘š))
122121eleq2i 2825 . . . . . . . . . . . . . . . . 17 ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(cardβ€˜(π΅β€˜π‘š))) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)))
123120, 122bitri 274 . . . . . . . . . . . . . . . 16 ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)))
124114, 123sylib 217 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)))
125 nnaordr 8619 . . . . . . . . . . . . . . . 16 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)) ↔ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))))
126125biimpa 477 . . . . . . . . . . . . . . 15 ((((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰) ∧ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š))) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
127101, 103, 103, 124, 126syl31anc 1373 . . . . . . . . . . . . . 14 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
128 nnacl 8610 . . . . . . . . . . . . . . . . 17 (((cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰) β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ Ο‰)
129102, 102, 128syl2anc 584 . . . . . . . . . . . . . . . 16 ((π΅β€˜π‘š) ∈ Fin β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ Ο‰)
130 cardnn 9957 . . . . . . . . . . . . . . . 16 (((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ Ο‰ β†’ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) = ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
131129, 130syl 17 . . . . . . . . . . . . . . 15 ((π΅β€˜π‘š) ∈ Fin β†’ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) = ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
132131adantl 482 . . . . . . . . . . . . . 14 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) = ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
133127, 132eleqtrrd 2836 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))))
134 cardsdomelir 9967 . . . . . . . . . . . . 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 9112 . . . . . . . . . . . 12 (((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∧ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
13799, 135, 136syl2anc 584 . . . . . . . . . . 11 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
138 cardadju 10188 . . . . . . . . . . . . . 14 (((π΅β€˜π‘š) ∈ dom card ∧ (π΅β€˜π‘š) ∈ dom card) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
13996, 96, 138syl2anc 584 . . . . . . . . . . . . 13 ((π΅β€˜π‘š) ∈ Fin β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
140139ensymd 9000 . . . . . . . . . . . 12 ((π΅β€˜π‘š) ∈ Fin β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) β‰ˆ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
141140adantl 482 . . . . . . . . . . 11 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) β‰ˆ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
142 sdomentr 9110 . . . . . . . . . . 11 (((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∧ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) β‰ˆ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
143137, 141, 142syl2anc 584 . . . . . . . . . 10 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
144 domsdomtr 9111 . . . . . . . . . 10 ((βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) ∧ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
14589, 143, 144sylancr 587 . . . . . . . . 9 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
146145expcom 414 . . . . . . . 8 ((π΅β€˜π‘š) ∈ Fin β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))))
14782, 146syl 17 . . . . . . 7 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))))
148 sdomentr 9110 . . . . . . . 8 ((βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) ∧ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))
149148expcom 414 . . . . . . 7 (((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š) β†’ (βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
15072, 147, 149sylsyld 61 . . . . . 6 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
15138, 150syld 47 . . . . 5 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
152151ex 413 . . . 4 (π‘š ∈ Ο‰ β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))))
153152com23 86 . . 3 (π‘š ∈ Ο‰ β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))))
1546, 12, 18, 32, 153finds1 7891 . 2 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›)))
155154imp 407 1 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  Vcvv 3474   βˆͺ 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 7408  Ο‰com 7854  1oc1o 8458   +o coa 8462   β‰ˆ cen 8935   β‰Ό cdom 8936   β‰Ί csdm 8937  Fincfn 8938   βŠ” cdju 9892  cardccrd 9929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-inf2 9635
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-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 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-1st 7974  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-2o 8466  df-oadd 8469  df-er 8702  df-map 8821  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-dju 9895  df-card 9933
This theorem is referenced by:  domtriomlem  10436
  Copyright terms: Public domain W3C validator