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 4247 | . . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | |
2 | intss1 4860 | . . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥) | |
3 | vex 3402 | . . . . . 6 ⊢ 𝑥 ∈ V | |
4 | 3 | ssex 5199 | . . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V) |
5 | 2, 4 | syl 17 | . . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V) |
6 | 5 | exlimiv 1938 | . . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V) |
7 | 1, 6 | sylbi 220 | . 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V) |
8 | vprc 5193 | . . . 4 ⊢ ¬ V ∈ V | |
9 | inteq 4848 | . . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅) | |
10 | int0 4859 | . . . . . 6 ⊢ ∩ ∅ = V | |
11 | 9, 10 | eqtrdi 2787 | . . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V) |
12 | 11 | eleq1d 2815 | . . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V)) |
13 | 8, 12 | mtbiri 330 | . . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V) |
14 | 13 | necon2ai 2961 | . 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅) |
15 | 7, 14 | impbii 212 | 1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1543 ∃wex 1787 ∈ wcel 2112 ≠ wne 2932 Vcvv 3398 ⊆ wss 3853 ∅c0 4223 ∩ cint 4845 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 ax-sep 5177 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-ne 2933 df-ral 3056 df-rab 3060 df-v 3400 df-dif 3856 df-in 3860 df-ss 3870 df-nul 4224 df-int 4846 |
This theorem is referenced by: intnex 5216 intexab 5217 iinexg 5219 onint0 7553 onintrab 7558 onmindif2 7569 fival 9006 elfi2 9008 elfir 9009 dffi2 9017 elfiun 9024 fifo 9026 tz9.1c 9324 tz9.12lem1 9368 tz9.12lem3 9370 rankf 9375 cardf2 9524 cardval3 9533 cardid2 9534 cardcf 9831 cflim2 9842 intwun 10314 wuncval 10321 inttsk 10353 intgru 10393 gruina 10397 dfrtrcl2 14590 mremre 17061 mrcval 17067 asplss 20787 aspsubrg 20789 toponmre 21944 subbascn 22105 zarclsint 31490 insiga 31771 sigagenval 31774 sigagensiga 31775 dmsigagen 31778 dfon2lem8 33436 dfon2lem9 33437 bj-snmoore 34968 igenval 35905 pclvalN 37590 elrfi 40160 ismrcd1 40164 mzpval 40198 dmmzp 40199 salgenval 43480 intsal 43487 |
Copyright terms: Public domain | W3C validator |