sltlpss

		Ref	Expression
	Assertion	sltlpss	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to (X <_{s} Y \leftrightarrow L (X) \subset L (Y))$

Proof

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

Metamath Proof Explorer

Theorem sltlpss

Proof