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 ⊢ A ⊆ On → ⋂ A = ∅ ↔ ∅ ∈ A

Proof

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