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

Metamath Proof Explorer

Theorem oe0lem

Description: A helper lemma for oe0 and others. (Contributed by NM, 6-Jan-2005)

Ref Expression
Hypotheses oe0lem.1 
|- ( ( ph /\ A = (/) ) -> ps )
oe0lem.2 
|- ( ( ( A e. On /\ ph ) /\ (/) e. A ) -> ps )
Assertion oe0lem 
|- ( ( A e. On /\ ph ) -> ps )

Proof

Step Hyp Ref Expression
1 oe0lem.1 
 |-  ( ( ph /\ A = (/) ) -> ps )
2 oe0lem.2 
 |-  ( ( ( A e. On /\ ph ) /\ (/) e. A ) -> ps )
3 1 ex 
 |-  ( ph -> ( A = (/) -> ps ) )
4 3 adantl 
 |-  ( ( A e. On /\ ph ) -> ( A = (/) -> ps ) )
5 on0eln0 
 |-  ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
6 5 adantr 
 |-  ( ( A e. On /\ ph ) -> ( (/) e. A <-> A =/= (/) ) )
7 2 ex 
 |-  ( ( A e. On /\ ph ) -> ( (/) e. A -> ps ) )
8 6 7 sylbird 
 |-  ( ( A e. On /\ ph ) -> ( A =/= (/) -> ps ) )
9 4 8 pm2.61dne 
 |-  ( ( A e. On /\ ph ) -> ps )