scutval

Description: The value of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021)

		Ref	Expression
	Assertion	scutval	$⊢ 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)\}])$

Proof

Step	Hyp	Ref	Expression
1		ssltex1	$⊢ A ≪_{s} B \to A \in V$
2		ssltss1	$⊢ A ≪_{s} B \to A \subseteq No$
3	1 2	elpwd	$⊢ A ≪_{s} B \to A \in 𝒫 No$
4		df-br	$⊢ A ≪_{s} B \leftrightarrow ⟨A, B⟩ \in ≪_{s}$
5	4	biimpi	$⊢ A ≪_{s} B \to ⟨A, B⟩ \in ≪_{s}$
6		ssltex2	$⊢ A ≪_{s} B \to B \in V$
7		elimasng	$⊢ (A \in V \land B \in V) \to (B \in ≪_{s} [\{A\}] \leftrightarrow ⟨A, B⟩ \in ≪_{s})$
8	1 6 7	syl2anc	$⊢ A ≪_{s} B \to (B \in ≪_{s} [\{A\}] \leftrightarrow ⟨A, B⟩ \in ≪_{s})$
9	5 8	mpbird	$⊢ A ≪_{s} B \to B \in ≪_{s} [\{A\}]$
10		riotaex	$⊢ (ι 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)\}]) \in V$
11		breq1	$⊢ a = A \to (a ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{y\})$
12		breq2	$⊢ b = B \to (\{y\} ≪_{s} b \leftrightarrow \{y\} ≪_{s} B)$
13	11 12	bi2anan9	$⊢ (a = A \land b = B) \to ((a ≪_{s} \{y\} \land \{y\} ≪_{s} b) \leftrightarrow (A ≪_{s} \{y\} \land \{y\} ≪_{s} B))$
14	13	rabbidv	$⊢ (a = A \land b = B) \to \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} = \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}$
15	14	imaeq2d	$⊢ (a = A \land b = B) \to bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}] = bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
16	15	inteqd	$⊢ (a = A \land b = B) \to ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}] = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
17	16	eqeq2d	$⊢ (a = A \land b = B) \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)\}])$
18	14 17	riotaeqbidv	$⊢ (a = A \land b = B) \to (ι 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 \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \| bday (x) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}])$
19		sneq	$⊢ a = A \to \{a\} = \{A\}$
20	19	imaeq2d	$⊢ a = A \to ≪_{s} [\{a\}] = ≪_{s} [\{A\}]$
21		df-scut	$⊢ \|_{s} = (a \in 𝒫 No, b \in ≪_{s} [\{a\}] ⟼ (ι 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)\}]))$
22	18 20 21	ovmpox	$⊢ (A \in 𝒫 No \land B \in ≪_{s} [\{A\}] \land (ι 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)\}]) \in V) \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)\}])$
23	10 22	mp3an3	$⊢ (A \in 𝒫 No \land B \in ≪_{s} [\{A\}]) \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)\}])$
24	3 9 23	syl2anc	$⊢ 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)\}])$

Metamath Proof Explorer

Theorem scutval

Proof