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 4307 | . . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | |
2 | intss1 4882 | . . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥) | |
3 | vex 3495 | . . . . . 6 ⊢ 𝑥 ∈ V | |
4 | 3 | ssex 5216 | . . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V) |
5 | 2, 4 | syl 17 | . . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V) |
6 | 5 | exlimiv 1922 | . . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V) |
7 | 1, 6 | sylbi 218 | . 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V) |
8 | vprc 5210 | . . . 4 ⊢ ¬ V ∈ V | |
9 | inteq 4870 | . . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅) | |
10 | int0 4881 | . . . . . 6 ⊢ ∩ ∅ = V | |
11 | 9, 10 | syl6eq 2869 | . . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V) |
12 | 11 | eleq1d 2894 | . . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V)) |
13 | 8, 12 | mtbiri 328 | . . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V) |
14 | 13 | necon2ai 3042 | . 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅) |
15 | 7, 14 | impbii 210 | 1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1528 ∃wex 1771 ∈ wcel 2105 ≠ wne 3013 Vcvv 3492 ⊆ wss 3933 ∅c0 4288 ∩ cint 4867 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-ral 3140 df-rab 3144 df-v 3494 df-dif 3936 df-in 3940 df-ss 3949 df-nul 4289 df-int 4868 |
This theorem is referenced by: intnex 5232 intexab 5233 iinexg 5235 onint0 7500 onintrab 7505 onmindif2 7516 fival 8864 elfi2 8866 elfir 8867 dffi2 8875 elfiun 8882 fifo 8884 tz9.1c 9160 tz9.12lem1 9204 tz9.12lem3 9206 rankf 9211 cardf2 9360 cardval3 9369 cardid2 9370 cardcf 9662 cflim2 9673 intwun 10145 wuncval 10152 inttsk 10184 intgru 10224 gruina 10228 dfrtrcl2 14409 mremre 16863 mrcval 16869 asplss 20031 aspsubrg 20033 toponmre 21629 subbascn 21790 insiga 31295 sigagenval 31298 sigagensiga 31299 dmsigagen 31302 dfon2lem8 32932 dfon2lem9 32933 bj-snmoore 34299 igenval 35220 pclvalN 36906 elrfi 39169 ismrcd1 39173 mzpval 39207 dmmzp 39208 salgenval 42483 intsal 42490 |
Copyright terms: Public domain | W3C validator |