ltslpss

		Ref	Expression
	Assertion	ltslpss	$⊢ (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		oldno	$⊢ x \in Old (bday (X)) \to x \in No$
2	1	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$
3		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$
4		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$
5		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$
6		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$
7	2 3 4 5 6	ltstrd	$⊢ (((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	7	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))$
9	8	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))$
10		fveq2	$⊢ bday (X) = bday (Y) \to Old (bday (X)) = Old (bday (Y))$
11	10	3ad2ant3	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to Old (bday (X)) = Old (bday (Y))$
12	11	adantr	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \to Old (bday (X)) = Old (bday (Y))$
13	12	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)))$
14	13	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))$
15	9 14	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))$
16		leftval	$⊢ L (X) = \{x \in Old (bday (X)) \| x <_{s} X\}$
17	16	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\}$
18	17	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\})$
19		rabid	$⊢ x \in \{x \in Old (bday (X)) \| x <_{s} X\} \leftrightarrow (x \in Old (bday (X)) \land x <_{s} X)$
20	18 19	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))$
21		leftval	$⊢ L (Y) = \{x \in Old (bday (Y)) \| x <_{s} Y\}$
22	21	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\}$
23	22	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\})$
24		rabid	$⊢ x \in \{x \in Old (bday (Y)) \| x <_{s} Y\} \leftrightarrow (x \in Old (bday (Y)) \land x <_{s} Y)$
25	23 24	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))$
26	15 20 25	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))$
27	26	ssrdv	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \to L (X) \subseteq L (Y)$
28		ltsirr	$⊢ Y \in No \to \neg Y <_{s} Y$
29	28	3ad2ant2	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to \neg Y <_{s} Y$
30		breq1	$⊢ X = Y \to (X <_{s} Y \leftrightarrow Y <_{s} Y)$
31	30	notbid	$⊢ X = Y \to (\neg X <_{s} Y \leftrightarrow \neg Y <_{s} Y)$
32	29 31	syl5ibrcom	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to (X = Y \to \neg X <_{s} Y)$
33	32	con2d	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to (X <_{s} Y \to \neg X = Y)$
34	33	imp	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \to \neg X = Y$
35		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)$
36		lruneq	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to L (X) \cup R (X) = L (Y) \cup R (Y)$
37	36	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)$
38	37	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)$
39	38 35	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)$
40		difundir	$⊢ (L (X) \cup R (X)) ∖ L (X) = (L (X) ∖ L (X)) \cup (R (X) ∖ L (X))$
41		difid	$⊢ L (X) ∖ L (X) = \emptyset$
42	41	uneq1i	$⊢ (L (X) ∖ L (X)) \cup (R (X) ∖ L (X)) = \emptyset \cup (R (X) ∖ L (X))$
43		0un	$⊢ \emptyset \cup (R (X) ∖ L (X)) = R (X) ∖ L (X)$
44	40 42 43	3eqtri	$⊢ (L (X) \cup R (X)) ∖ L (X) = R (X) ∖ L (X)$
45		incom	$⊢ L (X) \cap R (X) = R (X) \cap L (X)$
46		lltr	$⊢ L (X) ≪_{s} R (X)$
47		sltsdisj	$⊢ L (X) ≪_{s} R (X) \to L (X) \cap R (X) = \emptyset$
48	46 47	mp1i	$⊢ (((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$
49	45 48	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$
50		disjdif2	$⊢ R (X) \cap L (X) = \emptyset \to R (X) ∖ L (X) = R (X)$
51	49 50	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)$
52	44 51	eqtrid	$⊢ (((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)$
53		difundir	$⊢ (L (Y) \cup R (Y)) ∖ L (Y) = (L (Y) ∖ L (Y)) \cup (R (Y) ∖ L (Y))$
54		difid	$⊢ L (Y) ∖ L (Y) = \emptyset$
55	54	uneq1i	$⊢ (L (Y) ∖ L (Y)) \cup (R (Y) ∖ L (Y)) = \emptyset \cup (R (Y) ∖ L (Y))$
56		0un	$⊢ \emptyset \cup (R (Y) ∖ L (Y)) = R (Y) ∖ L (Y)$
57	53 55 56	3eqtri	$⊢ (L (Y) \cup R (Y)) ∖ L (Y) = R (Y) ∖ L (Y)$
58		incom	$⊢ L (Y) \cap R (Y) = R (Y) \cap L (Y)$
59		lltr	$⊢ L (Y) ≪_{s} R (Y)$
60		sltsdisj	$⊢ L (Y) ≪_{s} R (Y) \to L (Y) \cap R (Y) = \emptyset$
61	59 60	mp1i	$⊢ (((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$
62	58 61	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$
63		disjdif2	$⊢ R (Y) \cap L (Y) = \emptyset \to R (Y) ∖ L (Y) = R (Y)$
64	62 63	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)$
65	57 64	eqtrid	$⊢ (((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)$
66	39 52 65	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)$
67	35 66	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)$
68		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$
69		lrcut	$⊢ X \in No \to L (X) \|_{s} R (X) = X$
70	68 69	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$
71		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$
72		lrcut	$⊢ Y \in No \to L (Y) \|_{s} R (Y) = Y$
73	71 72	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$
74	67 70 73	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$
75	34 74	mtand	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \to \neg L (X) = L (Y)$
76		dfpss2	$⊢ L (X) \subset L (Y) \leftrightarrow (L (X) \subseteq L (Y) \land \neg L (X) = L (Y))$
77	27 75 76	sylanbrc	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \to L (X) \subset L (Y)$
78	77	ex	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to (X <_{s} Y \to L (X) \subset L (Y))$
79		dfpss3	$⊢ L (X) \subset L (Y) \leftrightarrow (L (X) \subseteq L (Y) \land \neg L (Y) \subseteq L (X))$
80		ssdif0	$⊢ L (Y) \subseteq L (X) \leftrightarrow L (Y) ∖ L (X) = \emptyset$
81	80	necon3bbii	$⊢ \neg L (Y) \subseteq L (X) \leftrightarrow L (Y) ∖ L (X) \neq \emptyset$
82		n0	$⊢ L (Y) ∖ L (X) \neq \emptyset \leftrightarrow \exists x x \in (L (Y) ∖ L (X))$
83	81 82	bitri	$⊢ \neg L (Y) \subseteq L (X) \leftrightarrow \exists x x \in (L (Y) ∖ L (X))$
84		eldif	$⊢ x \in (L (Y) ∖ L (X)) \leftrightarrow (x \in L (Y) \land \neg x \in L (X))$
85	21	a1i	$⊢ Y \in No \to L (Y) = \{x \in Old (bday (Y)) \| x <_{s} Y\}$
86	85	eleq2d	$⊢ Y \in No \to (x \in L (Y) \leftrightarrow x \in \{x \in Old (bday (Y)) \| x <_{s} Y\})$
87	86 24	bitrdi	$⊢ Y \in No \to (x \in L (Y) \leftrightarrow (x \in Old (bday (Y)) \land x <_{s} Y))$
88	16	a1i	$⊢ X \in No \to L (X) = \{x \in Old (bday (X)) \| x <_{s} X\}$
89	88	eleq2d	$⊢ X \in No \to (x \in L (X) \leftrightarrow x \in \{x \in Old (bday (X)) \| x <_{s} X\})$
90	89 19	bitrdi	$⊢ X \in No \to (x \in L (X) \leftrightarrow (x \in Old (bday (X)) \land x <_{s} X))$
91	90	notbid	$⊢ X \in No \to (\neg x \in L (X) \leftrightarrow \neg (x \in Old (bday (X)) \land x <_{s} X))$
92		ianor	$⊢ \neg (x \in Old (bday (X)) \land x <_{s} X) \leftrightarrow (\neg x \in Old (bday (X)) \lor \neg x <_{s} X)$
93	91 92	bitrdi	$⊢ X \in No \to (\neg x \in L (X) \leftrightarrow (\neg x \in Old (bday (X)) \lor \neg x <_{s} X))$
94	87 93	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)))$
95	94	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)))$
96		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))$
97		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)$
98	97	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))$
99	96 98	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))$
100	99	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)$
101		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$
102	96	oldnod	$⊢ ((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$
103	102	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$
104		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$
105		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$
106		lenlts	$⊢ (X \in No \land x \in No) \to (X \leq_{s} x \leftrightarrow \neg x <_{s} X)$
107	105 102 106	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)$
108	107	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$
109		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$
110	101 103 104 108 109	leltstrd	$⊢ (((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$
111	110	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)$
112	100 111	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)$
113	112	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)$
114	95 113	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)$
115	84 114	biimtrid	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to (x \in (L (Y) ∖ L (X)) \to X <_{s} Y)$
116	115	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)$
117	83 116	biimtrid	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to (\neg L (Y) \subseteq L (X) \to X <_{s} Y)$
118	117	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)$
119	79 118	biimtrid	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to (L (X) \subset L (Y) \to X <_{s} Y)$
120	78 119	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 ltslpss

Proof