Theorem nodenselem6

Description: The restriction of a surreal to the abstraction from nodenselem4 is still a surreal. (Contributed by Scott Fenton, 16-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		simpll	|- ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A A e. No )
2		nodenselem4	|- ( ( ( A e. No /\ B e. No ) /\ A |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On )
3	2	adantrl	|- ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On )
4		noreson	|- ( ( A e. No /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On ) -> ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. No )
5	1 3 4	syl2anc	|- ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A ( A |` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. No )