Theorem sltlpss 27826

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

Assertion

Ref	Expression
sltlpss	⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 ↔ ( L ‘𝑋) ⊊ ( L ‘𝑌)))

Proof of Theorem sltlpss

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		oldssno 27776	. . . . . . . . . . . 12 ⊢ ( O ‘( bday ‘𝑋)) ⊆ No
2	1	sseli 3945	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ( O ‘( bday ‘𝑋)) → 𝑥 ∈ No )
3	2	3ad2ant2 1134	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋) → 𝑥 ∈ No )
4		simp1l1 1267	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋) → 𝑋 ∈ No )
5		simp1l2 1268	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋) → 𝑌 ∈ No )
6		simp3 1138	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋) → 𝑥 <s 𝑋)
7		simp1r 1199	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋) → 𝑋 <s 𝑌)
8	3, 4, 5, 6, 7	slttrd 27678	. . . . . . . . 9 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋) → 𝑥 <s 𝑌)
9	8	3exp 1119	. . . . . . . 8 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( O ‘( bday ‘𝑋)) → (𝑥 <s 𝑋 → 𝑥 <s 𝑌)))
10	9	imdistand 570	. . . . . . 7 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ((𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋) → (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑌)))
11		fveq2 6861	. . . . . . . . . . 11 ⊢ (( bday ‘𝑋) = ( bday ‘𝑌) → ( O ‘( bday ‘𝑋)) = ( O ‘( bday ‘𝑌)))
12	11	3ad2ant3 1135	. . . . . . . . . 10 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → ( O ‘( bday ‘𝑋)) = ( O ‘( bday ‘𝑌)))
13	12	adantr 480	. . . . . . . . 9 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( O ‘( bday ‘𝑋)) = ( O ‘( bday ‘𝑌)))
14	13	eleq2d 2815	. . . . . . . 8 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( O ‘( bday ‘𝑋)) ↔ 𝑥 ∈ ( O ‘( bday ‘𝑌))))
15	14	anbi1d 631	. . . . . . 7 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ((𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑌) ↔ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)))
16	10, 15	sylibd 239	. . . . . 6 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ((𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋) → (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)))
17		leftval 27778	. . . . . . . . 9 ⊢ ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}
18	17	a1i 11	. . . . . . . 8 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋})
19	18	eleq2d 2815	. . . . . . 7 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( L ‘𝑋) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}))
20		rabid 3430	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋} ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋))
21	19, 20	bitrdi 287	. . . . . 6 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( L ‘𝑋) ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋)))
22		leftval 27778	. . . . . . . . 9 ⊢ ( L ‘𝑌) = {𝑥 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑥 <s 𝑌}
23	22	a1i 11	. . . . . . . 8 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑌) = {𝑥 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑥 <s 𝑌})
24	23	eleq2d 2815	. . . . . . 7 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( L ‘𝑌) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑥 <s 𝑌}))
25		rabid 3430	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑥 <s 𝑌} ↔ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌))
26	24, 25	bitrdi 287	. . . . . 6 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( L ‘𝑌) ↔ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)))
27	16, 21, 26	3imtr4d 294	. . . . 5 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( L ‘𝑋) → 𝑥 ∈ ( L ‘𝑌)))
28	27	ssrdv 3955	. . . 4 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑋) ⊆ ( L ‘𝑌))
29		sltirr 27665	. . . . . . . . 9 ⊢ (𝑌 ∈ No → ¬ 𝑌 <s 𝑌)
30	29	3ad2ant2 1134	. . . . . . . 8 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → ¬ 𝑌 <s 𝑌)
31		breq1 5113	. . . . . . . . 9 ⊢ (𝑋 = 𝑌 → (𝑋 <s 𝑌 ↔ 𝑌 <s 𝑌))
32	31	notbid 318	. . . . . . . 8 ⊢ (𝑋 = 𝑌 → (¬ 𝑋 <s 𝑌 ↔ ¬ 𝑌 <s 𝑌))
33	30, 32	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑋 = 𝑌 → ¬ 𝑋 <s 𝑌))
34	33	con2d 134	. . . . . 6 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 → ¬ 𝑋 = 𝑌))
35	34	imp 406	. . . . 5 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ¬ 𝑋 = 𝑌)
36		simpr 484	. . . . . . 7 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ( L ‘𝑋) = ( L ‘𝑌))
37		lruneq 27825	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (( L ‘𝑋) ∪ ( R ‘𝑋)) = (( L ‘𝑌) ∪ ( R ‘𝑌)))
38	37	adantr 480	. . . . . . . . . 10 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (( L ‘𝑋) ∪ ( R ‘𝑋)) = (( L ‘𝑌) ∪ ( R ‘𝑌)))
39	38	adantr 480	. . . . . . . . 9 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑋) ∪ ( R ‘𝑋)) = (( L ‘𝑌) ∪ ( R ‘𝑌)))
40	39, 36	difeq12d 4093	. . . . . . . 8 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ((( L ‘𝑋) ∪ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = ((( L ‘𝑌) ∪ ( R ‘𝑌)) ∖ ( L ‘𝑌)))
41		difundir 4257	. . . . . . . . . 10 ⊢ ((( L ‘𝑋) ∪ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = ((( L ‘𝑋) ∖ ( L ‘𝑋)) ∪ (( R ‘𝑋) ∖ ( L ‘𝑋)))
42		difid 4342	. . . . . . . . . . 11 ⊢ (( L ‘𝑋) ∖ ( L ‘𝑋)) = ∅
43	42	uneq1i 4130	. . . . . . . . . 10 ⊢ ((( L ‘𝑋) ∖ ( L ‘𝑋)) ∪ (( R ‘𝑋) ∖ ( L ‘𝑋))) = (∅ ∪ (( R ‘𝑋) ∖ ( L ‘𝑋)))
44		0un 4362	. . . . . . . . . 10 ⊢ (∅ ∪ (( R ‘𝑋) ∖ ( L ‘𝑋))) = (( R ‘𝑋) ∖ ( L ‘𝑋))
45	41, 43, 44	3eqtri 2757	. . . . . . . . 9 ⊢ ((( L ‘𝑋) ∪ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = (( R ‘𝑋) ∖ ( L ‘𝑋))
46		incom 4175	. . . . . . . . . . 11 ⊢ (( L ‘𝑋) ∩ ( R ‘𝑋)) = (( R ‘𝑋) ∩ ( L ‘𝑋))
47		lltropt 27791	. . . . . . . . . . . 12 ⊢ ( L ‘𝑋) <<s ( R ‘𝑋)
48		ssltdisj 27740	. . . . . . . . . . . 12 ⊢ (( L ‘𝑋) <<s ( R ‘𝑋) → (( L ‘𝑋) ∩ ( R ‘𝑋)) = ∅)
49	47, 48	mp1i 13	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑋) ∩ ( R ‘𝑋)) = ∅)
50	46, 49	eqtr3id 2779	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑋) ∩ ( L ‘𝑋)) = ∅)
51		disjdif2 4446	. . . . . . . . . 10 ⊢ ((( R ‘𝑋) ∩ ( L ‘𝑋)) = ∅ → (( R ‘𝑋) ∖ ( L ‘𝑋)) = ( R ‘𝑋))
52	50, 51	syl 17	. . . . . . . . 9 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑋) ∖ ( L ‘𝑋)) = ( R ‘𝑋))
53	45, 52	eqtrid 2777	. . . . . . . 8 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ((( L ‘𝑋) ∪ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = ( R ‘𝑋))
54		difundir 4257	. . . . . . . . . 10 ⊢ ((( L ‘𝑌) ∪ ( R ‘𝑌)) ∖ ( L ‘𝑌)) = ((( L ‘𝑌) ∖ ( L ‘𝑌)) ∪ (( R ‘𝑌) ∖ ( L ‘𝑌)))
55		difid 4342	. . . . . . . . . . 11 ⊢ (( L ‘𝑌) ∖ ( L ‘𝑌)) = ∅
56	55	uneq1i 4130	. . . . . . . . . 10 ⊢ ((( L ‘𝑌) ∖ ( L ‘𝑌)) ∪ (( R ‘𝑌) ∖ ( L ‘𝑌))) = (∅ ∪ (( R ‘𝑌) ∖ ( L ‘𝑌)))
57		0un 4362	. . . . . . . . . 10 ⊢ (∅ ∪ (( R ‘𝑌) ∖ ( L ‘𝑌))) = (( R ‘𝑌) ∖ ( L ‘𝑌))
58	54, 56, 57	3eqtri 2757	. . . . . . . . 9 ⊢ ((( L ‘𝑌) ∪ ( R ‘𝑌)) ∖ ( L ‘𝑌)) = (( R ‘𝑌) ∖ ( L ‘𝑌))
59		incom 4175	. . . . . . . . . . 11 ⊢ (( L ‘𝑌) ∩ ( R ‘𝑌)) = (( R ‘𝑌) ∩ ( L ‘𝑌))
60		lltropt 27791	. . . . . . . . . . . 12 ⊢ ( L ‘𝑌) <<s ( R ‘𝑌)
61		ssltdisj 27740	. . . . . . . . . . . 12 ⊢ (( L ‘𝑌) <<s ( R ‘𝑌) → (( L ‘𝑌) ∩ ( R ‘𝑌)) = ∅)
62	60, 61	mp1i 13	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑌) ∩ ( R ‘𝑌)) = ∅)
63	59, 62	eqtr3id 2779	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑌) ∩ ( L ‘𝑌)) = ∅)
64		disjdif2 4446	. . . . . . . . . 10 ⊢ ((( R ‘𝑌) ∩ ( L ‘𝑌)) = ∅ → (( R ‘𝑌) ∖ ( L ‘𝑌)) = ( R ‘𝑌))
65	63, 64	syl 17	. . . . . . . . 9 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑌) ∖ ( L ‘𝑌)) = ( R ‘𝑌))
66	58, 65	eqtrid 2777	. . . . . . . 8 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ((( L ‘𝑌) ∪ ( R ‘𝑌)) ∖ ( L ‘𝑌)) = ( R ‘𝑌))
67	40, 53, 66	3eqtr3d 2773	. . . . . . 7 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ( R ‘𝑋) = ( R ‘𝑌))
68	36, 67	oveq12d 7408	. . . . . 6 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑋) |s ( R ‘𝑋)) = (( L ‘𝑌) |s ( R ‘𝑌)))
69		simpll1 1213	. . . . . . 7 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → 𝑋 ∈ No )
70		lrcut 27822	. . . . . . 7 ⊢ (𝑋 ∈ No → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋)
71	69, 70	syl 17	. . . . . 6 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋)
72		simpll2 1214	. . . . . . 7 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → 𝑌 ∈ No )
73		lrcut 27822	. . . . . . 7 ⊢ (𝑌 ∈ No → (( L ‘𝑌) |s ( R ‘𝑌)) = 𝑌)
74	72, 73	syl 17	. . . . . 6 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑌) |s ( R ‘𝑌)) = 𝑌)
75	68, 71, 74	3eqtr3d 2773	. . . . 5 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → 𝑋 = 𝑌)
76	35, 75	mtand 815	. . . 4 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ¬ ( L ‘𝑋) = ( L ‘𝑌))
77		dfpss2 4054	. . . 4 ⊢ (( L ‘𝑋) ⊊ ( L ‘𝑌) ↔ (( L ‘𝑋) ⊆ ( L ‘𝑌) ∧ ¬ ( L ‘𝑋) = ( L ‘𝑌)))
78	28, 76, 77	sylanbrc 583	. . 3 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑋) ⊊ ( L ‘𝑌))
79	78	ex 412	. 2 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 → ( L ‘𝑋) ⊊ ( L ‘𝑌)))
80		dfpss3 4055	. . 3 ⊢ (( L ‘𝑋) ⊊ ( L ‘𝑌) ↔ (( L ‘𝑋) ⊆ ( L ‘𝑌) ∧ ¬ ( L ‘𝑌) ⊆ ( L ‘𝑋)))
81		ssdif0 4332	. . . . . . 7 ⊢ (( L ‘𝑌) ⊆ ( L ‘𝑋) ↔ (( L ‘𝑌) ∖ ( L ‘𝑋)) = ∅)
82	81	necon3bbii 2973	. . . . . 6 ⊢ (¬ ( L ‘𝑌) ⊆ ( L ‘𝑋) ↔ (( L ‘𝑌) ∖ ( L ‘𝑋)) ≠ ∅)
83		n0 4319	. . . . . 6 ⊢ ((( L ‘𝑌) ∖ ( L ‘𝑋)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)))
84	82, 83	bitri 275	. . . . 5 ⊢ (¬ ( L ‘𝑌) ⊆ ( L ‘𝑋) ↔ ∃𝑥 𝑥 ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)))
85		eldif 3927	. . . . . . 7 ⊢ (𝑥 ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)) ↔ (𝑥 ∈ ( L ‘𝑌) ∧ ¬ 𝑥 ∈ ( L ‘𝑋)))
86	22	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑌 ∈ No → ( L ‘𝑌) = {𝑥 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑥 <s 𝑌})
87	86	eleq2d 2815	. . . . . . . . . . 11 ⊢ (𝑌 ∈ No → (𝑥 ∈ ( L ‘𝑌) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑥 <s 𝑌}))
88	87, 25	bitrdi 287	. . . . . . . . . 10 ⊢ (𝑌 ∈ No → (𝑥 ∈ ( L ‘𝑌) ↔ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)))
89	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ No → ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋})
90	89	eleq2d 2815	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ No → (𝑥 ∈ ( L ‘𝑋) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}))
91	90, 20	bitrdi 287	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ No → (𝑥 ∈ ( L ‘𝑋) ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋)))
92	91	notbid 318	. . . . . . . . . . 11 ⊢ (𝑋 ∈ No → (¬ 𝑥 ∈ ( L ‘𝑋) ↔ ¬ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋)))
93		ianor 983	. . . . . . . . . . 11 ⊢ (¬ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋) ↔ (¬ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∨ ¬ 𝑥 <s 𝑋))
94	92, 93	bitrdi 287	. . . . . . . . . 10 ⊢ (𝑋 ∈ No → (¬ 𝑥 ∈ ( L ‘𝑋) ↔ (¬ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∨ ¬ 𝑥 <s 𝑋)))
95	88, 94	bi2anan9r 639	. . . . . . . . 9 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ) → ((𝑥 ∈ ( L ‘𝑌) ∧ ¬ 𝑥 ∈ ( L ‘𝑋)) ↔ ((𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌) ∧ (¬ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∨ ¬ 𝑥 <s 𝑋))))
96	95	3adant3 1132	. . . . . . . 8 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → ((𝑥 ∈ ( L ‘𝑌) ∧ ¬ 𝑥 ∈ ( L ‘𝑋)) ↔ ((𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌) ∧ (¬ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∨ ¬ 𝑥 <s 𝑋))))
97		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) → 𝑥 ∈ ( O ‘( bday ‘𝑌)))
98		simpl3 1194	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) → ( bday ‘𝑋) = ( bday ‘𝑌))
99	98	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) → ( O ‘( bday ‘𝑋)) = ( O ‘( bday ‘𝑌)))
100	97, 99	eleqtrrd 2832	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) → 𝑥 ∈ ( O ‘( bday ‘𝑋)))
101	100	pm2.24d 151	. . . . . . . . . 10 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) → (¬ 𝑥 ∈ ( O ‘( bday ‘𝑋)) → 𝑋 <s 𝑌))
102		simpll1 1213	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) ∧ ¬ 𝑥 <s 𝑋) → 𝑋 ∈ No )
103		oldssno 27776	. . . . . . . . . . . . . 14 ⊢ ( O ‘( bday ‘𝑌)) ⊆ No
104	103, 97	sselid 3947	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) → 𝑥 ∈ No )
105	104	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) ∧ ¬ 𝑥 <s 𝑋) → 𝑥 ∈ No )
106		simpll2 1214	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) ∧ ¬ 𝑥 <s 𝑋) → 𝑌 ∈ No )
107		simpl1 1192	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) → 𝑋 ∈ No )
108		slenlt 27671	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ No ∧ 𝑥 ∈ No ) → (𝑋 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝑋))
109	107, 104, 108	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) → (𝑋 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝑋))
110	109	biimpar 477	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) ∧ ¬ 𝑥 <s 𝑋) → 𝑋 ≤s 𝑥)
111		simplrr 777	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) ∧ ¬ 𝑥 <s 𝑋) → 𝑥 <s 𝑌)
112	102, 105, 106, 110, 111	slelttrd 27680	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) ∧ ¬ 𝑥 <s 𝑋) → 𝑋 <s 𝑌)
113	112	ex 412	. . . . . . . . . 10 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) → (¬ 𝑥 <s 𝑋 → 𝑋 <s 𝑌))
114	101, 113	jaod 859	. . . . . . . . 9 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) → ((¬ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∨ ¬ 𝑥 <s 𝑋) → 𝑋 <s 𝑌))
115	114	expimpd 453	. . . . . . . 8 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (((𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌) ∧ (¬ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∨ ¬ 𝑥 <s 𝑋)) → 𝑋 <s 𝑌))
116	96, 115	sylbid 240	. . . . . . 7 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → ((𝑥 ∈ ( L ‘𝑌) ∧ ¬ 𝑥 ∈ ( L ‘𝑋)) → 𝑋 <s 𝑌))
117	85, 116	biimtrid 242	. . . . . 6 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑥 ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)) → 𝑋 <s 𝑌))
118	117	exlimdv 1933	. . . . 5 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (∃𝑥 𝑥 ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)) → 𝑋 <s 𝑌))
119	84, 118	biimtrid 242	. . . 4 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (¬ ( L ‘𝑌) ⊆ ( L ‘𝑋) → 𝑋 <s 𝑌))
120	119	adantld 490	. . 3 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → ((( L ‘𝑋) ⊆ ( L ‘𝑌) ∧ ¬ ( L ‘𝑌) ⊆ ( L ‘𝑋)) → 𝑋 <s 𝑌))
121	80, 120	biimtrid 242	. 2 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (( L ‘𝑋) ⊊ ( L ‘𝑌) → 𝑋 <s 𝑌))
122	79, 121	impbid 212	1 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 ↔ ( L ‘𝑋) ⊊ ( L ‘𝑌)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2926  {crab 3408   ∖ cdif 3914   ∪ cun 3915   ∩ cin 3916   ⊆ wss 3917   ⊊ wpss 3918  ∅c0 4299   class class class wbr 5110  ‘cfv 6514  (class class class)co 7390   No csur 27558   <s cslt 27559   bday cbday 27560   ≤s csle 27663   <<s csslt 27699   |s cscut 27701   O cold 27758   L cleft 27760   R cright 27761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-1o 8437  df-2o 8438  df-no 27561  df-slt 27562  df-bday 27563  df-sle 27664  df-sslt 27700  df-scut 27702  df-made 27762  df-old 27763  df-left 27765  df-right 27766

This theorem is referenced by:  slelss  27827