cutbdaybnd

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

		Ref	Expression
	Assertion	cutbdaybnd	$⊢ (A ≪_{s} B \land O \in On \land bday [A \cup B] \subseteq O) \to bday (A \|_{s} B) \subseteq O$

Proof

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

Metamath Proof Explorer

Theorem cutbdaybnd

Proof