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

Metamath Proof Explorer

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 → ( ∩ 𝐴 = ∅ ↔ ∅ ∈ 𝐴 ) )