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	bilanri	$⊢ ((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$
21	12 15 20	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)$
22		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))$
23	11 21 22	sylanbrc	$⊢ ((A ≪_{s} B \land y \in No) \land \forall p \in A p <_{s} y) \to A ≪_{s} \{y\}$
24	23	ex	$⊢ (A ≪_{s} B \land y \in No) \to (\forall p \in A p <_{s} y \to A ≪_{s} \{y\})$
25	4	ad2antrr	$⊢ ((A ≪_{s} B \land y \in No) \land \forall q \in B y <_{s} q) \to B \in V$
26	25 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)$
27	14	adantr	$⊢ ((A ≪_{s} B \land y \in No) \land \forall q \in B y <_{s} q) \to \{y\} \subseteq No$
28	3	ad2antrr	$⊢ ((A ≪_{s} B \land y \in No) \land \forall q \in B y <_{s} q) \to B \subseteq No$
29		ralcom	$⊢ \forall p \in \{y\} \forall q \in B p <_{s} q \leftrightarrow \forall q \in B \forall p \in \{y\} p <_{s} q$
30		breq1	$⊢ p = y \to (p <_{s} q \leftrightarrow y <_{s} q)$
31	16 30	ralsn	$⊢ \forall p \in \{y\} p <_{s} q \leftrightarrow y <_{s} q$
32	31	ralbii	$⊢ \forall q \in B \forall p \in \{y\} p <_{s} q \leftrightarrow \forall q \in B y <_{s} q$
33	29 32	sylbbr	$⊢ \forall q \in B y <_{s} q \to \forall p \in \{y\} \forall q \in B p <_{s} q$
34	33	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$
35	27 28 34	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)$
36		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))$
37	26 35 36	sylanbrc	$⊢ ((A ≪_{s} B \land y \in No) \land \forall q \in B y <_{s} q) \to \{y\} ≪_{s} B$
38	37	ex	$⊢ (A ≪_{s} B \land y \in No) \to (\forall q \in B y <_{s} q \to \{y\} ≪_{s} B)$
39	24 38	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))$
40	8 39	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))$
41	40	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))$
42	7 41	mpd	$⊢ A ≪_{s} B \to \exists y \in No (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)$
43		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)$
44	42 43	sylibr	$⊢ A ≪_{s} B \to \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \neq \emptyset$
45		ssrab2	$⊢ \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \subseteq No$
46	45	a1i	$⊢ A ≪_{s} B \to \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \subseteq No$
47		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$
48	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$
49		vsnex	$⊢ \{r\} \in V$
50	48 49	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)$
51	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$
52	47	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$
53	51	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$
54		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$
55	54	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$
56	47	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$
57		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\}$
58	57	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\}$
59		sltssep	$⊢ A ≪_{s} \{p\} \to \forall x \in A \forall y \in \{p\} x <_{s} y$
60	58 59	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$
61	60	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$
62		vex	$⊢ p \in V$
63		breq2	$⊢ y = p \to (x <_{s} y \leftrightarrow x <_{s} p)$
64	62 63	ralsn	$⊢ \forall y \in \{p\} x <_{s} y \leftrightarrow x <_{s} p$
65	61 64	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$
66		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$
67	66	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$
68	53 55 56 65 67	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$
69		vex	$⊢ r \in V$
70		breq2	$⊢ y = r \to (x <_{s} y \leftrightarrow x <_{s} r)$
71	69 70	ralsn	$⊢ \forall y \in \{r\} x <_{s} y \leftrightarrow x <_{s} r$
72	68 71	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$
73	72	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$
74	51 52 73	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)$
75		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))$
76	50 74 75	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\}$
77	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$
78	77 49	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)$
79	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$
80	47	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$
81		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$
82	81	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$
83	79	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$
84		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$
85	84	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$
86		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$
87	86	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$
88		sltssep	$⊢ \{q\} ≪_{s} B \to \forall x \in \{q\} \forall y \in B x <_{s} y$
89	87 88	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$
90		vex	$⊢ q \in V$
91		breq1	$⊢ x = q \to (x <_{s} y \leftrightarrow q <_{s} y)$
92	91	ralbidv	$⊢ x = q \to (\forall y \in B x <_{s} y \leftrightarrow \forall y \in B q <_{s} y)$
93	90 92	ralsn	$⊢ \forall x \in \{q\} \forall y \in B x <_{s} y \leftrightarrow \forall y \in B q <_{s} y$
94	89 93	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$
95	94	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$
96	80 82 83 85 95	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$
97	96	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$
98		breq1	$⊢ x = r \to (x <_{s} y \leftrightarrow r <_{s} y)$
99	98	ralbidv	$⊢ x = r \to (\forall y \in B x <_{s} y \leftrightarrow \forall y \in B r <_{s} y)$
100	69 99	ralsn	$⊢ \forall x \in \{r\} \forall y \in B x <_{s} y \leftrightarrow \forall y \in B r <_{s} y$
101	97 100	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$
102	52 79 101	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)$
103		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))$
104	78 102 103	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$
105	47 76 104	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))$
106	105	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)))))$
107	106	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)))))$
108		sneq	$⊢ y = p \to \{y\} = \{p\}$
109	108	breq2d	$⊢ y = p \to (A ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{p\})$
110	108	breq1d	$⊢ y = p \to (\{y\} ≪_{s} B \leftrightarrow \{p\} ≪_{s} B)$
111	109 110	anbi12d	$⊢ y = p \to ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{p\} \land \{p\} ≪_{s} B))$
112	111	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)))))$
113		sneq	$⊢ y = q \to \{y\} = \{q\}$
114	113	breq2d	$⊢ y = q \to (A ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{q\})$
115	113	breq1d	$⊢ y = q \to (\{y\} ≪_{s} B \leftrightarrow \{q\} ≪_{s} B)$
116	114 115	anbi12d	$⊢ y = q \to ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{q\} \land \{q\} ≪_{s} B))$
117	116	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))))$
118		sneq	$⊢ y = r \to \{y\} = \{r\}$
119	118	breq2d	$⊢ y = r \to (A ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{r\})$
120	118	breq1d	$⊢ y = r \to (\{y\} ≪_{s} B \leftrightarrow \{r\} ≪_{s} B)$
121	119 120	anbi12d	$⊢ y = r \to ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{r\} \land \{r\} ≪_{s} B))$
122	121	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))$
123	122	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)))$
124	123	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)))$
125	124	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)))$
126		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))))$
127	126	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))))$
128	117 125 127	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))))$
129	128	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))))$
130		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)))))$
131	130	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)))))$
132		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)))))$
133	131 132	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)))))$
134	133	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)))))$
135	112 129 134	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)))))$
136	107 135	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)\})$
137		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)\}]$
138	44 46 136 137	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