Theorem nodenselem7

Description: Lemma for nodense . A and B are equal at all elements of the abstraction. (Contributed by Scott Fenton, 17-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		simpll	|- ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A A e. No )
2		simplr	|- ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A B e. No )
3		sltso	|-
4		sonr	|- ( ( -. A
5	3 4	mpan	|- ( A e. No -> -. A
6		breq2	|- ( A = B -> ( A A
7	6	notbid	|- ( A = B -> ( -. A -. A
8	5 7	syl5ibcom	|- ( A e. No -> ( A = B -> -. A
9	8	necon2ad	|- ( A e. No -> ( A A =/= B ) )
10	9	imp	|- ( ( A e. No /\ A A =/= B )
11	10	ad2ant2rl	|- ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A A =/= B )
12	1 2 11	3jca	|- ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A ( A e. No /\ B e. No /\ A =/= B ) )
13		nosepeq	|- ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ C e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> ( A ` C ) = ( B ` C ) )
14	12 13	sylan	|- ( ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A ( A ` C ) = ( B ` C ) )
15	14	ex	|- ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A ( C e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( A ` C ) = ( B ` C ) ) )