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		sltsss1	$⊢ A ≪_{s} B \to A \subseteq No$
2		sltsex1	$⊢ A ≪_{s} B \to A \in V$
3		sltsss2	$⊢ A ≪_{s} B \to B \subseteq No$
4		sltsex2	$⊢ A ≪_{s} B \to B \in V$
5		sltssep	$⊢ 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		brslts	$⊢ 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		brslts	$⊢ \{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	48	snssd	$⊢ ((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$
54	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$
55		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$
56	55	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$
57	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$
58		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\}$
59	58	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\}$
60		sltssep	$⊢ A ≪_{s} \{p\} \to \forall x \in A \forall y \in \{p\} x <_{s} y$
61	59 60	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$
62	61	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$
63		vex	$⊢ p \in V$
64		breq2	$⊢ y = p \to (x <_{s} y \leftrightarrow x <_{s} p)$
65	63 64	ralsn	$⊢ \forall y \in \{p\} x <_{s} y \leftrightarrow x <_{s} p$
66	62 65	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$
67		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$
68	67	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$
69	54 56 57 66 68	ltstrd	$⊢ (((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$
70		vex	$⊢ r \in V$
71		breq2	$⊢ y = r \to (x <_{s} y \leftrightarrow x <_{s} r)$
72	70 71	ralsn	$⊢ \forall y \in \{r\} x <_{s} y \leftrightarrow x <_{s} r$
73	69 72	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$
74	73	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$
75	52 53 74	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)$
76		brslts	$⊢ 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))$
77	51 75 76	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\}$
78	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$
79	78 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)$
80	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$
81	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$
82		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$
83	82	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$
84	80	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$
85		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$
86	85	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$
87		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$
88	87	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$
89		sltssep	$⊢ \{q\} ≪_{s} B \to \forall x \in \{q\} \forall y \in B x <_{s} y$
90	88 89	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$
91		vex	$⊢ q \in V$
92		breq1	$⊢ x = q \to (x <_{s} y \leftrightarrow q <_{s} y)$
93	92	ralbidv	$⊢ x = q \to (\forall y \in B x <_{s} y \leftrightarrow \forall y \in B q <_{s} y)$
94	91 93	ralsn	$⊢ \forall x \in \{q\} \forall y \in B x <_{s} y \leftrightarrow \forall y \in B q <_{s} y$
95	90 94	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$
96	95	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$
97	81 83 84 86 96	ltstrd	$⊢ (((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$
98	97	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$
99		breq1	$⊢ x = r \to (x <_{s} y \leftrightarrow r <_{s} y)$
100	99	ralbidv	$⊢ x = r \to (\forall y \in B x <_{s} y \leftrightarrow \forall y \in B r <_{s} y)$
101	70 100	ralsn	$⊢ \forall x \in \{r\} \forall y \in B x <_{s} y \leftrightarrow \forall y \in B r <_{s} y$
102	98 101	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$
103	53 80 102	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)$
104		brslts	$⊢ \{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))$
105	79 103 104	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$
106	48 77 105	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))$
107	106	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)))))$
108	107	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)))))$
109		sneq	$⊢ y = p \to \{y\} = \{p\}$
110	109	breq2d	$⊢ y = p \to (A ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{p\})$
111	109	breq1d	$⊢ y = p \to (\{y\} ≪_{s} B \leftrightarrow \{p\} ≪_{s} B)$
112	110 111	anbi12d	$⊢ y = p \to ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{p\} \land \{p\} ≪_{s} B))$
113	112	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)))))$
114		sneq	$⊢ y = q \to \{y\} = \{q\}$
115	114	breq2d	$⊢ y = q \to (A ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{q\})$
116	114	breq1d	$⊢ y = q \to (\{y\} ≪_{s} B \leftrightarrow \{q\} ≪_{s} B)$
117	115 116	anbi12d	$⊢ y = q \to ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{q\} \land \{q\} ≪_{s} B))$
118	117	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))))$
119		sneq	$⊢ y = r \to \{y\} = \{r\}$
120	119	breq2d	$⊢ y = r \to (A ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{r\})$
121	119	breq1d	$⊢ y = r \to (\{y\} ≪_{s} B \leftrightarrow \{r\} ≪_{s} B)$
122	120 121	anbi12d	$⊢ y = r \to ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))$
123	122	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))$
124	123	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)))$
125	124	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)))$
126	125	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)))$
127		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))))$
128	127	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))))$
129	118 126 128	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))))$
130	129	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))))$
131		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)))))$
132	131	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)))))$
133		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)))))$
134	132 133	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)))))$
135	134	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)))))$
136	113 130 135	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)))))$
137	108 136	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)\})$
138		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)\}]$
139	45 47 137 138	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