Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > intex | Structured version Visualization version GIF version |
Description: The intersection of a nonempty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse. (Contributed by NM, 13-Aug-2002.) |
Ref | Expression |
---|---|
intex | ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0 3890 | . . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | |
2 | intss1 4427 | . . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥) | |
3 | vex 3176 | . . . . . 6 ⊢ 𝑥 ∈ V | |
4 | 3 | ssex 4730 | . . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V) |
5 | 2, 4 | syl 17 | . . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V) |
6 | 5 | exlimiv 1845 | . . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V) |
7 | 1, 6 | sylbi 206 | . 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V) |
8 | vprc 4724 | . . . 4 ⊢ ¬ V ∈ V | |
9 | inteq 4413 | . . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅) | |
10 | int0 4425 | . . . . . 6 ⊢ ∩ ∅ = V | |
11 | 9, 10 | syl6eq 2660 | . . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V) |
12 | 11 | eleq1d 2672 | . . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V)) |
13 | 8, 12 | mtbiri 316 | . . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V) |
14 | 13 | necon2ai 2811 | . 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅) |
15 | 7, 14 | impbii 198 | 1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ≠ wne 2780 Vcvv 3173 ⊆ wss 3540 ∅c0 3874 ∩ cint 4410 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-v 3175 df-dif 3543 df-in 3547 df-ss 3554 df-nul 3875 df-int 4411 |
This theorem is referenced by: intnex 4748 intexab 4749 iinexg 4751 onint0 6888 onintrab 6893 onmindif2 6904 fival 8201 elfi2 8203 elfir 8204 dffi2 8212 elfiun 8219 fifo 8221 tz9.1c 8489 tz9.12lem1 8533 tz9.12lem3 8535 rankf 8540 cardf2 8652 cardval3 8661 cardid2 8662 cardcf 8957 cflim2 8968 intwun 9436 wuncval 9443 inttsk 9475 intgru 9515 gruina 9519 dfrtrcl2 13650 mremre 16087 mrcval 16093 asplss 19150 aspsubrg 19152 toponmre 20707 subbascn 20868 insiga 29527 sigagenval 29530 sigagensiga 29531 dmsigagen 29534 dfon2lem8 30939 dfon2lem9 30940 igenval 33030 pclvalN 34194 elrfi 36275 ismrcd1 36279 mzpval 36313 dmmzp 36314 salgenval 39217 intsal 39224 |
Copyright terms: Public domain | W3C validator |