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

Theorem pwsdompw 10148
Description: Lemma for domtriom 10387. 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 6387 . . . . 5 (𝑛 = βˆ… β†’ suc 𝑛 = suc βˆ…)
21raleqdv 3312 . . . 4 (𝑛 = βˆ… β†’ (βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜))
3 iuneq1 4974 . . . . 5 (𝑛 = βˆ… β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) = βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜))
4 fveq2 6846 . . . . 5 (𝑛 = βˆ… β†’ (π΅β€˜π‘›) = (π΅β€˜βˆ…))
53, 4breq12d 5122 . . . 4 (𝑛 = βˆ… β†’ (βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›) ↔ βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜) β‰Ί (π΅β€˜βˆ…)))
62, 5imbi12d 345 . . 3 (𝑛 = βˆ… β†’ ((βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›)) ↔ (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜) β‰Ί (π΅β€˜βˆ…))))
7 suceq 6387 . . . . 5 (𝑛 = π‘š β†’ suc 𝑛 = suc π‘š)
87raleqdv 3312 . . . 4 (𝑛 = π‘š β†’ (βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜))
9 iuneq1 4974 . . . . 5 (𝑛 = π‘š β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) = βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜))
10 fveq2 6846 . . . . 5 (𝑛 = π‘š β†’ (π΅β€˜π‘›) = (π΅β€˜π‘š))
119, 10breq12d 5122 . . . 4 (𝑛 = π‘š β†’ (βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›) ↔ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)))
128, 11imbi12d 345 . . 3 (𝑛 = π‘š β†’ ((βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›)) ↔ (βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š))))
13 suceq 6387 . . . . 5 (𝑛 = suc π‘š β†’ suc 𝑛 = suc suc π‘š)
1413raleqdv 3312 . . . 4 (𝑛 = suc π‘š β†’ (βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜))
15 iuneq1 4974 . . . . 5 (𝑛 = suc π‘š β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) = βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜))
16 fveq2 6846 . . . . 5 (𝑛 = suc π‘š β†’ (π΅β€˜π‘›) = (π΅β€˜suc π‘š))
1715, 16breq12d 5122 . . . 4 (𝑛 = suc π‘š β†’ (βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›) ↔ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
1814, 17imbi12d 345 . . 3 (𝑛 = suc π‘š β†’ ((βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›)) ↔ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))))
19 0iun 5027 . . . 4 βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜) = βˆ…
20 0ex 5268 . . . . . . 7 βˆ… ∈ V
2120sucid 6403 . . . . . 6 βˆ… ∈ suc βˆ…
22 fveq2 6846 . . . . . . . 8 (π‘˜ = βˆ… β†’ (π΅β€˜π‘˜) = (π΅β€˜βˆ…))
23 pweq 4578 . . . . . . . 8 (π‘˜ = βˆ… β†’ 𝒫 π‘˜ = 𝒫 βˆ…)
2422, 23breq12d 5122 . . . . . . 7 (π‘˜ = βˆ… β†’ ((π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ (π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ…))
2524rspcv 3579 . . . . . 6 (βˆ… ∈ suc βˆ… β†’ (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ…))
2621, 25ax-mp 5 . . . . 5 (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ…)
2720canth2 9080 . . . . . 6 βˆ… β‰Ί 𝒫 βˆ…
28 ensym 8949 . . . . . 6 ((π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ… β†’ 𝒫 βˆ… β‰ˆ (π΅β€˜βˆ…))
29 sdomentr 9061 . . . . . 6 ((βˆ… β‰Ί 𝒫 βˆ… ∧ 𝒫 βˆ… β‰ˆ (π΅β€˜βˆ…)) β†’ βˆ… β‰Ί (π΅β€˜βˆ…))
3027, 28, 29sylancr 588 . . . . 5 ((π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ… β†’ βˆ… β‰Ί (π΅β€˜βˆ…))
3126, 30syl 17 . . . 4 (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆ… β‰Ί (π΅β€˜βˆ…))
3219, 31eqbrtrid 5144 . . 3 (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜) β‰Ί (π΅β€˜βˆ…))
33 sssucid 6401 . . . . . . . . 9 suc π‘š βŠ† suc suc π‘š
34 ssralv 4014 . . . . . . . . 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 483 . . . . . 6 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)))
39 vex 3451 . . . . . . . . . . . . 13 π‘š ∈ V
4039sucid 6403 . . . . . . . . . . . 12 π‘š ∈ suc π‘š
41 elelsuc 6394 . . . . . . . . . . . 12 (π‘š ∈ suc π‘š β†’ π‘š ∈ suc suc π‘š)
42 fveq2 6846 . . . . . . . . . . . . . 14 (π‘˜ = π‘š β†’ (π΅β€˜π‘˜) = (π΅β€˜π‘š))
43 pweq 4578 . . . . . . . . . . . . . 14 (π‘˜ = π‘š β†’ 𝒫 π‘˜ = 𝒫 π‘š)
4442, 43breq12d 5122 . . . . . . . . . . . . 13 (π‘˜ = π‘š β†’ ((π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ (π΅β€˜π‘š) β‰ˆ 𝒫 π‘š))
4544rspcv 3579 . . . . . . . . . . . 12 (π‘š ∈ suc suc π‘š β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜π‘š) β‰ˆ 𝒫 π‘š))
4640, 41, 45mp2b 10 . . . . . . . . . . 11 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜π‘š) β‰ˆ 𝒫 π‘š)
47 djuen 10113 . . . . . . . . . . 11 (((π΅β€˜π‘š) β‰ˆ 𝒫 π‘š ∧ (π΅β€˜π‘š) β‰ˆ 𝒫 π‘š) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (𝒫 π‘š βŠ” 𝒫 π‘š))
4846, 46, 47syl2anc 585 . . . . . . . . . 10 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (𝒫 π‘š βŠ” 𝒫 π‘š))
49 pwdju1 10134 . . . . . . . . . . 11 (π‘š ∈ Ο‰ β†’ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 (π‘š βŠ” 1o))
50 nnord 7814 . . . . . . . . . . . . . 14 (π‘š ∈ Ο‰ β†’ Ord π‘š)
51 ordirr 6339 . . . . . . . . . . . . . 14 (Ord π‘š β†’ Β¬ π‘š ∈ π‘š)
5250, 51syl 17 . . . . . . . . . . . . 13 (π‘š ∈ Ο‰ β†’ Β¬ π‘š ∈ π‘š)
53 dju1en 10115 . . . . . . . . . . . . 13 ((π‘š ∈ Ο‰ ∧ Β¬ π‘š ∈ π‘š) β†’ (π‘š βŠ” 1o) β‰ˆ suc π‘š)
5452, 53mpdan 686 . . . . . . . . . . . 12 (π‘š ∈ Ο‰ β†’ (π‘š βŠ” 1o) β‰ˆ suc π‘š)
55 pwen 9100 . . . . . . . . . . . 12 ((π‘š βŠ” 1o) β‰ˆ suc π‘š β†’ 𝒫 (π‘š βŠ” 1o) β‰ˆ 𝒫 suc π‘š)
5654, 55syl 17 . . . . . . . . . . 11 (π‘š ∈ Ο‰ β†’ 𝒫 (π‘š βŠ” 1o) β‰ˆ 𝒫 suc π‘š)
57 entr 8952 . . . . . . . . . . 11 (((𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 (π‘š βŠ” 1o) ∧ 𝒫 (π‘š βŠ” 1o) β‰ˆ 𝒫 suc π‘š) β†’ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 suc π‘š)
5849, 56, 57syl2anc 585 . . . . . . . . . 10 (π‘š ∈ Ο‰ β†’ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 suc π‘š)
59 entr 8952 . . . . . . . . . 10 ((((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (𝒫 π‘š βŠ” 𝒫 π‘š) ∧ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 suc π‘š) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ 𝒫 suc π‘š)
6048, 58, 59syl2an 597 . . . . . . . . 9 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ 𝒫 suc π‘š)
6139sucex 7745 . . . . . . . . . . . . 13 suc π‘š ∈ V
6261sucid 6403 . . . . . . . . . . . 12 suc π‘š ∈ suc suc π‘š
63 fveq2 6846 . . . . . . . . . . . . . 14 (π‘˜ = suc π‘š β†’ (π΅β€˜π‘˜) = (π΅β€˜suc π‘š))
64 pweq 4578 . . . . . . . . . . . . . 14 (π‘˜ = suc π‘š β†’ 𝒫 π‘˜ = 𝒫 suc π‘š)
6563, 64breq12d 5122 . . . . . . . . . . . . 13 (π‘˜ = suc π‘š β†’ ((π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ (π΅β€˜suc π‘š) β‰ˆ 𝒫 suc π‘š))
6665rspcv 3579 . . . . . . . . . . . 12 (suc π‘š ∈ suc suc π‘š β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜suc π‘š) β‰ˆ 𝒫 suc π‘š))
6762, 66ax-mp 5 . . . . . . . . . . 11 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜suc π‘š) β‰ˆ 𝒫 suc π‘š)
6867ensymd 8951 . . . . . . . . . 10 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ 𝒫 suc π‘š β‰ˆ (π΅β€˜suc π‘š))
6968adantr 482 . . . . . . . . 9 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ 𝒫 suc π‘š β‰ˆ (π΅β€˜suc π‘š))
70 entr 8952 . . . . . . . . 9 ((((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ 𝒫 suc π‘š ∧ 𝒫 suc π‘š β‰ˆ (π΅β€˜suc π‘š)) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š))
7160, 69, 70syl2anc 585 . . . . . . . 8 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š))
7271ancoms 460 . . . . . . 7 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š))
73 nnfi 9117 . . . . . . . . . . . 12 (π‘š ∈ Ο‰ β†’ π‘š ∈ Fin)
74 pwfi 9128 . . . . . . . . . . . . 13 (π‘š ∈ Fin ↔ 𝒫 π‘š ∈ Fin)
75 isfinite 9596 . . . . . . . . . . . . 13 (𝒫 π‘š ∈ Fin ↔ 𝒫 π‘š β‰Ί Ο‰)
7674, 75bitri 275 . . . . . . . . . . . 12 (π‘š ∈ Fin ↔ 𝒫 π‘š β‰Ί Ο‰)
7773, 76sylib 217 . . . . . . . . . . 11 (π‘š ∈ Ο‰ β†’ 𝒫 π‘š β‰Ί Ο‰)
78 ensdomtr 9063 . . . . . . . . . . 11 (((π΅β€˜π‘š) β‰ˆ 𝒫 π‘š ∧ 𝒫 π‘š β‰Ί Ο‰) β†’ (π΅β€˜π‘š) β‰Ί Ο‰)
7946, 77, 78syl2an 597 . . . . . . . . . 10 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ (π΅β€˜π‘š) β‰Ί Ο‰)
80 isfinite 9596 . . . . . . . . . 10 ((π΅β€˜π‘š) ∈ Fin ↔ (π΅β€˜π‘š) β‰Ί Ο‰)
8179, 80sylibr 233 . . . . . . . . 9 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ (π΅β€˜π‘š) ∈ Fin)
8281ancoms 460 . . . . . . . 8 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ (π΅β€˜π‘š) ∈ Fin)
8339, 42iunsuc 6406 . . . . . . . . . . 11 βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) = (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βˆͺ (π΅β€˜π‘š))
84 fvex 6859 . . . . . . . . . . . . 13 (π΅β€˜π‘˜) ∈ V
8539, 84iunex 7905 . . . . . . . . . . . 12 βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ V
86 fvex 6859 . . . . . . . . . . . 12 (π΅β€˜π‘š) ∈ V
87 undjudom 10111 . . . . . . . . . . . 12 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ V ∧ (π΅β€˜π‘š) ∈ V) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βˆͺ (π΅β€˜π‘š)) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)))
8885, 86, 87mp2an 691 . . . . . . . . . . 11 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βˆͺ (π΅β€˜π‘š)) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š))
8983, 88eqbrtri 5130 . . . . . . . . . 10 βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š))
90 sdomtr 9065 . . . . . . . . . . . . . . . 16 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) β‰Ί Ο‰) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί Ο‰)
9180, 90sylan2b 595 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί Ο‰)
92 isfinite 9596 . . . . . . . . . . . . . . 15 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin ↔ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί Ο‰)
9391, 92sylibr 233 . . . . . . . . . . . . . 14 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin)
94 finnum 9892 . . . . . . . . . . . . . 14 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card)
9593, 94syl 17 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card)
96 finnum 9892 . . . . . . . . . . . . . 14 ((π΅β€˜π‘š) ∈ Fin β†’ (π΅β€˜π‘š) ∈ dom card)
9796adantl 483 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (π΅β€˜π‘š) ∈ dom card)
98 cardadju 10138 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card ∧ (π΅β€˜π‘š) ∈ dom card) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))))
9995, 97, 98syl2anc 585 . . . . . . . . . . . 12 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))))
100 ficardom 9905 . . . . . . . . . . . . . . . 16 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰)
10193, 100syl 17 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰)
102 ficardom 9905 . . . . . . . . . . . . . . . 16 ((π΅β€˜π‘š) ∈ Fin β†’ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰)
103102adantl 483 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰)
104 cardid2 9897 . . . . . . . . . . . . . . . . . 18 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜))
10593, 94, 1043syl 18 . . . . . . . . . . . . . . . . 17 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜))
106 simpl 484 . . . . . . . . . . . . . . . . 17 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š))
107 cardid2 9897 . . . . . . . . . . . . . . . . . . 19 ((π΅β€˜π‘š) ∈ dom card β†’ (cardβ€˜(π΅β€˜π‘š)) β‰ˆ (π΅β€˜π‘š))
108 ensym 8949 . . . . . . . . . . . . . . . . . . 19 ((cardβ€˜(π΅β€˜π‘š)) β‰ˆ (π΅β€˜π‘š) β†’ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š)))
10996, 107, 1083syl 18 . . . . . . . . . . . . . . . . . 18 ((π΅β€˜π‘š) ∈ Fin β†’ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š)))
110109adantl 483 . . . . . . . . . . . . . . . . 17 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š)))
111 ensdomtr 9063 . . . . . . . . . . . . . . . . . 18 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∧ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (π΅β€˜π‘š))
112 sdomentr 9061 . . . . . . . . . . . . . . . . . 18 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š))) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)))
113111, 112sylan 581 . . . . . . . . . . . . . . . . 17 ((((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∧ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) ∧ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š))) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)))
114105, 106, 110, 113syl21anc 837 . . . . . . . . . . . . . . . 16 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)))
115 cardon 9888 . . . . . . . . . . . . . . . . . 18 (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ On
116 cardon 9888 . . . . . . . . . . . . . . . . . . 19 (cardβ€˜(π΅β€˜π‘š)) ∈ On
117 onenon 9893 . . . . . . . . . . . . . . . . . . 19 ((cardβ€˜(π΅β€˜π‘š)) ∈ On β†’ (cardβ€˜(π΅β€˜π‘š)) ∈ dom card)
118116, 117ax-mp 5 . . . . . . . . . . . . . . . . . 18 (cardβ€˜(π΅β€˜π‘š)) ∈ dom card
119 cardsdomel 9918 . . . . . . . . . . . . . . . . . 18 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ On ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ dom card) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(cardβ€˜(π΅β€˜π‘š)))))
120115, 118, 119mp2an 691 . . . . . . . . . . . . . . . . 17 ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(cardβ€˜(π΅β€˜π‘š))))
121 cardidm 9903 . . . . . . . . . . . . . . . . . 18 (cardβ€˜(cardβ€˜(π΅β€˜π‘š))) = (cardβ€˜(π΅β€˜π‘š))
122121eleq2i 2826 . . . . . . . . . . . . . . . . 17 ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(cardβ€˜(π΅β€˜π‘š))) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)))
123120, 122bitri 275 . . . . . . . . . . . . . . . 16 ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)))
124114, 123sylib 217 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)))
125 nnaordr 8571 . . . . . . . . . . . . . . . 16 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)) ↔ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))))
126125biimpa 478 . . . . . . . . . . . . . . 15 ((((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰) ∧ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š))) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
127101, 103, 103, 124, 126syl31anc 1374 . . . . . . . . . . . . . 14 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
128 nnacl 8562 . . . . . . . . . . . . . . . . 17 (((cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰) β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ Ο‰)
129102, 102, 128syl2anc 585 . . . . . . . . . . . . . . . 16 ((π΅β€˜π‘š) ∈ Fin β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ Ο‰)
130 cardnn 9907 . . . . . . . . . . . . . . . 16 (((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ Ο‰ β†’ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) = ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
131129, 130syl 17 . . . . . . . . . . . . . . 15 ((π΅β€˜π‘š) ∈ Fin β†’ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) = ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
132131adantl 483 . . . . . . . . . . . . . 14 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) = ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
133127, 132eleqtrrd 2837 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))))
134 cardsdomelir 9917 . . . . . . . . . . . . 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 9063 . . . . . . . . . . . 12 (((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∧ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
13799, 135, 136syl2anc 585 . . . . . . . . . . 11 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
138 cardadju 10138 . . . . . . . . . . . . . 14 (((π΅β€˜π‘š) ∈ dom card ∧ (π΅β€˜π‘š) ∈ dom card) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
13996, 96, 138syl2anc 585 . . . . . . . . . . . . 13 ((π΅β€˜π‘š) ∈ Fin β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
140139ensymd 8951 . . . . . . . . . . . 12 ((π΅β€˜π‘š) ∈ Fin β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) β‰ˆ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
141140adantl 483 . . . . . . . . . . 11 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) β‰ˆ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
142 sdomentr 9061 . . . . . . . . . . 11 (((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∧ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) β‰ˆ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
143137, 141, 142syl2anc 585 . . . . . . . . . 10 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
144 domsdomtr 9062 . . . . . . . . . 10 ((βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) ∧ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
14589, 143, 144sylancr 588 . . . . . . . . 9 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
146145expcom 415 . . . . . . . 8 ((π΅β€˜π‘š) ∈ Fin β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))))
14782, 146syl 17 . . . . . . 7 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))))
148 sdomentr 9061 . . . . . . . 8 ((βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) ∧ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))
149148expcom 415 . . . . . . 7 (((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š) β†’ (βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
15072, 147, 149sylsyld 61 . . . . . 6 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
15138, 150syld 47 . . . . 5 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
152151ex 414 . . . 4 (π‘š ∈ Ο‰ β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))))
153152com23 86 . . 3 (π‘š ∈ Ο‰ β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))))
1546, 12, 18, 32, 153finds1 7842 . 2 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›)))
155154imp 408 1 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061  Vcvv 3447   βˆͺ cun 3912   βŠ† wss 3914  βˆ…c0 4286  π’« cpw 4564  βˆͺ ciun 4958   class class class wbr 5109  dom cdm 5637  Ord word 6320  Oncon0 6321  suc csuc 6323  β€˜cfv 6500  (class class class)co 7361  Ο‰com 7806  1oc1o 8409   +o coa 8413   β‰ˆ cen 8886   β‰Ό cdom 8887   β‰Ί csdm 8888  Fincfn 8889   βŠ” cdju 9842  cardccrd 9879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-inf2 9585
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-2o 8417  df-oadd 8420  df-er 8654  df-map 8773  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-dju 9845  df-card 9883
This theorem is referenced by:  domtriomlem  10386
  Copyright terms: Public domain W3C validator