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 )