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