![]() |
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 4349 | . . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | |
2 | intss1 4971 | . . . . 5 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥) | |
3 | vex 3466 | . . . . . 6 ⊢ 𝑥 ∈ V | |
4 | 3 | ssex 5326 | . . . . 5 ⊢ (∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V) |
5 | 2, 4 | syl 17 | . . . 4 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V) |
6 | 5 | exlimiv 1926 | . . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V) |
7 | 1, 6 | sylbi 216 | . 2 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V) |
8 | vprc 5320 | . . . 4 ⊢ ¬ V ∈ V | |
9 | inteq 4957 | . . . . . 6 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅) | |
10 | int0 4970 | . . . . . 6 ⊢ ∩ ∅ = V | |
11 | 9, 10 | eqtrdi 2782 | . . . . 5 ⊢ (𝐴 = ∅ → ∩ 𝐴 = V) |
12 | 11 | eleq1d 2811 | . . . 4 ⊢ (𝐴 = ∅ → (∩ 𝐴 ∈ V ↔ V ∈ V)) |
13 | 8, 12 | mtbiri 326 | . . 3 ⊢ (𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V) |
14 | 13 | necon2ai 2960 | . 2 ⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅) |
15 | 7, 14 | impbii 208 | 1 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1534 ∃wex 1774 ∈ wcel 2099 ≠ wne 2930 Vcvv 3462 ⊆ wss 3947 ∅c0 4325 ∩ cint 4954 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5304 |
This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ne 2931 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-dif 3950 df-in 3954 df-ss 3964 df-nul 4326 df-int 4955 |
This theorem is referenced by: intnex 5345 intexab 5346 iinexg 5348 onint0 7800 onintrab 7805 onmindif2 7816 fival 9455 elfi2 9457 elfir 9458 dffi2 9466 elfiun 9473 fifo 9475 tz9.1c 9773 tz9.12lem1 9830 tz9.12lem3 9832 rankf 9837 cardf2 9986 cardval3 9995 cardid2 9996 cardcf 10295 cflim2 10306 intwun 10778 wuncval 10785 inttsk 10817 intgru 10857 gruina 10861 dfrtrcl2 15067 mremre 17617 mrcval 17623 asplss 21871 aspsubrg 21873 toponmre 23088 subbascn 23249 zarclsint 33687 insiga 33970 sigagenval 33973 sigagensiga 33974 dmsigagen 33977 dfon2lem8 35614 dfon2lem9 35615 bj-snmoore 36820 igenval 37762 pclvalN 39589 elrfi 42351 ismrcd1 42355 mzpval 42389 dmmzp 42390 oninfex2 42910 salgenval 45942 intsal 45951 |
Copyright terms: Public domain | W3C validator |