Theorem nodenselem8

Description: Lemma for nodense . Give a condition for surreal less than when two surreals have the same birthday. (Contributed by Scott Fenton, 19-Jun-2011)

	Ref	Expression
Assertion	nodenselem8	|- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) )

Proof

Step	Hyp	Ref	Expression
1		nodenselem5	|- ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) )
2	1	exp32	|- ( ( A e. No /\ B e. No ) -> ( ( bday ` A ) = ( bday ` B ) -> ( A |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) ) ) )
3	2	3impia	|- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) ) )
4		sltval2	|- ( ( A e. No /\ B e. No ) -> ( A ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
5	4	3adant3	|- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
6		fvex	|- ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. _V
7		fvex	|- ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. _V
8	6 7	brtp	|- ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) <-> ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) )
9		eleq2	|- ( ( bday ` A ) = ( bday ` B ) -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) <-> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` B ) ) )
10	9	biimpd	|- ( ( bday ` A ) = ( bday ` B ) -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` B ) ) )
11		nosgnn0	|- -. (/) e. { 1o , 2o }
12		nofnbday	|- ( B e. No -> B Fn ( bday ` B ) )
13		fnfvelrn	|- ( ( B Fn ( bday ` B ) /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` B ) ) -> ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. ran B )
14		eleq1	|- ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. ran B <-> (/) e. ran B ) )
15	13 14	syl5ibcom	|- ( ( B Fn ( bday ` B ) /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` B ) ) -> ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> (/) e. ran B ) )
16	12 15	sylan	|- ( ( B e. No /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` B ) ) -> ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> (/) e. ran B ) )
17		norn	|- ( B e. No -> ran B C_ { 1o , 2o } )
18	17	sseld	|- ( B e. No -> ( (/) e. ran B -> (/) e. { 1o , 2o } ) )
19	18	adantr	|- ( ( B e. No /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` B ) ) -> ( (/) e. ran B -> (/) e. { 1o , 2o } ) )
20	16 19	syld	|- ( ( B e. No /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` B ) ) -> ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> (/) e. { 1o , 2o } ) )
21	11 20	mtoi	|- ( ( B e. No /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` B ) ) -> -. ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) )
22	21	ex	|- ( B e. No -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` B ) -> -. ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) )
23	22	adantl	|- ( ( A e. No /\ B e. No ) -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` B ) -> -. ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) )
24	10 23	syl9r	|- ( ( A e. No /\ B e. No ) -> ( ( bday ` A ) = ( bday ` B ) -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) -> -. ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) ) )
25	24	3impia	|- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) -> -. ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) )
26	25	imp	|- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) ) -> -. ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) )
27	26	intnand	|- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) ) -> -. ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) )
28		nofnbday	|- ( A e. No -> A Fn ( bday ` A ) )
29		fnfvelrn	|- ( ( A Fn ( bday ` A ) /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) ) -> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. ran A )
30		eleq1	|- ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. ran A <-> (/) e. ran A ) )
31	29 30	syl5ibcom	|- ( ( A Fn ( bday ` A ) /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) ) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> (/) e. ran A ) )
32	28 31	sylan	|- ( ( A e. No /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) ) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> (/) e. ran A ) )
33		norn	|- ( A e. No -> ran A C_ { 1o , 2o } )
34	33	sseld	|- ( A e. No -> ( (/) e. ran A -> (/) e. { 1o , 2o } ) )
35	34	adantr	|- ( ( A e. No /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) ) -> ( (/) e. ran A -> (/) e. { 1o , 2o } ) )
36	32 35	syld	|- ( ( A e. No /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) ) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> (/) e. { 1o , 2o } ) )
37	11 36	mtoi	|- ( ( A e. No /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) ) -> -. ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) )
38	37	3ad2antl1	|- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) ) -> -. ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) )
39	38	intnanrd	|- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) ) -> -. ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) )
40		3orel13	|- ( ( -. ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) /\ -. ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) -> ( ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) )
41	27 39 40	syl2anc	|- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) ) -> ( ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) )
42	41	ex	|- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) -> ( ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) ) )
43	42	com23	|- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) ) )
44	8 43	syl5bi	|- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) ) )
45	5 44	sylbid	|- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) ) )
46	3 45	mpdd	|- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) )
47		3mix2	|- ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) -> ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) )
48	47 8	sylibr	|- ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) -> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
49	48 5	syl5ibr	|- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) -> A
50	46 49	impbid	|- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) )