This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem intex

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
Assertion intex ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
2 intss1 ⊢ ( 𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥 )
3 vex ⊢ 𝑥 ∈ V
4 3 ssex ⊢ ( ∩ 𝐴 ⊆ 𝑥 → ∩ 𝐴 ∈ V )
5 2 4 syl ⊢ ( 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V )
6 5 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V )
7 1 6 sylbi ⊢ ( 𝐴 ≠ ∅ → ∩ 𝐴 ∈ V )
8 vprc ⊢ ¬ V ∈ V
9 inteq ⊢ ( 𝐴 = ∅ → ∩ 𝐴 = ∩ ∅ )
10 int0 ⊢ ∩ ∅ = V
11 9 10 eqtrdi ⊢ ( 𝐴 = ∅ → ∩ 𝐴 = V )
12 11 eleq1d ⊢ ( 𝐴 = ∅ → ( ∩ 𝐴 ∈ V ↔ V ∈ V ) )
13 8 12 mtbiri ⊢ ( 𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V )
14 13 necon2ai ⊢ ( ∩ 𝐴 ∈ V → 𝐴 ≠ ∅ )
15 7 14 impbii ⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )