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	syl6eq	⊢ ( 𝐴 = ∅ → ∩ 𝐴 = V )
12	11	eleq1d	⊢ ( 𝐴 = ∅ → ( ∩ 𝐴 ∈ V ↔ V ∈ V ) )
13	8 12	mtbiri	⊢ ( 𝐴 = ∅ → ¬ ∩ 𝐴 ∈ V )
14	13	necon2ai	⊢ ( ∩ 𝐴 ∈ V → 𝐴 ≠ ∅ )
15	7 14	impbii	⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )