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 5233. (Revised by BTernaryTau, 7-Sep-2024.) |
Ref | Expression |
---|---|
pwfi | ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pweq 4505 | . . . 4 ⊢ (𝑥 = ∅ → 𝒫 𝑥 = 𝒫 ∅) | |
2 | 1 | eleq1d 2818 | . . 3 ⊢ (𝑥 = ∅ → (𝒫 𝑥 ∈ Fin ↔ 𝒫 ∅ ∈ Fin)) |
3 | pweq 4505 | . . . 4 ⊢ (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦) | |
4 | 3 | eleq1d 2818 | . . 3 ⊢ (𝑥 = 𝑦 → (𝒫 𝑥 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin)) |
5 | pweq 4505 | . . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → 𝒫 𝑥 = 𝒫 (𝑦 ∪ {𝑧})) | |
6 | 5 | eleq1d 2818 | . . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝒫 𝑥 ∈ Fin ↔ 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)) |
7 | pweq 4505 | . . . 4 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴) | |
8 | 7 | eleq1d 2818 | . . 3 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)) |
9 | pw0 4701 | . . . 4 ⊢ 𝒫 ∅ = {∅} | |
10 | snfi 8645 | . . . 4 ⊢ {∅} ∈ Fin | |
11 | 9, 10 | eqeltri 2830 | . . 3 ⊢ 𝒫 ∅ ∈ Fin |
12 | eqid 2739 | . . . . 5 ⊢ (𝑐 ∈ 𝒫 𝑦 ↦ (𝑐 ∪ {𝑧})) = (𝑐 ∈ 𝒫 𝑦 ↦ (𝑐 ∪ {𝑧})) | |
13 | 12 | pwfilem 8778 | . . . 4 ⊢ (𝒫 𝑦 ∈ Fin → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin) |
14 | 13 | a1i 11 | . . 3 ⊢ (𝑦 ∈ Fin → (𝒫 𝑦 ∈ Fin → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)) |
15 | 2, 4, 6, 8, 11, 14 | findcard2 8766 | . 2 ⊢ (𝐴 ∈ Fin → 𝒫 𝐴 ∈ Fin) |
16 | pwfir 8777 | . 2 ⊢ (𝒫 𝐴 ∈ Fin → 𝐴 ∈ Fin) | |
17 | 15, 16 | impbii 212 | 1 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1542 ∈ wcel 2114 ∪ cun 3842 ∅c0 4212 𝒫 cpw 4489 {csn 4517 ↦ cmpt 5111 Fincfn 8558 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-sep 5168 ax-nul 5175 ax-pr 5297 ax-un 7482 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-ne 2936 df-ral 3059 df-rex 3060 df-reu 3061 df-rab 3063 df-v 3401 df-sbc 3682 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-pss 3863 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-tp 4522 df-op 4524 df-uni 4798 df-br 5032 df-opab 5094 df-mpt 5112 df-tr 5138 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5484 df-we 5486 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-om 7603 df-1o 8134 df-en 8559 df-fin 8562 |
This theorem is referenced by: mapfi 8896 r1fin 9278 dfac12k 9650 pwsdompw 9707 ackbij1lem5 9727 ackbij1lem9 9731 ackbij1lem10 9732 ackbij1lem14 9736 ackbij1b 9742 isfin1-2 9888 isfin1-3 9889 domtriomlem 9945 dominf 9948 dominfac 10076 gchhar 10182 omina 10194 gchina 10202 hashpw 13892 hashbclem 13905 qshash 15278 ackbijnn 15279 incexclem 15287 incexc 15288 incexc2 15289 hashbccl 16442 lagsubg2 18462 lagsubg 18463 orbsta2 18565 sylow1lem3 18846 sylow1lem5 18848 sylow2alem2 18864 sylow2a 18865 sylow2blem2 18867 sylow2blem3 18868 sylow3lem3 18875 sylow3lem4 18876 sylow3lem6 18878 pgpfac1lem5 19323 discmp 22152 cmpfi 22162 dis1stc 22253 1stckgenlem 22307 ptcmpfi 22567 fiufl 22670 musum 25931 qerclwwlknfi 28013 hasheuni 31626 coinfliplem 32018 ballotth 32077 fineqvpow 32639 erdszelem2 32728 kelac2lem 40484 pwinfig 40736 |
Copyright terms: Public domain | W3C validator |