![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pwfi | Structured version Visualization version GIF version |
Description: The power set of a finite set is finite and vice-versa. Theorem 38 of [Suppes] p. 104 and its converse, Theorem 40 of [Suppes] p. 105. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5364. (Revised by BTernaryTau, 7-Sep-2024.) |
Ref | Expression |
---|---|
pwfi | ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pweq 4617 | . . . 4 ⊢ (𝑥 = ∅ → 𝒫 𝑥 = 𝒫 ∅) | |
2 | 1 | eleq1d 2819 | . . 3 ⊢ (𝑥 = ∅ → (𝒫 𝑥 ∈ Fin ↔ 𝒫 ∅ ∈ Fin)) |
3 | pweq 4617 | . . . 4 ⊢ (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦) | |
4 | 3 | eleq1d 2819 | . . 3 ⊢ (𝑥 = 𝑦 → (𝒫 𝑥 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin)) |
5 | pweq 4617 | . . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → 𝒫 𝑥 = 𝒫 (𝑦 ∪ {𝑧})) | |
6 | 5 | eleq1d 2819 | . . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝒫 𝑥 ∈ Fin ↔ 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)) |
7 | pweq 4617 | . . . 4 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴) | |
8 | 7 | eleq1d 2819 | . . 3 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)) |
9 | pw0 4816 | . . . 4 ⊢ 𝒫 ∅ = {∅} | |
10 | snfi 9044 | . . . 4 ⊢ {∅} ∈ Fin | |
11 | 9, 10 | eqeltri 2830 | . . 3 ⊢ 𝒫 ∅ ∈ Fin |
12 | eqid 2733 | . . . . 5 ⊢ (𝑐 ∈ 𝒫 𝑦 ↦ (𝑐 ∪ {𝑧})) = (𝑐 ∈ 𝒫 𝑦 ↦ (𝑐 ∪ {𝑧})) | |
13 | 12 | pwfilem 9177 | . . . 4 ⊢ (𝒫 𝑦 ∈ Fin → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin) |
14 | 13 | a1i 11 | . . 3 ⊢ (𝑦 ∈ Fin → (𝒫 𝑦 ∈ Fin → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)) |
15 | 2, 4, 6, 8, 11, 14 | findcard2 9164 | . 2 ⊢ (𝐴 ∈ Fin → 𝒫 𝐴 ∈ Fin) |
16 | pwfir 9176 | . 2 ⊢ (𝒫 𝐴 ∈ Fin → 𝐴 ∈ Fin) | |
17 | 15, 16 | impbii 208 | 1 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ∈ wcel 2107 ∪ cun 3947 ∅c0 4323 𝒫 cpw 4603 {csn 4629 ↦ cmpt 5232 Fincfn 8939 |
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-sep 5300 ax-nul 5307 ax-pr 5428 ax-un 7725 |
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 2942 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-om 7856 df-1o 8466 df-en 8940 df-fin 8943 |
This theorem is referenced by: xpfi 9317 mapfi 9348 r1fin 9768 dfac12k 10142 pwsdompw 10199 ackbij1lem5 10219 ackbij1lem9 10223 ackbij1lem10 10224 ackbij1lem14 10228 ackbij1b 10234 isfin1-2 10380 isfin1-3 10381 domtriomlem 10437 dominf 10440 dominfac 10568 gchhar 10674 omina 10686 gchina 10694 hashpw 14396 hashbclem 14411 qshash 15773 ackbijnn 15774 incexclem 15782 incexc 15783 incexc2 15784 hashbccl 16936 lagsubg2 19071 lagsubg 19072 orbsta2 19178 sylow1lem3 19468 sylow1lem5 19470 sylow2alem2 19486 sylow2a 19487 sylow2blem2 19489 sylow2blem3 19490 sylow3lem3 19497 sylow3lem4 19498 sylow3lem6 19500 pgpfac1lem5 19949 discmp 22902 cmpfi 22912 dis1stc 23003 1stckgenlem 23057 ptcmpfi 23317 fiufl 23420 musum 26695 qerclwwlknfi 29326 hasheuni 33083 coinfliplem 33477 ballotth 33536 fineqvpow 34096 erdszelem2 34183 sticksstones22 40984 kelac2lem 41806 pwinfig 42312 |
Copyright terms: Public domain | W3C validator |