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 C_ On -> ( |^| A = (/) <-> (/) e. A ) )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 eleq1 
 |-  ( |^| A = (/) -> ( |^| A e. _V <-> (/) e. _V ) )
3 1 2 mpbiri 
 |-  ( |^| A = (/) -> |^| A e. _V )
4 intex 
 |-  ( A =/= (/) <-> |^| A e. _V )
5 3 4 sylibr 
 |-  ( |^| A = (/) -> A =/= (/) )
6 onint 
 |-  ( ( A C_ On /\ A =/= (/) ) -> |^| A e. A )
7 5 6 sylan2 
 |-  ( ( A C_ On /\ |^| A = (/) ) -> |^| A e. A )
8 eleq1 
 |-  ( |^| A = (/) -> ( |^| A e. A <-> (/) e. A ) )
9 8 adantl 
 |-  ( ( A C_ On /\ |^| A = (/) ) -> ( |^| A e. A <-> (/) e. A ) )
10 7 9 mpbid 
 |-  ( ( A C_ On /\ |^| A = (/) ) -> (/) e. A )
11 10 ex 
 |-  ( A C_ On -> ( |^| A = (/) -> (/) e. A ) )
12 int0el 
 |-  ( (/) e. A -> |^| A = (/) )
13 11 12 impbid1 
 |-  ( A C_ On -> ( |^| A = (/) <-> (/) e. A ) )