Theorem onint0

Description: The intersection of a class of ordinal numbers is zero iff the class contains zero. (Contributed by NM, 24-Apr-2004)

	Ref	Expression
Assertion	onint0	⊢ ( 𝐴 ⊆ On → ( ∩ 𝐴 = ∅ ↔ ∅ ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		eleq1	⊢ ( ∩ 𝐴 = ∅ → ( ∩ 𝐴 ∈ V ↔ ∅ ∈ V ) )
3	1 2	mpbiri	⊢ ( ∩ 𝐴 = ∅ → ∩ 𝐴 ∈ V )
4		intex	⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )
5	3 4	sylibr	⊢ ( ∩ 𝐴 = ∅ → 𝐴 ≠ ∅ )
6		onint	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝐴 )
7	5 6	sylan2	⊢ ( ( 𝐴 ⊆ On ∧ ∩ 𝐴 = ∅ ) → ∩ 𝐴 ∈ 𝐴 )
8		eleq1	⊢ ( ∩ 𝐴 = ∅ → ( ∩ 𝐴 ∈ 𝐴 ↔ ∅ ∈ 𝐴 ) )
9	8	adantl	⊢ ( ( 𝐴 ⊆ On ∧ ∩ 𝐴 = ∅ ) → ( ∩ 𝐴 ∈ 𝐴 ↔ ∅ ∈ 𝐴 ) )
10	7 9	mpbid	⊢ ( ( 𝐴 ⊆ On ∧ ∩ 𝐴 = ∅ ) → ∅ ∈ 𝐴 )
11	10	ex	⊢ ( 𝐴 ⊆ On → ( ∩ 𝐴 = ∅ → ∅ ∈ 𝐴 ) )
12		int0el	⊢ ( ∅ ∈ 𝐴 → ∩ 𝐴 = ∅ )
13	11 12	impbid1	⊢ ( 𝐴 ⊆ On → ( ∩ 𝐴 = ∅ ↔ ∅ ∈ 𝐴 ) )