Theorem nodenselem4

Description: Lemma for nodense . Show that a particular abstraction is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011)

	Ref	Expression
Assertion	nodenselem4	|- ( ( ( A e. No /\ B e. No ) /\ A |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On )

Proof

Step	Hyp	Ref	Expression
1		simpll	|- ( ( ( A e. No /\ B e. No ) /\ A A e. No )
2		simplr	|- ( ( ( A e. No /\ B e. No ) /\ A B e. No )
3		sltso	|-
4		sonr	|- ( ( -. A
5	3 4	mpan	|- ( A e. No -> -. A
6	5	adantr	|- ( ( A e. No /\ B e. No ) -> -. A
7		breq2	|- ( A = B -> ( A A
8	7	notbid	|- ( A = B -> ( -. A -. A
9	6 8	syl5ibcom	|- ( ( A e. No /\ B e. No ) -> ( A = B -> -. A
10	9	necon2ad	|- ( ( A e. No /\ B e. No ) -> ( A A =/= B ) )
11	10	imp	|- ( ( ( A e. No /\ B e. No ) /\ A A =/= B )
12		nosepon	|- ( ( A e. No /\ B e. No /\ A =/= B ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On )
13	1 2 11 12	syl3anc	|- ( ( ( A e. No /\ B e. No ) /\ A |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On )