Theorem sltlpss 27945

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 27900	. . . . . . . . . . . 12 ⊢ ( O ‘( bday ‘𝑋)) ⊆ No
2	1	sseli 3979	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ( O ‘( bday ‘𝑋)) → 𝑥 ∈ No )
3	2	3ad2ant2 1135	. . . . . . . . . 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 1139	. . . . . . . . . 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 27804	. . . . . . . . 9 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋) → 𝑥 <s 𝑌)
9	8	3exp 1120	. . . . . . . 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 6906	. . . . . . . . . . 11 ⊢ (( bday ‘𝑋) = ( bday ‘𝑌) → ( O ‘( bday ‘𝑋)) = ( O ‘( bday ‘𝑌)))
12	11	3ad2ant3 1136	. . . . . . . . . 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 2827	. . . . . . . 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 27902	. . . . . . . . 9 ⊢ ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}
18	17	a1i 11	. . . . . . . 8 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋})
19	18	eleq2d 2827	. . . . . . 7 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( L ‘𝑋) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}))
20		rabid 3458	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋} ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋))
21	19, 20	bitrdi 287	. . . . . 6 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( L ‘𝑋) ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋)))
22		leftval 27902	. . . . . . . . 9 ⊢ ( L ‘𝑌) = {𝑥 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑥 <s 𝑌}
23	22	a1i 11	. . . . . . . 8 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑌) = {𝑥 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑥 <s 𝑌})
24	23	eleq2d 2827	. . . . . . 7 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( L ‘𝑌) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑥 <s 𝑌}))
25		rabid 3458	. . . . . . 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 3989	. . . 4 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑋) ⊆ ( L ‘𝑌))
29		sltirr 27791	. . . . . . . . 9 ⊢ (𝑌 ∈ No → ¬ 𝑌 <s 𝑌)
30	29	3ad2ant2 1135	. . . . . . . 8 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → ¬ 𝑌 <s 𝑌)
31		breq1 5146	. . . . . . . . 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 27944	. . . . . . . . . . 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 4127	. . . . . . . 8 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ((( L ‘𝑋) ∪ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = ((( L ‘𝑌) ∪ ( R ‘𝑌)) ∖ ( L ‘𝑌)))
41		difundir 4291	. . . . . . . . . 10 ⊢ ((( L ‘𝑋) ∪ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = ((( L ‘𝑋) ∖ ( L ‘𝑋)) ∪ (( R ‘𝑋) ∖ ( L ‘𝑋)))
42		difid 4376	. . . . . . . . . . 11 ⊢ (( L ‘𝑋) ∖ ( L ‘𝑋)) = ∅
43	42	uneq1i 4164	. . . . . . . . . 10 ⊢ ((( L ‘𝑋) ∖ ( L ‘𝑋)) ∪ (( R ‘𝑋) ∖ ( L ‘𝑋))) = (∅ ∪ (( R ‘𝑋) ∖ ( L ‘𝑋)))
44		0un 4396	. . . . . . . . . 10 ⊢ (∅ ∪ (( R ‘𝑋) ∖ ( L ‘𝑋))) = (( R ‘𝑋) ∖ ( L ‘𝑋))
45	41, 43, 44	3eqtri 2769	. . . . . . . . 9 ⊢ ((( L ‘𝑋) ∪ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = (( R ‘𝑋) ∖ ( L ‘𝑋))
46		incom 4209	. . . . . . . . . . 11 ⊢ (( L ‘𝑋) ∩ ( R ‘𝑋)) = (( R ‘𝑋) ∩ ( L ‘𝑋))
47		lltropt 27911	. . . . . . . . . . . 12 ⊢ ( L ‘𝑋) <<s ( R ‘𝑋)
48		ssltdisj 27866	. . . . . . . . . . . 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 2791	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑋) ∩ ( L ‘𝑋)) = ∅)
51		disjdif2 4480	. . . . . . . . . 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 2789	. . . . . . . 8 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ((( L ‘𝑋) ∪ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = ( R ‘𝑋))
54		difundir 4291	. . . . . . . . . 10 ⊢ ((( L ‘𝑌) ∪ ( R ‘𝑌)) ∖ ( L ‘𝑌)) = ((( L ‘𝑌) ∖ ( L ‘𝑌)) ∪ (( R ‘𝑌) ∖ ( L ‘𝑌)))
55		difid 4376	. . . . . . . . . . 11 ⊢ (( L ‘𝑌) ∖ ( L ‘𝑌)) = ∅
56	55	uneq1i 4164	. . . . . . . . . 10 ⊢ ((( L ‘𝑌) ∖ ( L ‘𝑌)) ∪ (( R ‘𝑌) ∖ ( L ‘𝑌))) = (∅ ∪ (( R ‘𝑌) ∖ ( L ‘𝑌)))
57		0un 4396	. . . . . . . . . 10 ⊢ (∅ ∪ (( R ‘𝑌) ∖ ( L ‘𝑌))) = (( R ‘𝑌) ∖ ( L ‘𝑌))
58	54, 56, 57	3eqtri 2769	. . . . . . . . 9 ⊢ ((( L ‘𝑌) ∪ ( R ‘𝑌)) ∖ ( L ‘𝑌)) = (( R ‘𝑌) ∖ ( L ‘𝑌))
59		incom 4209	. . . . . . . . . . 11 ⊢ (( L ‘𝑌) ∩ ( R ‘𝑌)) = (( R ‘𝑌) ∩ ( L ‘𝑌))
60		lltropt 27911	. . . . . . . . . . . 12 ⊢ ( L ‘𝑌) <<s ( R ‘𝑌)
61		ssltdisj 27866	. . . . . . . . . . . 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 2791	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑌) ∩ ( L ‘𝑌)) = ∅)
64		disjdif2 4480	. . . . . . . . . 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 2789	. . . . . . . 8 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ((( L ‘𝑌) ∪ ( R ‘𝑌)) ∖ ( L ‘𝑌)) = ( R ‘𝑌))
67	40, 53, 66	3eqtr3d 2785	. . . . . . 7 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ( R ‘𝑋) = ( R ‘𝑌))
68	36, 67	oveq12d 7449	. . . . . 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 27941	. . . . . . 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 27941	. . . . . . 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 2785	. . . . 5 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → 𝑋 = 𝑌)
76	35, 75	mtand 816	. . . 4 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ¬ ( L ‘𝑋) = ( L ‘𝑌))
77		dfpss2 4088	. . . 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 4089	. . 3 ⊢ (( L ‘𝑋) ⊊ ( L ‘𝑌) ↔ (( L ‘𝑋) ⊆ ( L ‘𝑌) ∧ ¬ ( L ‘𝑌) ⊆ ( L ‘𝑋)))
81		ssdif0 4366	. . . . . . 7 ⊢ (( L ‘𝑌) ⊆ ( L ‘𝑋) ↔ (( L ‘𝑌) ∖ ( L ‘𝑋)) = ∅)
82	81	necon3bbii 2988	. . . . . 6 ⊢ (¬ ( L ‘𝑌) ⊆ ( L ‘𝑋) ↔ (( L ‘𝑌) ∖ ( L ‘𝑋)) ≠ ∅)
83		n0 4353	. . . . . 6 ⊢ ((( L ‘𝑌) ∖ ( L ‘𝑋)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)))
84	82, 83	bitri 275	. . . . 5 ⊢ (¬ ( L ‘𝑌) ⊆ ( L ‘𝑋) ↔ ∃𝑥 𝑥 ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)))
85		eldif 3961	. . . . . . 7 ⊢ (𝑥 ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)) ↔ (𝑥 ∈ ( L ‘𝑌) ∧ ¬ 𝑥 ∈ ( L ‘𝑋)))
86	22	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑌 ∈ No → ( L ‘𝑌) = {𝑥 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑥 <s 𝑌})
87	86	eleq2d 2827	. . . . . . . . . . 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 2827	. . . . . . . . . . . . 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 984	. . . . . . . . . . 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 1133	. . . . . . . 8 ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → ((𝑥 ∈ ( L ‘𝑌) ∧ ¬ 𝑥 ∈ ( L ‘𝑋)) ↔ ((𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌) ∧ (¬ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∨ ¬ 𝑥 <s 𝑋))))
97		simprl 771	. . . . . . . . . . . 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 6910	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) → ( O ‘( bday ‘𝑋)) = ( O ‘( bday ‘𝑌)))
100	97, 99	eleqtrrd 2844	. . . . . . . . . . 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 27900	. . . . . . . . . . . . . 14 ⊢ ( O ‘( bday ‘𝑌)) ⊆ No
104	103, 97	sselid 3981	. . . . . . . . . . . . 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 27797	. . . . . . . . . . . . . 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 778	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌)) ∧ ¬ 𝑥 <s 𝑋) → 𝑥 <s 𝑌)
112	102, 105, 106, 110, 111	slelttrd 27806	. . . . . . . . . . 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 860	. . . . . . . . 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 848   ∧ w3a 1087   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2940  {crab 3436   ∖ cdif 3948   ∪ cun 3949   ∩ cin 3950   ⊆ wss 3951   ⊊ wpss 3952  ∅c0 4333   class class class wbr 5143  ‘cfv 6561  (class class class)co 7431   No csur 27684   <s cslt 27685   bday cbday 27686   ≤s csle 27789   <<s csslt 27825   |s cscut 27827   O cold 27882   L cleft 27884   R cright 27885

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-1o 8506  df-2o 8507  df-no 27687  df-slt 27688  df-bday 27689  df-sle 27790  df-sslt 27826  df-scut 27828  df-made 27886  df-old 27887  df-left 27889  df-right 27890

This theorem is referenced by:  slelss  27946