cutbdaybnd2

Description: An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021)

		Ref	Expression
	Assertion	cutbdaybnd2	$⊢ A ≪_{s} B \to bday (A \|_{s} B) \subseteq suc ⋃ bday [A \cup B]$

Proof

Step	Hyp	Ref	Expression
1		etaslts2	$⊢ A ≪_{s} B \to \exists x \in No (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B])$
2		cutbday	$⊢ A ≪_{s} B \to bday (A \|_{s} B) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
3	2	adantr	$⊢ (A ≪_{s} B \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B]))) \to bday (A \|_{s} B) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
4		bdayfn	$⊢ bday Fn No$
5		ssrab2	$⊢ \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \subseteq No$
6		simprl	$⊢ (A ≪_{s} B \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B]))) \to x \in No$
7		simprr1	$⊢ (A ≪_{s} B \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B]))) \to A ≪_{s} \{x\}$
8		simprr2	$⊢ (A ≪_{s} B \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B]))) \to \{x\} ≪_{s} B$
9	7 8	jca	$⊢ (A ≪_{s} B \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B]))) \to (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)$
10		sneq	$⊢ y = x \to \{y\} = \{x\}$
11	10	breq2d	$⊢ y = x \to (A ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{x\})$
12	10	breq1d	$⊢ y = x \to (\{y\} ≪_{s} B \leftrightarrow \{x\} ≪_{s} B)$
13	11 12	anbi12d	$⊢ y = x \to ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{x\} \land \{x\} ≪_{s} B))$
14	13	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))$
15	6 9 14	sylanbrc	$⊢ (A ≪_{s} B \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B]))) \to x \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}$
16		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)\}]$
17	4 5 15 16	mp3an12i	$⊢ (A ≪_{s} B \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B]))) \to bday (x) \in bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
18		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)$
19	17 18	syl	$⊢ (A ≪_{s} B \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B]))) \to ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}] \subseteq bday (x)$
20	3 19	eqsstrd	$⊢ (A ≪_{s} B \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B]))) \to bday (A \|_{s} B) \subseteq bday (x)$
21		simprr3	$⊢ (A ≪_{s} B \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B]))) \to bday (x) \subseteq suc ⋃ bday [A \cup B]$
22	20 21	sstrd	$⊢ (A ≪_{s} B \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B]))) \to bday (A \|_{s} B) \subseteq suc ⋃ bday [A \cup B]$
23	22	rexlimdvaa	$⊢ A ≪_{s} B \to (\exists x \in No (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B]) \to bday (A \|_{s} B) \subseteq suc ⋃ bday [A \cup B])$
24	1 23	mpd	$⊢ A ≪_{s} B \to bday (A \|_{s} B) \subseteq suc ⋃ bday [A \cup B]$

Metamath Proof Explorer

Theorem cutbdaybnd2

Proof