cutbdaylt

Description: If a surreal lies in a gap and is not equal to the cut, its birthday is greater than the cut's. (Contributed by Scott Fenton, 11-Dec-2021)

		Ref	Expression
	Assertion	cutbdaylt	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to bday (A \|_{s} B) \in bday (X)$

Proof

Step	Hyp	Ref	Expression
1		simp2l	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to A ≪_{s} \{X\}$
2		simp2r	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to \{X\} ≪_{s} B$
3		snnzg	$⊢ X \in No \to \{X\} \neq \emptyset$
4	3	3ad2ant1	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to \{X\} \neq \emptyset$
5		sltstr	$⊢ (A ≪_{s} \{X\} \land \{X\} ≪_{s} B \land \{X\} \neq \emptyset) \to A ≪_{s} B$
6	1 2 4 5	syl3anc	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to A ≪_{s} B$
7		cutbday	$⊢ A ≪_{s} B \to bday (A \|_{s} B) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
8	6 7	syl	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to bday (A \|_{s} B) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
9		bdayfn	$⊢ bday Fn No$
10		ssrab2	$⊢ \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \subseteq No$
11		simp1	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to X \in No$
12		simp2	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)$
13		sneq	$⊢ y = X \to \{y\} = \{X\}$
14	13	breq2d	$⊢ y = X \to (A ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{X\})$
15	13	breq1d	$⊢ y = X \to (\{y\} ≪_{s} B \leftrightarrow \{X\} ≪_{s} B)$
16	14 15	anbi12d	$⊢ y = X \to ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{X\} \land \{X\} ≪_{s} B))$
17	16	elrab	$⊢ X \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \leftrightarrow (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B))$
18	11 12 17	sylanbrc	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to X \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}$
19		fnfvima	$⊢ (bday Fn No \land \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \subseteq No \land X \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}) \to bday (X) \in bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
20	9 10 18 19	mp3an12i	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to bday (X) \in bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
21		intss1	$⊢ bday (X) \in bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}] \to ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}] \subseteq bday (X)$
22	20 21	syl	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}] \subseteq bday (X)$
23	8 22	eqsstrd	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to bday (A \|_{s} B) \subseteq bday (X)$
24		simprl	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \to A ≪_{s} \{X\}$
25		simprr	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \to \{X\} ≪_{s} B$
26	3	adantr	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \to \{X\} \neq \emptyset$
27	24 25 26 5	syl3anc	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \to A ≪_{s} B$
28	27 7	syl	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \to bday (A \|_{s} B) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
29	28	eqeq1d	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \to (bday (A \|_{s} B) = bday (X) \leftrightarrow ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}] = bday (X))$
30		eqcom	$⊢ ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}] = bday (X) \leftrightarrow bday (X) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
31	29 30	bitrdi	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \to (bday (A \|_{s} B) = bday (X) \leftrightarrow bday (X) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}])$
32	31	biimpa	$⊢ ((X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \land bday (A \|_{s} B) = bday (X)) \to bday (X) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
33	17	biimpri	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \to X \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}$
34	27	adantr	$⊢ ((X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \land bday (A \|_{s} B) = bday (X)) \to A ≪_{s} B$
35		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)\}]$
36	34 35	syl	$⊢ ((X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \land bday (A \|_{s} B) = bday (X)) \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)\}]$
37		fveqeq2	$⊢ x = X \to (bday (x) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}] \leftrightarrow bday (X) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}])$
38	37	riota2	$⊢ (X \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \land \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)\}]) \to (bday (X) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}] \leftrightarrow (ι 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)\}]) = X)$
39		eqcom	$⊢ (ι 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)\}]) = X \leftrightarrow X = (ι 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)\}])$
40	38 39	bitrdi	$⊢ (X \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \land \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)\}]) \to (bday (X) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}] \leftrightarrow X = (ι 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)\}]))$
41	33 36 40	syl2an2r	$⊢ ((X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \land bday (A \|_{s} B) = bday (X)) \to (bday (X) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}] \leftrightarrow X = (ι 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)\}]))$
42	32 41	mpbid	$⊢ ((X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \land bday (A \|_{s} B) = bday (X)) \to X = (ι 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)\}])$
43		cutsval	$⊢ A ≪_{s} B \to A \|_{s} B = (ι 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)\}])$
44	34 43	syl	$⊢ ((X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \land bday (A \|_{s} B) = bday (X)) \to A \|_{s} B = (ι 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)\}])$
45	42 44	eqtr4d	$⊢ ((X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \land bday (A \|_{s} B) = bday (X)) \to X = A \|_{s} B$
46	45	ex	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \to (bday (A \|_{s} B) = bday (X) \to X = A \|_{s} B)$
47	46	necon3d	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B)) \to (X \neq A \|_{s} B \to bday (A \|_{s} B) \neq bday (X))$
48	47	3impia	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to bday (A \|_{s} B) \neq bday (X)$
49		bdayon	$⊢ bday (A \|_{s} B) \in On$
50		bdayon	$⊢ bday (X) \in On$
51		onelpss	$⊢ (bday (A \|_{s} B) \in On \land bday (X) \in On) \to (bday (A \|_{s} B) \in bday (X) \leftrightarrow (bday (A \|_{s} B) \subseteq bday (X) \land bday (A \|_{s} B) \neq bday (X)))$
52	49 50 51	mp2an	$⊢ bday (A \|_{s} B) \in bday (X) \leftrightarrow (bday (A \|_{s} B) \subseteq bday (X) \land bday (A \|_{s} B) \neq bday (X))$
53	23 48 52	sylanbrc	$⊢ (X \in No \land (A ≪_{s} \{X\} \land \{X\} ≪_{s} B) \land X \neq A \|_{s} B) \to bday (A \|_{s} B) \in bday (X)$

Metamath Proof Explorer

Theorem cutbdaylt

Proof