lesrec

Description: A comparison law for surreals considered as cuts of sets of surreals. Definition from Conway p. 4. Theorem 4 of Alling p. 186. Theorem 2.5 of Gonshor p. 9. (Contributed by Scott Fenton, 11-Dec-2021)

		Ref	Expression
	Assertion	lesrec	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to (X \leq_{s} Y \leftrightarrow (\forall d \in D X <_{s} d \land \forall a \in A a <_{s} Y))$

Proof

Step	Hyp	Ref	Expression
1		cutscl	$⊢ A ≪_{s} B \to A \|_{s} B \in No$
2	1	ad3antrrr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \land d \in D) \to A \|_{s} B \in No$
3		cutscl	$⊢ C ≪_{s} D \to C \|_{s} D \in No$
4	3	ad3antlr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \land d \in D) \to C \|_{s} D \in No$
5		sltsss2	$⊢ C ≪_{s} D \to D \subseteq No$
6	5	ad2antlr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \to D \subseteq No$
7	6	sselda	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \land d \in D) \to d \in No$
8		simplr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \land d \in D) \to (A \|_{s} B) \leq_{s} (C \|_{s} D)$
9		cutcuts	$⊢ C ≪_{s} D \to (C \|_{s} D \in No \land C ≪_{s} \{C \|_{s} D\} \land \{C \|_{s} D\} ≪_{s} D)$
10	9	simp3d	$⊢ C ≪_{s} D \to \{C \|_{s} D\} ≪_{s} D$
11	10	ad2antlr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \to \{C \|_{s} D\} ≪_{s} D$
12		sltssep	$⊢ \{C \|_{s} D\} ≪_{s} D \to \forall a \in \{C \|_{s} D\} \forall d \in D a <_{s} d$
13	11 12	syl	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \to \forall a \in \{C \|_{s} D\} \forall d \in D a <_{s} d$
14		ovex	$⊢ C \|_{s} D \in V$
15		breq1	$⊢ a = C \|_{s} D \to (a <_{s} d \leftrightarrow (C \|_{s} D) <_{s} d)$
16	15	ralbidv	$⊢ a = C \|_{s} D \to (\forall d \in D a <_{s} d \leftrightarrow \forall d \in D (C \|_{s} D) <_{s} d)$
17	14 16	ralsn	$⊢ \forall a \in \{C \|_{s} D\} \forall d \in D a <_{s} d \leftrightarrow \forall d \in D (C \|_{s} D) <_{s} d$
18	13 17	sylib	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \to \forall d \in D (C \|_{s} D) <_{s} d$
19	18	r19.21bi	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \land d \in D) \to (C \|_{s} D) <_{s} d$
20	2 4 7 8 19	leltstrd	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \land d \in D) \to (A \|_{s} B) <_{s} d$
21	20	ralrimiva	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \to \forall d \in D (A \|_{s} B) <_{s} d$
22		sltsss1	$⊢ A ≪_{s} B \to A \subseteq No$
23	22	adantr	$⊢ (A ≪_{s} B \land C ≪_{s} D) \to A \subseteq No$
24	23	adantr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \to A \subseteq No$
25	24	sselda	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \land a \in A) \to a \in No$
26	1	ad3antrrr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \land a \in A) \to A \|_{s} B \in No$
27	3	ad3antlr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \land a \in A) \to C \|_{s} D \in No$
28		cutcuts	$⊢ A ≪_{s} B \to (A \|_{s} B \in No \land A ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} B)$
29	28	simp2d	$⊢ A ≪_{s} B \to A ≪_{s} \{A \|_{s} B\}$
30	29	adantr	$⊢ (A ≪_{s} B \land C ≪_{s} D) \to A ≪_{s} \{A \|_{s} B\}$
31	30	adantr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \to A ≪_{s} \{A \|_{s} B\}$
32		sltssep	$⊢ A ≪_{s} \{A \|_{s} B\} \to \forall a \in A \forall d \in \{A \|_{s} B\} a <_{s} d$
33	31 32	syl	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \to \forall a \in A \forall d \in \{A \|_{s} B\} a <_{s} d$
34	33	r19.21bi	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \land a \in A) \to \forall d \in \{A \|_{s} B\} a <_{s} d$
35		ovex	$⊢ A \|_{s} B \in V$
36		breq2	$⊢ d = A \|_{s} B \to (a <_{s} d \leftrightarrow a <_{s} (A \|_{s} B))$
37	35 36	ralsn	$⊢ \forall d \in \{A \|_{s} B\} a <_{s} d \leftrightarrow a <_{s} (A \|_{s} B)$
38	34 37	sylib	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \land a \in A) \to a <_{s} (A \|_{s} B)$
39		simplr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \land a \in A) \to (A \|_{s} B) \leq_{s} (C \|_{s} D)$
40	25 26 27 38 39	ltlestrd	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \land a \in A) \to a <_{s} (C \|_{s} D)$
41	40	ralrimiva	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \to \forall a \in A a <_{s} (C \|_{s} D)$
42	21 41	jca	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (A \|_{s} B) \leq_{s} (C \|_{s} D)) \to (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))$
43		bdayon	$⊢ bday (A \|_{s} B) \in On$
44	43	onordi	$⊢ Ord bday (A \|_{s} B)$
45		ordn2lp	$⊢ Ord bday (A \|_{s} B) \to \neg (bday (A \|_{s} B) \in bday (C \|_{s} D) \land bday (C \|_{s} D) \in bday (A \|_{s} B))$
46	44 45	ax-mp	$⊢ \neg (bday (A \|_{s} B) \in bday (C \|_{s} D) \land bday (C \|_{s} D) \in bday (A \|_{s} B))$
47	3	ad2antlr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \to C \|_{s} D \in No$
48	1	adantr	$⊢ (A ≪_{s} B \land C ≪_{s} D) \to A \|_{s} B \in No$
49	48	adantr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \to A \|_{s} B \in No$
50		ltnles	$⊢ (C \|_{s} D \in No \land A \|_{s} B \in No) \to ((C \|_{s} D) <_{s} (A \|_{s} B) \leftrightarrow \neg (A \|_{s} B) \leq_{s} (C \|_{s} D))$
51	47 49 50	syl2anc	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \to ((C \|_{s} D) <_{s} (A \|_{s} B) \leftrightarrow \neg (A \|_{s} B) \leq_{s} (C \|_{s} D))$
52	3	ad3antlr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to C \|_{s} D \in No$
53		sltsex1	$⊢ A ≪_{s} B \to A \in V$
54	53	ad3antrrr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to A \in V$
55		snex	$⊢ \{C \|_{s} D\} \in V$
56	54 55	jctir	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to (A \in V \land \{C \|_{s} D\} \in V)$
57	22	ad3antrrr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to A \subseteq No$
58	52	snssd	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \{C \|_{s} D\} \subseteq No$
59		simplrr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \forall a \in A a <_{s} (C \|_{s} D)$
60		breq2	$⊢ d = C \|_{s} D \to (a <_{s} d \leftrightarrow a <_{s} (C \|_{s} D))$
61	14 60	ralsn	$⊢ \forall d \in \{C \|_{s} D\} a <_{s} d \leftrightarrow a <_{s} (C \|_{s} D)$
62	61	ralbii	$⊢ \forall a \in A \forall d \in \{C \|_{s} D\} a <_{s} d \leftrightarrow \forall a \in A a <_{s} (C \|_{s} D)$
63	59 62	sylibr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \forall a \in A \forall d \in \{C \|_{s} D\} a <_{s} d$
64	57 58 63	3jca	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to (A \subseteq No \land \{C \|_{s} D\} \subseteq No \land \forall a \in A \forall d \in \{C \|_{s} D\} a <_{s} d)$
65		brslts	$⊢ A ≪_{s} \{C \|_{s} D\} \leftrightarrow ((A \in V \land \{C \|_{s} D\} \in V) \land (A \subseteq No \land \{C \|_{s} D\} \subseteq No \land \forall a \in A \forall d \in \{C \|_{s} D\} a <_{s} d))$
66	56 64 65	sylanbrc	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to A ≪_{s} \{C \|_{s} D\}$
67		sltsex2	$⊢ A ≪_{s} B \to B \in V$
68	67	ad3antrrr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to B \in V$
69	68 55	jctil	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to (\{C \|_{s} D\} \in V \land B \in V)$
70		sltsss2	$⊢ A ≪_{s} B \to B \subseteq No$
71	70	ad3antrrr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to B \subseteq No$
72	52	adantr	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land b \in B) \to C \|_{s} D \in No$
73	48	ad3antrrr	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land b \in B) \to A \|_{s} B \in No$
74	71	sselda	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land b \in B) \to b \in No$
75		simplr	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land b \in B) \to (C \|_{s} D) <_{s} (A \|_{s} B)$
76	28	simp3d	$⊢ A ≪_{s} B \to \{A \|_{s} B\} ≪_{s} B$
77	76	ad3antrrr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \{A \|_{s} B\} ≪_{s} B$
78		sltssep	$⊢ \{A \|_{s} B\} ≪_{s} B \to \forall a \in \{A \|_{s} B\} \forall b \in B a <_{s} b$
79	77 78	syl	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \forall a \in \{A \|_{s} B\} \forall b \in B a <_{s} b$
80		breq1	$⊢ a = A \|_{s} B \to (a <_{s} b \leftrightarrow (A \|_{s} B) <_{s} b)$
81	80	ralbidv	$⊢ a = A \|_{s} B \to (\forall b \in B a <_{s} b \leftrightarrow \forall b \in B (A \|_{s} B) <_{s} b)$
82	35 81	ralsn	$⊢ \forall a \in \{A \|_{s} B\} \forall b \in B a <_{s} b \leftrightarrow \forall b \in B (A \|_{s} B) <_{s} b$
83	79 82	sylib	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \forall b \in B (A \|_{s} B) <_{s} b$
84	83	r19.21bi	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land b \in B) \to (A \|_{s} B) <_{s} b$
85	72 73 74 75 84	ltstrd	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land b \in B) \to (C \|_{s} D) <_{s} b$
86	85	ralrimiva	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \forall b \in B (C \|_{s} D) <_{s} b$
87		breq1	$⊢ a = C \|_{s} D \to (a <_{s} b \leftrightarrow (C \|_{s} D) <_{s} b)$
88	87	ralbidv	$⊢ a = C \|_{s} D \to (\forall b \in B a <_{s} b \leftrightarrow \forall b \in B (C \|_{s} D) <_{s} b)$
89	14 88	ralsn	$⊢ \forall a \in \{C \|_{s} D\} \forall b \in B a <_{s} b \leftrightarrow \forall b \in B (C \|_{s} D) <_{s} b$
90	86 89	sylibr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \forall a \in \{C \|_{s} D\} \forall b \in B a <_{s} b$
91	58 71 90	3jca	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to (\{C \|_{s} D\} \subseteq No \land B \subseteq No \land \forall a \in \{C \|_{s} D\} \forall b \in B a <_{s} b)$
92		brslts	$⊢ \{C \|_{s} D\} ≪_{s} B \leftrightarrow ((\{C \|_{s} D\} \in V \land B \in V) \land (\{C \|_{s} D\} \subseteq No \land B \subseteq No \land \forall a \in \{C \|_{s} D\} \forall b \in B a <_{s} b))$
93	69 91 92	sylanbrc	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \{C \|_{s} D\} ≪_{s} B$
94		ltsirr	$⊢ A \|_{s} B \in No \to \neg (A \|_{s} B) <_{s} (A \|_{s} B)$
95	49 94	syl	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \to \neg (A \|_{s} B) <_{s} (A \|_{s} B)$
96		breq1	$⊢ A \|_{s} B = C \|_{s} D \to ((A \|_{s} B) <_{s} (A \|_{s} B) \leftrightarrow (C \|_{s} D) <_{s} (A \|_{s} B))$
97	96	notbid	$⊢ A \|_{s} B = C \|_{s} D \to (\neg (A \|_{s} B) <_{s} (A \|_{s} B) \leftrightarrow \neg (C \|_{s} D) <_{s} (A \|_{s} B))$
98	95 97	syl5ibcom	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \to (A \|_{s} B = C \|_{s} D \to \neg (C \|_{s} D) <_{s} (A \|_{s} B))$
99	98	necon2ad	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \to ((C \|_{s} D) <_{s} (A \|_{s} B) \to A \|_{s} B \neq C \|_{s} D)$
100	99	imp	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to A \|_{s} B \neq C \|_{s} D$
101	100	necomd	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to C \|_{s} D \neq A \|_{s} B$
102		cutbdaylt	$⊢ (C \|_{s} D \in No \land (A ≪_{s} \{C \|_{s} D\} \land \{C \|_{s} D\} ≪_{s} B) \land C \|_{s} D \neq A \|_{s} B) \to bday (A \|_{s} B) \in bday (C \|_{s} D)$
103	52 66 93 101 102	syl121anc	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to bday (A \|_{s} B) \in bday (C \|_{s} D)$
104	1	ad3antrrr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to A \|_{s} B \in No$
105		sltsex1	$⊢ C ≪_{s} D \to C \in V$
106	105	ad3antlr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to C \in V$
107		snex	$⊢ \{A \|_{s} B\} \in V$
108	106 107	jctir	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to (C \in V \land \{A \|_{s} B\} \in V)$
109		sltsss1	$⊢ C ≪_{s} D \to C \subseteq No$
110	109	ad3antlr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to C \subseteq No$
111	104	snssd	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \{A \|_{s} B\} \subseteq No$
112	110	sselda	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land c \in C) \to c \in No$
113	52	adantr	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land c \in C) \to C \|_{s} D \in No$
114	48	ad3antrrr	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land c \in C) \to A \|_{s} B \in No$
115	9	simp2d	$⊢ C ≪_{s} D \to C ≪_{s} \{C \|_{s} D\}$
116	115	ad3antlr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to C ≪_{s} \{C \|_{s} D\}$
117		sltssep	$⊢ C ≪_{s} \{C \|_{s} D\} \to \forall c \in C \forall d \in \{C \|_{s} D\} c <_{s} d$
118	116 117	syl	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \forall c \in C \forall d \in \{C \|_{s} D\} c <_{s} d$
119	118	r19.21bi	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land c \in C) \to \forall d \in \{C \|_{s} D\} c <_{s} d$
120		breq2	$⊢ d = C \|_{s} D \to (c <_{s} d \leftrightarrow c <_{s} (C \|_{s} D))$
121	14 120	ralsn	$⊢ \forall d \in \{C \|_{s} D\} c <_{s} d \leftrightarrow c <_{s} (C \|_{s} D)$
122	119 121	sylib	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land c \in C) \to c <_{s} (C \|_{s} D)$
123		simplr	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land c \in C) \to (C \|_{s} D) <_{s} (A \|_{s} B)$
124	112 113 114 122 123	ltstrd	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land c \in C) \to c <_{s} (A \|_{s} B)$
125		breq2	$⊢ a = A \|_{s} B \to (c <_{s} a \leftrightarrow c <_{s} (A \|_{s} B))$
126	35 125	ralsn	$⊢ \forall a \in \{A \|_{s} B\} c <_{s} a \leftrightarrow c <_{s} (A \|_{s} B)$
127	124 126	sylibr	$⊢ ((((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \land c \in C) \to \forall a \in \{A \|_{s} B\} c <_{s} a$
128	127	ralrimiva	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \forall c \in C \forall a \in \{A \|_{s} B\} c <_{s} a$
129	110 111 128	3jca	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to (C \subseteq No \land \{A \|_{s} B\} \subseteq No \land \forall c \in C \forall a \in \{A \|_{s} B\} c <_{s} a)$
130		brslts	$⊢ C ≪_{s} \{A \|_{s} B\} \leftrightarrow ((C \in V \land \{A \|_{s} B\} \in V) \land (C \subseteq No \land \{A \|_{s} B\} \subseteq No \land \forall c \in C \forall a \in \{A \|_{s} B\} c <_{s} a))$
131	108 129 130	sylanbrc	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to C ≪_{s} \{A \|_{s} B\}$
132		sltsex2	$⊢ C ≪_{s} D \to D \in V$
133	132	ad3antlr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to D \in V$
134	133 107	jctil	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to (\{A \|_{s} B\} \in V \land D \in V)$
135	5	ad3antlr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to D \subseteq No$
136		simplrl	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \forall d \in D (A \|_{s} B) <_{s} d$
137		breq1	$⊢ a = A \|_{s} B \to (a <_{s} d \leftrightarrow (A \|_{s} B) <_{s} d)$
138	137	ralbidv	$⊢ a = A \|_{s} B \to (\forall d \in D a <_{s} d \leftrightarrow \forall d \in D (A \|_{s} B) <_{s} d)$
139	35 138	ralsn	$⊢ \forall a \in \{A \|_{s} B\} \forall d \in D a <_{s} d \leftrightarrow \forall d \in D (A \|_{s} B) <_{s} d$
140	136 139	sylibr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \forall a \in \{A \|_{s} B\} \forall d \in D a <_{s} d$
141	111 135 140	3jca	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to (\{A \|_{s} B\} \subseteq No \land D \subseteq No \land \forall a \in \{A \|_{s} B\} \forall d \in D a <_{s} d)$
142		brslts	$⊢ \{A \|_{s} B\} ≪_{s} D \leftrightarrow ((\{A \|_{s} B\} \in V \land D \in V) \land (\{A \|_{s} B\} \subseteq No \land D \subseteq No \land \forall a \in \{A \|_{s} B\} \forall d \in D a <_{s} d))$
143	134 141 142	sylanbrc	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to \{A \|_{s} B\} ≪_{s} D$
144		cutbdaylt	$⊢ (A \|_{s} B \in No \land (C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land A \|_{s} B \neq C \|_{s} D) \to bday (C \|_{s} D) \in bday (A \|_{s} B)$
145	104 131 143 100 144	syl121anc	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to bday (C \|_{s} D) \in bday (A \|_{s} B)$
146	103 145	jca	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \land (C \|_{s} D) <_{s} (A \|_{s} B)) \to (bday (A \|_{s} B) \in bday (C \|_{s} D) \land bday (C \|_{s} D) \in bday (A \|_{s} B))$
147	146	ex	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \to ((C \|_{s} D) <_{s} (A \|_{s} B) \to (bday (A \|_{s} B) \in bday (C \|_{s} D) \land bday (C \|_{s} D) \in bday (A \|_{s} B)))$
148	51 147	sylbird	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \to (\neg (A \|_{s} B) \leq_{s} (C \|_{s} D) \to (bday (A \|_{s} B) \in bday (C \|_{s} D) \land bday (C \|_{s} D) \in bday (A \|_{s} B)))$
149	46 148	mt3i	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))) \to (A \|_{s} B) \leq_{s} (C \|_{s} D)$
150	42 149	impbida	$⊢ (A ≪_{s} B \land C ≪_{s} D) \to ((A \|_{s} B) \leq_{s} (C \|_{s} D) \leftrightarrow (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D)))$
151		breq12	$⊢ (X = A \|_{s} B \land Y = C \|_{s} D) \to (X \leq_{s} Y \leftrightarrow (A \|_{s} B) \leq_{s} (C \|_{s} D))$
152		breq1	$⊢ X = A \|_{s} B \to (X <_{s} d \leftrightarrow (A \|_{s} B) <_{s} d)$
153	152	ralbidv	$⊢ X = A \|_{s} B \to (\forall d \in D X <_{s} d \leftrightarrow \forall d \in D (A \|_{s} B) <_{s} d)$
154		breq2	$⊢ Y = C \|_{s} D \to (a <_{s} Y \leftrightarrow a <_{s} (C \|_{s} D))$
155	154	ralbidv	$⊢ Y = C \|_{s} D \to (\forall a \in A a <_{s} Y \leftrightarrow \forall a \in A a <_{s} (C \|_{s} D))$
156	153 155	bi2anan9	$⊢ (X = A \|_{s} B \land Y = C \|_{s} D) \to ((\forall d \in D X <_{s} d \land \forall a \in A a <_{s} Y) \leftrightarrow (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D)))$
157	151 156	bibi12d	$⊢ (X = A \|_{s} B \land Y = C \|_{s} D) \to ((X \leq_{s} Y \leftrightarrow (\forall d \in D X <_{s} d \land \forall a \in A a <_{s} Y)) \leftrightarrow ((A \|_{s} B) \leq_{s} (C \|_{s} D) \leftrightarrow (\forall d \in D (A \|_{s} B) <_{s} d \land \forall a \in A a <_{s} (C \|_{s} D))))$
158	150 157	imbitrrid	$⊢ (X = A \|_{s} B \land Y = C \|_{s} D) \to ((A ≪_{s} B \land C ≪_{s} D) \to (X \leq_{s} Y \leftrightarrow (\forall d \in D X <_{s} d \land \forall a \in A a <_{s} Y)))$
159	158	impcom	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to (X \leq_{s} Y \leftrightarrow (\forall d \in D X <_{s} d \land \forall a \in A a <_{s} Y))$

Metamath Proof Explorer

Theorem lesrec

Proof