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 )