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

Theorem pwsdompw 10201
Description: Lemma for domtriom 10440. 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 6429 . . . . 5 (𝑛 = βˆ… β†’ suc 𝑛 = suc βˆ…)
21raleqdv 3323 . . . 4 (𝑛 = βˆ… β†’ (βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜))
3 iuneq1 5012 . . . . 5 (𝑛 = βˆ… β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) = βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜))
4 fveq2 6890 . . . . 5 (𝑛 = βˆ… β†’ (π΅β€˜π‘›) = (π΅β€˜βˆ…))
53, 4breq12d 5160 . . . 4 (𝑛 = βˆ… β†’ (βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›) ↔ βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜) β‰Ί (π΅β€˜βˆ…)))
62, 5imbi12d 343 . . 3 (𝑛 = βˆ… β†’ ((βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›)) ↔ (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜) β‰Ί (π΅β€˜βˆ…))))
7 suceq 6429 . . . . 5 (𝑛 = π‘š β†’ suc 𝑛 = suc π‘š)
87raleqdv 3323 . . . 4 (𝑛 = π‘š β†’ (βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜))
9 iuneq1 5012 . . . . 5 (𝑛 = π‘š β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) = βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜))
10 fveq2 6890 . . . . 5 (𝑛 = π‘š β†’ (π΅β€˜π‘›) = (π΅β€˜π‘š))
119, 10breq12d 5160 . . . 4 (𝑛 = π‘š β†’ (βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›) ↔ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)))
128, 11imbi12d 343 . . 3 (𝑛 = π‘š β†’ ((βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›)) ↔ (βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š))))
13 suceq 6429 . . . . 5 (𝑛 = suc π‘š β†’ suc 𝑛 = suc suc π‘š)
1413raleqdv 3323 . . . 4 (𝑛 = suc π‘š β†’ (βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜))
15 iuneq1 5012 . . . . 5 (𝑛 = suc π‘š β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) = βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜))
16 fveq2 6890 . . . . 5 (𝑛 = suc π‘š β†’ (π΅β€˜π‘›) = (π΅β€˜suc π‘š))
1715, 16breq12d 5160 . . . 4 (𝑛 = suc π‘š β†’ (βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›) ↔ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
1814, 17imbi12d 343 . . 3 (𝑛 = suc π‘š β†’ ((βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›)) ↔ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))))
19 0iun 5065 . . . 4 βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜) = βˆ…
20 0ex 5306 . . . . . . 7 βˆ… ∈ V
2120sucid 6445 . . . . . 6 βˆ… ∈ suc βˆ…
22 fveq2 6890 . . . . . . . 8 (π‘˜ = βˆ… β†’ (π΅β€˜π‘˜) = (π΅β€˜βˆ…))
23 pweq 4615 . . . . . . . 8 (π‘˜ = βˆ… β†’ 𝒫 π‘˜ = 𝒫 βˆ…)
2422, 23breq12d 5160 . . . . . . 7 (π‘˜ = βˆ… β†’ ((π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ (π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ…))
2524rspcv 3607 . . . . . 6 (βˆ… ∈ suc βˆ… β†’ (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ…))
2621, 25ax-mp 5 . . . . 5 (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ…)
2720canth2 9132 . . . . . 6 βˆ… β‰Ί 𝒫 βˆ…
28 ensym 9001 . . . . . 6 ((π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ… β†’ 𝒫 βˆ… β‰ˆ (π΅β€˜βˆ…))
29 sdomentr 9113 . . . . . 6 ((βˆ… β‰Ί 𝒫 βˆ… ∧ 𝒫 βˆ… β‰ˆ (π΅β€˜βˆ…)) β†’ βˆ… β‰Ί (π΅β€˜βˆ…))
3027, 28, 29sylancr 585 . . . . 5 ((π΅β€˜βˆ…) β‰ˆ 𝒫 βˆ… β†’ βˆ… β‰Ί (π΅β€˜βˆ…))
3126, 30syl 17 . . . 4 (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆ… β‰Ί (π΅β€˜βˆ…))
3219, 31eqbrtrid 5182 . . 3 (βˆ€π‘˜ ∈ suc βˆ…(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ βˆ… (π΅β€˜π‘˜) β‰Ί (π΅β€˜βˆ…))
33 sssucid 6443 . . . . . . . . 9 suc π‘š βŠ† suc suc π‘š
34 ssralv 4049 . . . . . . . . 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 480 . . . . . 6 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)))
39 vex 3476 . . . . . . . . . . . . 13 π‘š ∈ V
4039sucid 6445 . . . . . . . . . . . 12 π‘š ∈ suc π‘š
41 elelsuc 6436 . . . . . . . . . . . 12 (π‘š ∈ suc π‘š β†’ π‘š ∈ suc suc π‘š)
42 fveq2 6890 . . . . . . . . . . . . . 14 (π‘˜ = π‘š β†’ (π΅β€˜π‘˜) = (π΅β€˜π‘š))
43 pweq 4615 . . . . . . . . . . . . . 14 (π‘˜ = π‘š β†’ 𝒫 π‘˜ = 𝒫 π‘š)
4442, 43breq12d 5160 . . . . . . . . . . . . 13 (π‘˜ = π‘š β†’ ((π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ (π΅β€˜π‘š) β‰ˆ 𝒫 π‘š))
4544rspcv 3607 . . . . . . . . . . . 12 (π‘š ∈ suc suc π‘š β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜π‘š) β‰ˆ 𝒫 π‘š))
4640, 41, 45mp2b 10 . . . . . . . . . . 11 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜π‘š) β‰ˆ 𝒫 π‘š)
47 djuen 10166 . . . . . . . . . . 11 (((π΅β€˜π‘š) β‰ˆ 𝒫 π‘š ∧ (π΅β€˜π‘š) β‰ˆ 𝒫 π‘š) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (𝒫 π‘š βŠ” 𝒫 π‘š))
4846, 46, 47syl2anc 582 . . . . . . . . . 10 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (𝒫 π‘š βŠ” 𝒫 π‘š))
49 pwdju1 10187 . . . . . . . . . . 11 (π‘š ∈ Ο‰ β†’ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 (π‘š βŠ” 1o))
50 nnord 7865 . . . . . . . . . . . . . 14 (π‘š ∈ Ο‰ β†’ Ord π‘š)
51 ordirr 6381 . . . . . . . . . . . . . 14 (Ord π‘š β†’ Β¬ π‘š ∈ π‘š)
5250, 51syl 17 . . . . . . . . . . . . 13 (π‘š ∈ Ο‰ β†’ Β¬ π‘š ∈ π‘š)
53 dju1en 10168 . . . . . . . . . . . . 13 ((π‘š ∈ Ο‰ ∧ Β¬ π‘š ∈ π‘š) β†’ (π‘š βŠ” 1o) β‰ˆ suc π‘š)
5452, 53mpdan 683 . . . . . . . . . . . 12 (π‘š ∈ Ο‰ β†’ (π‘š βŠ” 1o) β‰ˆ suc π‘š)
55 pwen 9152 . . . . . . . . . . . 12 ((π‘š βŠ” 1o) β‰ˆ suc π‘š β†’ 𝒫 (π‘š βŠ” 1o) β‰ˆ 𝒫 suc π‘š)
5654, 55syl 17 . . . . . . . . . . 11 (π‘š ∈ Ο‰ β†’ 𝒫 (π‘š βŠ” 1o) β‰ˆ 𝒫 suc π‘š)
57 entr 9004 . . . . . . . . . . 11 (((𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 (π‘š βŠ” 1o) ∧ 𝒫 (π‘š βŠ” 1o) β‰ˆ 𝒫 suc π‘š) β†’ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 suc π‘š)
5849, 56, 57syl2anc 582 . . . . . . . . . 10 (π‘š ∈ Ο‰ β†’ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 suc π‘š)
59 entr 9004 . . . . . . . . . 10 ((((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (𝒫 π‘š βŠ” 𝒫 π‘š) ∧ (𝒫 π‘š βŠ” 𝒫 π‘š) β‰ˆ 𝒫 suc π‘š) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ 𝒫 suc π‘š)
6048, 58, 59syl2an 594 . . . . . . . . 9 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ 𝒫 suc π‘š)
6139sucex 7796 . . . . . . . . . . . . 13 suc π‘š ∈ V
6261sucid 6445 . . . . . . . . . . . 12 suc π‘š ∈ suc suc π‘š
63 fveq2 6890 . . . . . . . . . . . . . 14 (π‘˜ = suc π‘š β†’ (π΅β€˜π‘˜) = (π΅β€˜suc π‘š))
64 pweq 4615 . . . . . . . . . . . . . 14 (π‘˜ = suc π‘š β†’ 𝒫 π‘˜ = 𝒫 suc π‘š)
6563, 64breq12d 5160 . . . . . . . . . . . . 13 (π‘˜ = suc π‘š β†’ ((π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ↔ (π΅β€˜suc π‘š) β‰ˆ 𝒫 suc π‘š))
6665rspcv 3607 . . . . . . . . . . . 12 (suc π‘š ∈ suc suc π‘š β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜suc π‘š) β‰ˆ 𝒫 suc π‘š))
6762, 66ax-mp 5 . . . . . . . . . . 11 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ (π΅β€˜suc π‘š) β‰ˆ 𝒫 suc π‘š)
6867ensymd 9003 . . . . . . . . . 10 (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ 𝒫 suc π‘š β‰ˆ (π΅β€˜suc π‘š))
6968adantr 479 . . . . . . . . 9 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ 𝒫 suc π‘š β‰ˆ (π΅β€˜suc π‘š))
70 entr 9004 . . . . . . . . 9 ((((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ 𝒫 suc π‘š ∧ 𝒫 suc π‘š β‰ˆ (π΅β€˜suc π‘š)) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š))
7160, 69, 70syl2anc 582 . . . . . . . 8 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š))
7271ancoms 457 . . . . . . 7 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š))
73 nnfi 9169 . . . . . . . . . . . 12 (π‘š ∈ Ο‰ β†’ π‘š ∈ Fin)
74 pwfi 9180 . . . . . . . . . . . . 13 (π‘š ∈ Fin ↔ 𝒫 π‘š ∈ Fin)
75 isfinite 9649 . . . . . . . . . . . . 13 (𝒫 π‘š ∈ Fin ↔ 𝒫 π‘š β‰Ί Ο‰)
7674, 75bitri 274 . . . . . . . . . . . 12 (π‘š ∈ Fin ↔ 𝒫 π‘š β‰Ί Ο‰)
7773, 76sylib 217 . . . . . . . . . . 11 (π‘š ∈ Ο‰ β†’ 𝒫 π‘š β‰Ί Ο‰)
78 ensdomtr 9115 . . . . . . . . . . 11 (((π΅β€˜π‘š) β‰ˆ 𝒫 π‘š ∧ 𝒫 π‘š β‰Ί Ο‰) β†’ (π΅β€˜π‘š) β‰Ί Ο‰)
7946, 77, 78syl2an 594 . . . . . . . . . 10 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ (π΅β€˜π‘š) β‰Ί Ο‰)
80 isfinite 9649 . . . . . . . . . 10 ((π΅β€˜π‘š) ∈ Fin ↔ (π΅β€˜π‘š) β‰Ί Ο‰)
8179, 80sylibr 233 . . . . . . . . 9 ((βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ ∧ π‘š ∈ Ο‰) β†’ (π΅β€˜π‘š) ∈ Fin)
8281ancoms 457 . . . . . . . 8 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ (π΅β€˜π‘š) ∈ Fin)
8339, 42iunsuc 6448 . . . . . . . . . . 11 βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) = (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βˆͺ (π΅β€˜π‘š))
84 fvex 6903 . . . . . . . . . . . . 13 (π΅β€˜π‘˜) ∈ V
8539, 84iunex 7957 . . . . . . . . . . . 12 βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ V
86 fvex 6903 . . . . . . . . . . . 12 (π΅β€˜π‘š) ∈ V
87 undjudom 10164 . . . . . . . . . . . 12 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ V ∧ (π΅β€˜π‘š) ∈ V) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βˆͺ (π΅β€˜π‘š)) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)))
8885, 86, 87mp2an 688 . . . . . . . . . . 11 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βˆͺ (π΅β€˜π‘š)) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š))
8983, 88eqbrtri 5168 . . . . . . . . . 10 βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š))
90 sdomtr 9117 . . . . . . . . . . . . . . . 16 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) β‰Ί Ο‰) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί Ο‰)
9180, 90sylan2b 592 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί Ο‰)
92 isfinite 9649 . . . . . . . . . . . . . . 15 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin ↔ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί Ο‰)
9391, 92sylibr 233 . . . . . . . . . . . . . 14 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin)
94 finnum 9945 . . . . . . . . . . . . . 14 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card)
9593, 94syl 17 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card)
96 finnum 9945 . . . . . . . . . . . . . 14 ((π΅β€˜π‘š) ∈ Fin β†’ (π΅β€˜π‘š) ∈ dom card)
9796adantl 480 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (π΅β€˜π‘š) ∈ dom card)
98 cardadju 10191 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card ∧ (π΅β€˜π‘š) ∈ dom card) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))))
9995, 97, 98syl2anc 582 . . . . . . . . . . . 12 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))))
100 ficardom 9958 . . . . . . . . . . . . . . . 16 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ Fin β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰)
10193, 100syl 17 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰)
102 ficardom 9958 . . . . . . . . . . . . . . . 16 ((π΅β€˜π‘š) ∈ Fin β†’ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰)
103102adantl 480 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰)
104 cardid2 9950 . . . . . . . . . . . . . . . . . 18 (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∈ dom card β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜))
10593, 94, 1043syl 18 . . . . . . . . . . . . . . . . 17 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜))
106 simpl 481 . . . . . . . . . . . . . . . . 17 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š))
107 cardid2 9950 . . . . . . . . . . . . . . . . . . 19 ((π΅β€˜π‘š) ∈ dom card β†’ (cardβ€˜(π΅β€˜π‘š)) β‰ˆ (π΅β€˜π‘š))
108 ensym 9001 . . . . . . . . . . . . . . . . . . 19 ((cardβ€˜(π΅β€˜π‘š)) β‰ˆ (π΅β€˜π‘š) β†’ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š)))
10996, 107, 1083syl 18 . . . . . . . . . . . . . . . . . 18 ((π΅β€˜π‘š) ∈ Fin β†’ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š)))
110109adantl 480 . . . . . . . . . . . . . . . . 17 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š)))
111 ensdomtr 9115 . . . . . . . . . . . . . . . . . 18 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∧ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (π΅β€˜π‘š))
112 sdomentr 9113 . . . . . . . . . . . . . . . . . 18 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š))) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)))
113111, 112sylan 578 . . . . . . . . . . . . . . . . 17 ((((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰ˆ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) ∧ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) ∧ (π΅β€˜π‘š) β‰ˆ (cardβ€˜(π΅β€˜π‘š))) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)))
114105, 106, 110, 113syl21anc 834 . . . . . . . . . . . . . . . 16 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)))
115 cardon 9941 . . . . . . . . . . . . . . . . . 18 (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ On
116 cardon 9941 . . . . . . . . . . . . . . . . . . 19 (cardβ€˜(π΅β€˜π‘š)) ∈ On
117 onenon 9946 . . . . . . . . . . . . . . . . . . 19 ((cardβ€˜(π΅β€˜π‘š)) ∈ On β†’ (cardβ€˜(π΅β€˜π‘š)) ∈ dom card)
118116, 117ax-mp 5 . . . . . . . . . . . . . . . . . 18 (cardβ€˜(π΅β€˜π‘š)) ∈ dom card
119 cardsdomel 9971 . . . . . . . . . . . . . . . . . 18 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ On ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ dom card) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(cardβ€˜(π΅β€˜π‘š)))))
120115, 118, 119mp2an 688 . . . . . . . . . . . . . . . . 17 ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(cardβ€˜(π΅β€˜π‘š))))
121 cardidm 9956 . . . . . . . . . . . . . . . . . 18 (cardβ€˜(cardβ€˜(π΅β€˜π‘š))) = (cardβ€˜(π΅β€˜π‘š))
122121eleq2i 2823 . . . . . . . . . . . . . . . . 17 ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(cardβ€˜(π΅β€˜π‘š))) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)))
123120, 122bitri 274 . . . . . . . . . . . . . . . 16 ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) β‰Ί (cardβ€˜(π΅β€˜π‘š)) ↔ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)))
124114, 123sylib 217 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)))
125 nnaordr 8622 . . . . . . . . . . . . . . . 16 (((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š)) ↔ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))))
126125biimpa 475 . . . . . . . . . . . . . . 15 ((((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰) ∧ (cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) ∈ (cardβ€˜(π΅β€˜π‘š))) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
127101, 103, 103, 124, 126syl31anc 1371 . . . . . . . . . . . . . 14 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
128 nnacl 8613 . . . . . . . . . . . . . . . . 17 (((cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰ ∧ (cardβ€˜(π΅β€˜π‘š)) ∈ Ο‰) β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ Ο‰)
129102, 102, 128syl2anc 582 . . . . . . . . . . . . . . . 16 ((π΅β€˜π‘š) ∈ Fin β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ Ο‰)
130 cardnn 9960 . . . . . . . . . . . . . . . 16 (((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ Ο‰ β†’ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) = ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
131129, 130syl 17 . . . . . . . . . . . . . . 15 ((π΅β€˜π‘š) ∈ Fin β†’ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) = ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
132131adantl 480 . . . . . . . . . . . . . 14 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) = ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
133127, 132eleqtrrd 2834 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∈ (cardβ€˜((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))))
134 cardsdomelir 9970 . . . . . . . . . . . . 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 9115 . . . . . . . . . . . 12 (((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) ∧ ((cardβ€˜βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜)) +o (cardβ€˜(π΅β€˜π‘š))) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š)))) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
13799, 135, 136syl2anc 582 . . . . . . . . . . 11 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
138 cardadju 10191 . . . . . . . . . . . . . 14 (((π΅β€˜π‘š) ∈ dom card ∧ (π΅β€˜π‘š) ∈ dom card) β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
13996, 96, 138syl2anc 582 . . . . . . . . . . . . 13 ((π΅β€˜π‘š) ∈ Fin β†’ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))))
140139ensymd 9003 . . . . . . . . . . . 12 ((π΅β€˜π‘š) ∈ Fin β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) β‰ˆ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
141140adantl 480 . . . . . . . . . . 11 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) β‰ˆ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
142 sdomentr 9113 . . . . . . . . . . 11 (((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) ∧ ((cardβ€˜(π΅β€˜π‘š)) +o (cardβ€˜(π΅β€˜π‘š))) β‰ˆ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
143137, 141, 142syl2anc 582 . . . . . . . . . 10 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
144 domsdomtr 9114 . . . . . . . . . 10 ((βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ό (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) ∧ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) βŠ” (π΅β€˜π‘š)) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
14589, 143, 144sylancr 585 . . . . . . . . 9 ((βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) ∧ (π΅β€˜π‘š) ∈ Fin) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)))
146145expcom 412 . . . . . . . 8 ((π΅β€˜π‘š) ∈ Fin β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))))
14782, 146syl 17 . . . . . . 7 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š))))
148 sdomentr 9113 . . . . . . . 8 ((βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) ∧ ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))
149148expcom 412 . . . . . . 7 (((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β‰ˆ (π΅β€˜suc π‘š) β†’ (βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί ((π΅β€˜π‘š) βŠ” (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
15072, 147, 149sylsyld 61 . . . . . 6 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ (βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
15138, 150syld 47 . . . . 5 ((π‘š ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š)))
152151ex 411 . . . 4 (π‘š ∈ Ο‰ β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))))
153152com23 86 . . 3 (π‘š ∈ Ο‰ β†’ ((βˆ€π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ π‘š (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘š)) β†’ (βˆ€π‘˜ ∈ suc suc π‘š(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ suc π‘š(π΅β€˜π‘˜) β‰Ί (π΅β€˜suc π‘š))))
1546, 12, 18, 32, 153finds1 7894 . 2 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜ β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›)))
155154imp 405 1 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘˜ ∈ suc 𝑛(π΅β€˜π‘˜) β‰ˆ 𝒫 π‘˜) β†’ βˆͺ π‘˜ ∈ 𝑛 (π΅β€˜π‘˜) β‰Ί (π΅β€˜π‘›))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  βˆ€wral 3059  Vcvv 3472   βˆͺ cun 3945   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  βˆͺ ciun 4996   class class class wbr 5147  dom cdm 5675  Ord word 6362  Oncon0 6363  suc csuc 6365  β€˜cfv 6542  (class class class)co 7411  Ο‰com 7857  1oc1o 8461   +o coa 8465   β‰ˆ cen 8938   β‰Ό cdom 8939   β‰Ί csdm 8940  Fincfn 8941   βŠ” cdju 9895  cardccrd 9932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  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 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-oadd 8472  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-dju 9898  df-card 9936
This theorem is referenced by:  domtriomlem  10439
  Copyright terms: Public domain W3C validator