![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > en0 | Structured version Visualization version GIF version |
Description: The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.) Avoid ax-pow 5370, ax-un 7753. (Revised by BTernaryTau, 23-Sep-2024.) |
Ref | Expression |
---|---|
en0 | ⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | encv 8991 | . . . . 5 ⊢ (𝐴 ≈ ∅ → (𝐴 ∈ V ∧ ∅ ∈ V)) | |
2 | breng 8992 | . . . . 5 ⊢ ((𝐴 ∈ V ∧ ∅ ∈ V) → (𝐴 ≈ ∅ ↔ ∃𝑓 𝑓:𝐴–1-1-onto→∅)) | |
3 | 1, 2 | syl 17 | . . . 4 ⊢ (𝐴 ≈ ∅ → (𝐴 ≈ ∅ ↔ ∃𝑓 𝑓:𝐴–1-1-onto→∅)) |
4 | 3 | ibi 267 | . . 3 ⊢ (𝐴 ≈ ∅ → ∃𝑓 𝑓:𝐴–1-1-onto→∅) |
5 | f1ocnv 6860 | . . . . 5 ⊢ (𝑓:𝐴–1-1-onto→∅ → ◡𝑓:∅–1-1-onto→𝐴) | |
6 | f1o00 6883 | . . . . . 6 ⊢ (◡𝑓:∅–1-1-onto→𝐴 ↔ (◡𝑓 = ∅ ∧ 𝐴 = ∅)) | |
7 | 6 | simprbi 496 | . . . . 5 ⊢ (◡𝑓:∅–1-1-onto→𝐴 → 𝐴 = ∅) |
8 | 5, 7 | syl 17 | . . . 4 ⊢ (𝑓:𝐴–1-1-onto→∅ → 𝐴 = ∅) |
9 | 8 | exlimiv 1927 | . . 3 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→∅ → 𝐴 = ∅) |
10 | 4, 9 | syl 17 | . 2 ⊢ (𝐴 ≈ ∅ → 𝐴 = ∅) |
11 | 0ex 5312 | . . . . 5 ⊢ ∅ ∈ V | |
12 | f1oeq1 6836 | . . . . 5 ⊢ (𝑓 = ∅ → (𝑓:∅–1-1-onto→∅ ↔ ∅:∅–1-1-onto→∅)) | |
13 | f1o0 6885 | . . . . 5 ⊢ ∅:∅–1-1-onto→∅ | |
14 | 11, 12, 13 | ceqsexv2d 3532 | . . . 4 ⊢ ∃𝑓 𝑓:∅–1-1-onto→∅ |
15 | breng 8992 | . . . . 5 ⊢ ((∅ ∈ V ∧ ∅ ∈ V) → (∅ ≈ ∅ ↔ ∃𝑓 𝑓:∅–1-1-onto→∅)) | |
16 | 11, 11, 15 | mp2an 692 | . . . 4 ⊢ (∅ ≈ ∅ ↔ ∃𝑓 𝑓:∅–1-1-onto→∅) |
17 | 14, 16 | mpbir 231 | . . 3 ⊢ ∅ ≈ ∅ |
18 | breq1 5150 | . . 3 ⊢ (𝐴 = ∅ → (𝐴 ≈ ∅ ↔ ∅ ≈ ∅)) | |
19 | 17, 18 | mpbiri 258 | . 2 ⊢ (𝐴 = ∅ → 𝐴 ≈ ∅) |
20 | 10, 19 | impbii 209 | 1 ⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1536 ∃wex 1775 ∈ wcel 2105 Vcvv 3477 ∅c0 4338 class class class wbr 5147 ◡ccnv 5687 –1-1-onto→wf1o 6561 ≈ cen 8980 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-mo 2537 df-clab 2712 df-cleq 2726 df-clel 2813 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5148 df-opab 5210 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-en 8984 |
This theorem is referenced by: 0fi 9080 snfiOLD 9082 enrefnn 9085 dom0 9140 dom0OLD 9141 0sdomgOLD 9143 sdom0 9146 findcard 9201 findcard2 9202 nneneq 9243 nneneqOLD 9255 snnen2oOLD 9261 enp1iOLD 9311 fiintOLD 9364 cantnff 9711 cantnf0 9712 cantnfp1lem2 9716 cantnflem1 9726 cantnf 9730 cnfcom2lem 9738 cardnueq0 10001 infmap2 10254 fin23lem26 10362 cardeq0 10589 hasheq0 14398 mreexexd 17692 pmtrfmvdn0 19494 pmtrsn 19551 rp-isfinite6 43507 ensucne0OLD 43519 |
Copyright terms: Public domain | W3C validator |