![]() |
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 4078 | . . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | |
2 | intss1 4626 | . . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥) | |
3 | vex 3354 | . . . . . 6 ⊢ 𝑥 ∈ V | |
4 | 3 | ssex 4936 | . . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V) |
5 | 2, 4 | syl 17 | . . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V) |
6 | 5 | exlimiv 2010 | . . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V) |
7 | 1, 6 | sylbi 207 | . 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V) |
8 | vprc 4930 | . . . 4 ⊢ ¬ V ∈ V | |
9 | inteq 4614 | . . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅) | |
10 | int0 4625 | . . . . . 6 ⊢ ∩ ∅ = V | |
11 | 9, 10 | syl6eq 2821 | . . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V) |
12 | 11 | eleq1d 2835 | . . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V)) |
13 | 8, 12 | mtbiri 316 | . . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V) |
14 | 13 | necon2ai 2972 | . 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅) |
15 | 7, 14 | impbii 199 | 1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1631 ∃wex 1852 ∈ wcel 2145 ≠ wne 2943 Vcvv 3351 ⊆ wss 3723 ∅c0 4063 ∩ cint 4611 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-v 3353 df-dif 3726 df-in 3730 df-ss 3737 df-nul 4064 df-int 4612 |
This theorem is referenced by: intnex 4952 intexab 4953 iinexg 4955 onint0 7143 onintrab 7148 onmindif2 7159 fival 8474 elfi2 8476 elfir 8477 dffi2 8485 elfiun 8492 fifo 8494 tz9.1c 8770 tz9.12lem1 8814 tz9.12lem3 8816 rankf 8821 cardf2 8969 cardval3 8978 cardid2 8979 cardcf 9276 cflim2 9287 intwun 9759 wuncval 9766 inttsk 9798 intgru 9838 gruina 9842 dfrtrcl2 14010 mremre 16472 mrcval 16478 asplss 19544 aspsubrg 19546 toponmre 21118 subbascn 21279 insiga 30540 sigagenval 30543 sigagensiga 30544 dmsigagen 30547 dfon2lem8 32031 dfon2lem9 32032 bj-snmoore 33400 igenval 34192 pclvalN 35698 elrfi 37783 ismrcd1 37787 mzpval 37821 dmmzp 37822 salgenval 41058 intsal 41065 |
Copyright terms: Public domain | W3C validator |