Metamath Proof Explorer

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 biimtrid 
 |-  ( ( 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 imbitrrid 
 |-  ( ( 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 ) ) )