Metamath Proof Explorer

Theorem sltlpss

Description: If two surreals share a birthday, then X iff the left set of X is a proper subset of the left set of Y . (Contributed by Scott Fenton, 17-Sep-2024)

Ref Expression
Assertion sltlpss 
|- ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X  ( _L ` X ) C. ( _L ` Y ) ) )

Proof

Step Hyp Ref Expression
1 oldssno 
 |-  ( _Old ` ( bday ` X ) ) C_ No
2 1 sseli 
 |-  ( x e. ( _Old ` ( bday ` X ) ) -> x e. No )
3 2 3ad2ant2 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  x e. No )
4 simp1l1 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  X e. No )
5 simp1l2 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  Y e. No )
6 simp3 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  x
7 simp1r 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  X
8 3 4 5 6 7 slttrd 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  x
9 8 3exp 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _Old ` ( bday ` X ) ) -> ( x  x
10 9 imdistand 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( x e. ( _Old ` ( bday ` X ) ) /\ x  ( x e. ( _Old ` ( bday ` X ) ) /\ x
11 fveq2 
 |-  ( ( bday ` X ) = ( bday ` Y ) -> ( _Old ` ( bday ` X ) ) = ( _Old ` ( bday ` Y ) ) )
12 11 3ad2ant3 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( _Old ` ( bday ` X ) ) = ( _Old ` ( bday ` Y ) ) )
13 12 adantr 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _Old ` ( bday ` X ) ) = ( _Old ` ( bday ` Y ) ) )
14 13 eleq2d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _Old ` ( bday ` X ) ) <-> x e. ( _Old ` ( bday ` Y ) ) ) )
15 14 anbi1d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( x e. ( _Old ` ( bday ` X ) ) /\ x  ( x e. ( _Old ` ( bday ` Y ) ) /\ x
16 10 15 sylibd 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( x e. ( _Old ` ( bday ` X ) ) /\ x  ( x e. ( _Old ` ( bday ` Y ) ) /\ x
17 leftval 
 |-  ( _L ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
18 17 a1i 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _L ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
19 18 eleq2d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _L ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) | x
20 rabid 
 |-  ( x e. { x e. ( _Old ` ( bday ` X ) ) | x  ( x e. ( _Old ` ( bday ` X ) ) /\ x
21 19 20 bitrdi 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _L ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x
22 leftval 
 |-  ( _L ` Y ) = { x e. ( _Old ` ( bday ` Y ) ) | x
23 22 a1i 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _L ` Y ) = { x e. ( _Old ` ( bday ` Y ) ) | x
24 23 eleq2d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _L ` Y ) <-> x e. { x e. ( _Old ` ( bday ` Y ) ) | x
25 rabid 
 |-  ( x e. { x e. ( _Old ` ( bday ` Y ) ) | x  ( x e. ( _Old ` ( bday ` Y ) ) /\ x
26 24 25 bitrdi 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _L ` Y ) <-> ( x e. ( _Old ` ( bday ` Y ) ) /\ x
27 16 21 26 3imtr4d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _L ` X ) -> x e. ( _L ` Y ) ) )
28 27 ssrdv 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _L ` X ) C_ ( _L ` Y ) )
29 sltirr 
 |-  ( Y e. No -> -. Y
30 29 3ad2ant2 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> -. Y
31 breq1 
 |-  ( X = Y -> ( X  Y
32 31 notbid 
 |-  ( X = Y -> ( -. X  -. Y
33 30 32 syl5ibrcom 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X = Y -> -. X
34 33 con2d 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X  -. X = Y ) )
35 34 imp 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  -. X = Y )
36 simpr 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _L ` X ) = ( _L ` Y ) )
37 lruneq 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( _L ` X ) u. ( _R ` X ) ) = ( ( _L ` Y ) u. ( _R ` Y ) ) )
38 37 adantr 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _L ` X ) u. ( _R ` X ) ) = ( ( _L ` Y ) u. ( _R ` Y ) ) )
39 38 adantr 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _L ` X ) u. ( _R ` X ) ) = ( ( _L ` Y ) u. ( _R ` Y ) ) )
40 39 36 difeq12d 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( ( _L ` X ) u. ( _R ` X ) ) \ ( _L ` X ) ) = ( ( ( _L ` Y ) u. ( _R ` Y ) ) \ ( _L ` Y ) ) )
41 difundir 
 |-  ( ( ( _L ` X ) u. ( _R ` X ) ) \ ( _L ` X ) ) = ( ( ( _L ` X ) \ ( _L ` X ) ) u. ( ( _R ` X ) \ ( _L ` X ) ) )
42 difid 
 |-  ( ( _L ` X ) \ ( _L ` X ) ) = (/)
43 42 uneq1i 
 |-  ( ( ( _L ` X ) \ ( _L ` X ) ) u. ( ( _R ` X ) \ ( _L ` X ) ) ) = ( (/) u. ( ( _R ` X ) \ ( _L ` X ) ) )
44 0un 
 |-  ( (/) u. ( ( _R ` X ) \ ( _L ` X ) ) ) = ( ( _R ` X ) \ ( _L ` X ) )
45 41 43 44 3eqtri 
 |-  ( ( ( _L ` X ) u. ( _R ` X ) ) \ ( _L ` X ) ) = ( ( _R ` X ) \ ( _L ` X ) )
46 incom 
 |-  ( ( _L ` X ) i^i ( _R ` X ) ) = ( ( _R ` X ) i^i ( _L ` X ) )
47 simpll1 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  X e. No )
48 lltropt 
 |-  ( X e. No -> ( _L ` X ) <
49 ssltdisj 
 |-  ( ( _L ` X ) < ( ( _L ` X ) i^i ( _R ` X ) ) = (/) )
50 47 48 49 3syl 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _L ` X ) i^i ( _R ` X ) ) = (/) )
51 46 50 eqtr3id 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _R ` X ) i^i ( _L ` X ) ) = (/) )
52 disjdif2 
 |-  ( ( ( _R ` X ) i^i ( _L ` X ) ) = (/) -> ( ( _R ` X ) \ ( _L ` X ) ) = ( _R ` X ) )
53 51 52 syl 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _R ` X ) \ ( _L ` X ) ) = ( _R ` X ) )
54 45 53 syl5eq 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( ( _L ` X ) u. ( _R ` X ) ) \ ( _L ` X ) ) = ( _R ` X ) )
55 difundir 
 |-  ( ( ( _L ` Y ) u. ( _R ` Y ) ) \ ( _L ` Y ) ) = ( ( ( _L ` Y ) \ ( _L ` Y ) ) u. ( ( _R ` Y ) \ ( _L ` Y ) ) )
56 difid 
 |-  ( ( _L ` Y ) \ ( _L ` Y ) ) = (/)
57 56 uneq1i 
 |-  ( ( ( _L ` Y ) \ ( _L ` Y ) ) u. ( ( _R ` Y ) \ ( _L ` Y ) ) ) = ( (/) u. ( ( _R ` Y ) \ ( _L ` Y ) ) )
58 0un 
 |-  ( (/) u. ( ( _R ` Y ) \ ( _L ` Y ) ) ) = ( ( _R ` Y ) \ ( _L ` Y ) )
59 55 57 58 3eqtri 
 |-  ( ( ( _L ` Y ) u. ( _R ` Y ) ) \ ( _L ` Y ) ) = ( ( _R ` Y ) \ ( _L ` Y ) )
60 incom 
 |-  ( ( _L ` Y ) i^i ( _R ` Y ) ) = ( ( _R ` Y ) i^i ( _L ` Y ) )
61 simpll2 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  Y e. No )
62 lltropt 
 |-  ( Y e. No -> ( _L ` Y ) <
63 ssltdisj 
 |-  ( ( _L ` Y ) < ( ( _L ` Y ) i^i ( _R ` Y ) ) = (/) )
64 61 62 63 3syl 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _L ` Y ) i^i ( _R ` Y ) ) = (/) )
65 60 64 eqtr3id 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _R ` Y ) i^i ( _L ` Y ) ) = (/) )
66 disjdif2 
 |-  ( ( ( _R ` Y ) i^i ( _L ` Y ) ) = (/) -> ( ( _R ` Y ) \ ( _L ` Y ) ) = ( _R ` Y ) )
67 65 66 syl 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _R ` Y ) \ ( _L ` Y ) ) = ( _R ` Y ) )
68 59 67 syl5eq 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( ( _L ` Y ) u. ( _R ` Y ) ) \ ( _L ` Y ) ) = ( _R ` Y ) )
69 40 54 68 3eqtr3d 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _R ` X ) = ( _R ` Y ) )
70 36 69 oveq12d 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _L ` X ) |s ( _R ` X ) ) = ( ( _L ` Y ) |s ( _R ` Y ) ) )
71 lrcut 
 |-  ( X e. No -> ( ( _L ` X ) |s ( _R ` X ) ) = X )
72 47 71 syl 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _L ` X ) |s ( _R ` X ) ) = X )
73 lrcut 
 |-  ( Y e. No -> ( ( _L ` Y ) |s ( _R ` Y ) ) = Y )
74 61 73 syl 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _L ` Y ) |s ( _R ` Y ) ) = Y )
75 70 72 74 3eqtr3d 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  X = Y )
76 35 75 mtand 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  -. ( _L ` X ) = ( _L ` Y ) )
77 dfpss2 
 |-  ( ( _L ` X ) C. ( _L ` Y ) <-> ( ( _L ` X ) C_ ( _L ` Y ) /\ -. ( _L ` X ) = ( _L ` Y ) ) )
78 28 76 77 sylanbrc 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _L ` X ) C. ( _L ` Y ) )
79 78 ex 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X  ( _L ` X ) C. ( _L ` Y ) ) )
80 dfpss3 
 |-  ( ( _L ` X ) C. ( _L ` Y ) <-> ( ( _L ` X ) C_ ( _L ` Y ) /\ -. ( _L ` Y ) C_ ( _L ` X ) ) )
81 ssdif0 
 |-  ( ( _L ` Y ) C_ ( _L ` X ) <-> ( ( _L ` Y ) \ ( _L ` X ) ) = (/) )
82 81 necon3bbii 
 |-  ( -. ( _L ` Y ) C_ ( _L ` X ) <-> ( ( _L ` Y ) \ ( _L ` X ) ) =/= (/) )
83 n0 
 |-  ( ( ( _L ` Y ) \ ( _L ` X ) ) =/= (/) <-> E. x x e. ( ( _L ` Y ) \ ( _L ` X ) ) )
84 82 83 bitri 
 |-  ( -. ( _L ` Y ) C_ ( _L ` X ) <-> E. x x e. ( ( _L ` Y ) \ ( _L ` X ) ) )
85 eldif 
 |-  ( x e. ( ( _L ` Y ) \ ( _L ` X ) ) <-> ( x e. ( _L ` Y ) /\ -. x e. ( _L ` X ) ) )
86 22 a1i 
 |-  ( Y e. No -> ( _L ` Y ) = { x e. ( _Old ` ( bday ` Y ) ) | x
87 86 eleq2d 
 |-  ( Y e. No -> ( x e. ( _L ` Y ) <-> x e. { x e. ( _Old ` ( bday ` Y ) ) | x
88 87 25 bitrdi 
 |-  ( Y e. No -> ( x e. ( _L ` Y ) <-> ( x e. ( _Old ` ( bday ` Y ) ) /\ x
89 17 a1i 
 |-  ( X e. No -> ( _L ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
90 89 eleq2d 
 |-  ( X e. No -> ( x e. ( _L ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) | x
91 90 20 bitrdi 
 |-  ( X e. No -> ( x e. ( _L ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x
92 91 notbid 
 |-  ( X e. No -> ( -. x e. ( _L ` X ) <-> -. ( x e. ( _Old ` ( bday ` X ) ) /\ x
93 ianor 
 |-  ( -. ( x e. ( _Old ` ( bday ` X ) ) /\ x  ( -. x e. ( _Old ` ( bday ` X ) ) \/ -. x
94 92 93 bitrdi 
 |-  ( X e. No -> ( -. x e. ( _L ` X ) <-> ( -. x e. ( _Old ` ( bday ` X ) ) \/ -. x
95 88 94 bi2anan9r 
 |-  ( ( X e. No /\ Y e. No ) -> ( ( x e. ( _L ` Y ) /\ -. x e. ( _L ` X ) ) <-> ( ( x e. ( _Old ` ( bday ` Y ) ) /\ x
96 95 3adant3 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( x e. ( _L ` Y ) /\ -. x e. ( _L ` X ) ) <-> ( ( x e. ( _Old ` ( bday ` Y ) ) /\ x
97 simprl 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  x e. ( _Old ` ( bday ` Y ) ) )
98 simpl3 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  ( bday ` X ) = ( bday ` Y ) )
99 98 fveq2d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  ( _Old ` ( bday ` X ) ) = ( _Old ` ( bday ` Y ) ) )
100 97 99 eleqtrrd 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  x e. ( _Old ` ( bday ` X ) ) )
101 100 pm2.24d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  ( -. x e. ( _Old ` ( bday ` X ) ) -> X
102 simpll1 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  X e. No )
103 oldssno 
 |-  ( _Old ` ( bday ` Y ) ) C_ No
104 103 97 sselid 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  x e. No )
105 104 adantr 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  x e. No )
106 simpll2 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  Y e. No )
107 simpl1 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  X e. No )
108 slenlt 
 |-  ( ( X e. No /\ x e. No ) -> ( X <_s x <-> -. x
109 107 104 108 syl2anc 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  ( X <_s x <-> -. x
110 109 biimpar 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  X <_s x )
111 simplrr 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  x
112 102 105 106 110 111 slelttrd 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  X
113 112 ex 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  ( -. x  X
114 101 113 jaod 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  ( ( -. x e. ( _Old ` ( bday ` X ) ) \/ -. x  X
115 114 expimpd 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( ( x e. ( _Old ` ( bday ` Y ) ) /\ x  X
116 96 115 sylbid 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( x e. ( _L ` Y ) /\ -. x e. ( _L ` X ) ) -> X
117 85 116 syl5bi 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( x e. ( ( _L ` Y ) \ ( _L ` X ) ) -> X
118 117 exlimdv 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( E. x x e. ( ( _L ` Y ) \ ( _L ` X ) ) -> X
119 84 118 syl5bi 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( -. ( _L ` Y ) C_ ( _L ` X ) -> X
120 119 adantld 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( ( _L ` X ) C_ ( _L ` Y ) /\ -. ( _L ` Y ) C_ ( _L ` X ) ) -> X
121 80 120 syl5bi 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( _L ` X ) C. ( _L ` Y ) -> X
122 79 121 impbid 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X  ( _L ` X ) C. ( _L ` Y ) ) )