conway

Description: Conway's Simplicity Theorem. Given A preceeding B , there is a unique surreal of minimal length separating them. This is a fundamental property of surreals and will be used (via surreal cuts) to prove many properties later on. Theorem from Alling p. 185. (Contributed by Scott Fenton, 8-Dec-2021)

		Ref	Expression
	Assertion	conway	$⊢ A ≪_{s} B \to \exists! x \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} bday (x) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$

Proof

Step	Hyp	Ref	Expression
1		ssltss1	$⊢ A ≪_{s} B \to A \subseteq No$
2		ssltex1	$⊢ A ≪_{s} B \to A \in V$
3		ssltss2	$⊢ A ≪_{s} B \to B \subseteq No$
4		ssltex2	$⊢ A ≪_{s} B \to B \in V$
5		ssltsep	$⊢ A ≪_{s} B \to \forall p \in A \forall q \in B p <_{s} q$
6		noeta2	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall p \in A \forall q \in B p <_{s} q) \to \exists y \in No (\forall p \in A p <_{s} y \land \forall q \in B y <_{s} q \land bday (y) \subseteq suc ⋃ bday [A \cup B])$
7	1 2 3 4 5 6	syl221anc	$⊢ A ≪_{s} B \to \exists y \in No (\forall p \in A p <_{s} y \land \forall q \in B y <_{s} q \land bday (y) \subseteq suc ⋃ bday [A \cup B])$
8		3simpa	$⊢ (\forall p \in A p <_{s} y \land \forall q \in B y <_{s} q \land bday (y) \subseteq suc ⋃ bday [A \cup B]) \to (\forall p \in A p <_{s} y \land \forall q \in B y <_{s} q)$
9	2	ad2antrr	$⊢ ((A ≪_{s} B \land y \in No) \land \forall p \in A p <_{s} y) \to A \in V$
10		vsnex	$⊢ \{y\} \in V$
11	9 10	jctir	$⊢ ((A ≪_{s} B \land y \in No) \land \forall p \in A p <_{s} y) \to (A \in V \land \{y\} \in V)$
12	1	ad2antrr	$⊢ ((A ≪_{s} B \land y \in No) \land \forall p \in A p <_{s} y) \to A \subseteq No$
13		snssi	$⊢ y \in No \to \{y\} \subseteq No$
14	13	adantl	$⊢ (A ≪_{s} B \land y \in No) \to \{y\} \subseteq No$
15	14	adantr	$⊢ ((A ≪_{s} B \land y \in No) \land \forall p \in A p <_{s} y) \to \{y\} \subseteq No$
16		vex	$⊢ y \in V$
17		breq2	$⊢ q = y \to (p <_{s} q \leftrightarrow p <_{s} y)$
18	16 17	ralsn	$⊢ \forall q \in \{y\} p <_{s} q \leftrightarrow p <_{s} y$
19	18	ralbii	$⊢ \forall p \in A \forall q \in \{y\} p <_{s} q \leftrightarrow \forall p \in A p <_{s} y$
20	19	biimpri	$⊢ \forall p \in A p <_{s} y \to \forall p \in A \forall q \in \{y\} p <_{s} q$
21	20	adantl	$⊢ ((A ≪_{s} B \land y \in No) \land \forall p \in A p <_{s} y) \to \forall p \in A \forall q \in \{y\} p <_{s} q$
22	12 15 21	3jca	$⊢ ((A ≪_{s} B \land y \in No) \land \forall p \in A p <_{s} y) \to (A \subseteq No \land \{y\} \subseteq No \land \forall p \in A \forall q \in \{y\} p <_{s} q)$
23		brsslt	$⊢ A ≪_{s} \{y\} \leftrightarrow ((A \in V \land \{y\} \in V) \land (A \subseteq No \land \{y\} \subseteq No \land \forall p \in A \forall q \in \{y\} p <_{s} q))$
24	11 22 23	sylanbrc	$⊢ ((A ≪_{s} B \land y \in No) \land \forall p \in A p <_{s} y) \to A ≪_{s} \{y\}$
25	24	ex	$⊢ (A ≪_{s} B \land y \in No) \to (\forall p \in A p <_{s} y \to A ≪_{s} \{y\})$
26	4	ad2antrr	$⊢ ((A ≪_{s} B \land y \in No) \land \forall q \in B y <_{s} q) \to B \in V$
27	26 10	jctil	$⊢ ((A ≪_{s} B \land y \in No) \land \forall q \in B y <_{s} q) \to (\{y\} \in V \land B \in V)$
28	14	adantr	$⊢ ((A ≪_{s} B \land y \in No) \land \forall q \in B y <_{s} q) \to \{y\} \subseteq No$
29	3	ad2antrr	$⊢ ((A ≪_{s} B \land y \in No) \land \forall q \in B y <_{s} q) \to B \subseteq No$
30		ralcom	$⊢ \forall p \in \{y\} \forall q \in B p <_{s} q \leftrightarrow \forall q \in B \forall p \in \{y\} p <_{s} q$
31		breq1	$⊢ p = y \to (p <_{s} q \leftrightarrow y <_{s} q)$
32	16 31	ralsn	$⊢ \forall p \in \{y\} p <_{s} q \leftrightarrow y <_{s} q$
33	32	ralbii	$⊢ \forall q \in B \forall p \in \{y\} p <_{s} q \leftrightarrow \forall q \in B y <_{s} q$
34	30 33	sylbbr	$⊢ \forall q \in B y <_{s} q \to \forall p \in \{y\} \forall q \in B p <_{s} q$
35	34	adantl	$⊢ ((A ≪_{s} B \land y \in No) \land \forall q \in B y <_{s} q) \to \forall p \in \{y\} \forall q \in B p <_{s} q$
36	28 29 35	3jca	$⊢ ((A ≪_{s} B \land y \in No) \land \forall q \in B y <_{s} q) \to (\{y\} \subseteq No \land B \subseteq No \land \forall p \in \{y\} \forall q \in B p <_{s} q)$
37		brsslt	$⊢ \{y\} ≪_{s} B \leftrightarrow ((\{y\} \in V \land B \in V) \land (\{y\} \subseteq No \land B \subseteq No \land \forall p \in \{y\} \forall q \in B p <_{s} q))$
38	27 36 37	sylanbrc	$⊢ ((A ≪_{s} B \land y \in No) \land \forall q \in B y <_{s} q) \to \{y\} ≪_{s} B$
39	38	ex	$⊢ (A ≪_{s} B \land y \in No) \to (\forall q \in B y <_{s} q \to \{y\} ≪_{s} B)$
40	25 39	anim12d	$⊢ (A ≪_{s} B \land y \in No) \to ((\forall p \in A p <_{s} y \land \forall q \in B y <_{s} q) \to (A ≪_{s} \{y\} \land \{y\} ≪_{s} B))$
41	8 40	syl5	$⊢ (A ≪_{s} B \land y \in No) \to ((\forall p \in A p <_{s} y \land \forall q \in B y <_{s} q \land bday (y) \subseteq suc ⋃ bday [A \cup B]) \to (A ≪_{s} \{y\} \land \{y\} ≪_{s} B))$
42	41	reximdva	$⊢ A ≪_{s} B \to (\exists y \in No (\forall p \in A p <_{s} y \land \forall q \in B y <_{s} q \land bday (y) \subseteq suc ⋃ bday [A \cup B]) \to \exists y \in No (A ≪_{s} \{y\} \land \{y\} ≪_{s} B))$
43	7 42	mpd	$⊢ A ≪_{s} B \to \exists y \in No (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)$
44		rabn0	$⊢ \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \neq \emptyset \leftrightarrow \exists y \in No (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)$
45	43 44	sylibr	$⊢ A ≪_{s} B \to \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \neq \emptyset$
46		ssrab2	$⊢ \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \subseteq No$
47	46	a1i	$⊢ A ≪_{s} B \to \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \subseteq No$
48		simplr3	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to r \in No$
49	2	ad2antrr	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to A \in V$
50		vsnex	$⊢ \{r\} \in V$
51	49 50	jctir	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to (A \in V \land \{r\} \in V)$
52	1	ad2antrr	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to A \subseteq No$
53		snssi	$⊢ r \in No \to \{r\} \subseteq No$
54	48 53	syl	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to \{r\} \subseteq No$
55	52	sselda	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land x \in A) \to x \in No$
56		simplr1	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to p \in No$
57	56	adantr	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land x \in A) \to p \in No$
58	48	adantr	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land x \in A) \to r \in No$
59		simplll	$⊢ (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q)) \to A ≪_{s} \{p\}$
60	59	adantl	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to A ≪_{s} \{p\}$
61		ssltsep	$⊢ A ≪_{s} \{p\} \to \forall x \in A \forall y \in \{p\} x <_{s} y$
62	60 61	syl	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to \forall x \in A \forall y \in \{p\} x <_{s} y$
63	62	r19.21bi	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land x \in A) \to \forall y \in \{p\} x <_{s} y$
64		vex	$⊢ p \in V$
65		breq2	$⊢ y = p \to (x <_{s} y \leftrightarrow x <_{s} p)$
66	64 65	ralsn	$⊢ \forall y \in \{p\} x <_{s} y \leftrightarrow x <_{s} p$
67	63 66	sylib	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land x \in A) \to x <_{s} p$
68		simprrl	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to p <_{s} r$
69	68	adantr	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land x \in A) \to p <_{s} r$
70	55 57 58 67 69	slttrd	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land x \in A) \to x <_{s} r$
71		vex	$⊢ r \in V$
72		breq2	$⊢ y = r \to (x <_{s} y \leftrightarrow x <_{s} r)$
73	71 72	ralsn	$⊢ \forall y \in \{r\} x <_{s} y \leftrightarrow x <_{s} r$
74	70 73	sylibr	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land x \in A) \to \forall y \in \{r\} x <_{s} y$
75	74	ralrimiva	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to \forall x \in A \forall y \in \{r\} x <_{s} y$
76	52 54 75	3jca	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to (A \subseteq No \land \{r\} \subseteq No \land \forall x \in A \forall y \in \{r\} x <_{s} y)$
77		brsslt	$⊢ A ≪_{s} \{r\} \leftrightarrow ((A \in V \land \{r\} \in V) \land (A \subseteq No \land \{r\} \subseteq No \land \forall x \in A \forall y \in \{r\} x <_{s} y))$
78	51 76 77	sylanbrc	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to A ≪_{s} \{r\}$
79	4	ad2antrr	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to B \in V$
80	79 50	jctil	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to (\{r\} \in V \land B \in V)$
81	3	ad2antrr	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to B \subseteq No$
82	48	adantr	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land y \in B) \to r \in No$
83		simplr2	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to q \in No$
84	83	adantr	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land y \in B) \to q \in No$
85	81	sselda	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land y \in B) \to y \in No$
86		simprrr	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to r <_{s} q$
87	86	adantr	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land y \in B) \to r <_{s} q$
88		simplrr	$⊢ (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q)) \to \{q\} ≪_{s} B$
89	88	adantl	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to \{q\} ≪_{s} B$
90		ssltsep	$⊢ \{q\} ≪_{s} B \to \forall x \in \{q\} \forall y \in B x <_{s} y$
91	89 90	syl	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to \forall x \in \{q\} \forall y \in B x <_{s} y$
92		vex	$⊢ q \in V$
93		breq1	$⊢ x = q \to (x <_{s} y \leftrightarrow q <_{s} y)$
94	93	ralbidv	$⊢ x = q \to (\forall y \in B x <_{s} y \leftrightarrow \forall y \in B q <_{s} y)$
95	92 94	ralsn	$⊢ \forall x \in \{q\} \forall y \in B x <_{s} y \leftrightarrow \forall y \in B q <_{s} y$
96	91 95	sylib	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to \forall y \in B q <_{s} y$
97	96	r19.21bi	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land y \in B) \to q <_{s} y$
98	82 84 85 87 97	slttrd	$⊢ (((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \land y \in B) \to r <_{s} y$
99	98	ralrimiva	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to \forall y \in B r <_{s} y$
100		breq1	$⊢ x = r \to (x <_{s} y \leftrightarrow r <_{s} y)$
101	100	ralbidv	$⊢ x = r \to (\forall y \in B x <_{s} y \leftrightarrow \forall y \in B r <_{s} y)$
102	71 101	ralsn	$⊢ \forall x \in \{r\} \forall y \in B x <_{s} y \leftrightarrow \forall y \in B r <_{s} y$
103	99 102	sylibr	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to \forall x \in \{r\} \forall y \in B x <_{s} y$
104	54 81 103	3jca	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to (\{r\} \subseteq No \land B \subseteq No \land \forall x \in \{r\} \forall y \in B x <_{s} y)$
105		brsslt	$⊢ \{r\} ≪_{s} B \leftrightarrow ((\{r\} \in V \land B \in V) \land (\{r\} \subseteq No \land B \subseteq No \land \forall x \in \{r\} \forall y \in B x <_{s} y))$
106	80 104 105	sylanbrc	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to \{r\} ≪_{s} B$
107	48 78 106	jca32	$⊢ ((A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \land (((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \land (A ≪_{s} \{q\} \land \{q\} ≪_{s} B)) \land (p <_{s} r \land r <_{s} q))) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))$
108	107	exp44	$⊢ (A ≪_{s} B \land (p \in No \land q \in No \land r \in No)) \to ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))))$
109	108	ralrimivvva	$⊢ A ≪_{s} B \to \forall p \in No \forall q \in No \forall r \in No ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))))$
110		sneq	$⊢ y = p \to \{y\} = \{p\}$
111	110	breq2d	$⊢ y = p \to (A ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{p\})$
112	110	breq1d	$⊢ y = p \to (\{y\} ≪_{s} B \leftrightarrow \{p\} ≪_{s} B)$
113	111 112	anbi12d	$⊢ y = p \to ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{p\} \land \{p\} ≪_{s} B))$
114	113	ralrab	$⊢ \forall p \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall q \in No \forall r \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))) \leftrightarrow \forall p \in No ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to \forall q \in No \forall r \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))))$
115		sneq	$⊢ y = q \to \{y\} = \{q\}$
116	115	breq2d	$⊢ y = q \to (A ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{q\})$
117	115	breq1d	$⊢ y = q \to (\{y\} ≪_{s} B \leftrightarrow \{q\} ≪_{s} B)$
118	116 117	anbi12d	$⊢ y = q \to ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{q\} \land \{q\} ≪_{s} B))$
119	118	ralrab	$⊢ \forall q \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall r \in No ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))) \leftrightarrow \forall q \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to \forall r \in No ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))))$
120		sneq	$⊢ y = r \to \{y\} = \{r\}$
121	120	breq2d	$⊢ y = r \to (A ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{r\})$
122	120	breq1d	$⊢ y = r \to (\{y\} ≪_{s} B \leftrightarrow \{r\} ≪_{s} B)$
123	121 122	anbi12d	$⊢ y = r \to ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))$
124	123	elrab	$⊢ r \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \leftrightarrow (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))$
125	124	imbi2i	$⊢ ((p <_{s} r \land r <_{s} q) \to r \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}) \leftrightarrow ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))$
126	125	ralbii	$⊢ \forall r \in No ((p <_{s} r \land r <_{s} q) \to r \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}) \leftrightarrow \forall r \in No ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))$
127	126	ralbii	$⊢ \forall q \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall r \in No ((p <_{s} r \land r <_{s} q) \to r \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}) \leftrightarrow \forall q \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall r \in No ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))$
128		r19.21v	$⊢ \forall r \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))) \leftrightarrow ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to \forall r \in No ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))))$
129	128	ralbii	$⊢ \forall q \in No \forall r \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))) \leftrightarrow \forall q \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to \forall r \in No ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))))$
130	119 127 129	3bitr4i	$⊢ \forall q \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall r \in No ((p <_{s} r \land r <_{s} q) \to r \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}) \leftrightarrow \forall q \in No \forall r \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))))$
131	130	ralbii	$⊢ \forall p \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall q \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall r \in No ((p <_{s} r \land r <_{s} q) \to r \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}) \leftrightarrow \forall p \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall q \in No \forall r \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))))$
132		r19.21v	$⊢ \forall r \in No ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))))) \leftrightarrow ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to \forall r \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))))$
133	132	ralbii	$⊢ \forall q \in No \forall r \in No ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))))) \leftrightarrow \forall q \in No ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to \forall r \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))))$
134		r19.21v	$⊢ \forall q \in No ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to \forall r \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))))) \leftrightarrow ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to \forall q \in No \forall r \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))))$
135	133 134	bitri	$⊢ \forall q \in No \forall r \in No ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))))) \leftrightarrow ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to \forall q \in No \forall r \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))))$
136	135	ralbii	$⊢ \forall p \in No \forall q \in No \forall r \in No ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))))) \leftrightarrow \forall p \in No ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to \forall q \in No \forall r \in No ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))))$
137	114 131 136	3bitr4i	$⊢ \forall p \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall q \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall r \in No ((p <_{s} r \land r <_{s} q) \to r \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}) \leftrightarrow \forall p \in No \forall q \in No \forall r \in No ((A ≪_{s} \{p\} \land \{p\} ≪_{s} B) \to ((A ≪_{s} \{q\} \land \{q\} ≪_{s} B) \to ((p <_{s} r \land r <_{s} q) \to (r \in No \land (A ≪_{s} \{r\} \land \{r\} ≪_{s} B)))))$
138	109 137	sylibr	$⊢ A ≪_{s} B \to \forall p \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall q \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall r \in No ((p <_{s} r \land r <_{s} q) \to r \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\})$
139		nocvxmin	$⊢ (\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \neq \emptyset \land \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \subseteq No \land \forall p \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall q \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \forall r \in No ((p <_{s} r \land r <_{s} q) \to r \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\})) \to \exists! x \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} bday (x) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
140	45 47 138 139	syl3anc	$⊢ A ≪_{s} B \to \exists! x \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} bday (x) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$

Metamath Proof Explorer

Theorem conway

Proof