Metamath Proof Explorer

Theorem ltslpss

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 ltslpss 
|- ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X  ( _Left ` X ) C. ( _Left ` Y ) ) )

Proof

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