Metamath Proof Explorer

Theorem addscut2

Description: Show that the cut involved in surreal addition is legitimate. (Contributed by Scott Fenton, 8-Mar-2025)

		Ref	Expression
	Hypotheses	addscut.1	$⊢ φ \to X \in No$
		addscut.2	$⊢ φ \to Y \in No$
	Assertion	addscut2	$⊢ φ \to (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})$

Proof

Step	Hyp	Ref	Expression
1		addscut.1	$⊢ φ \to X \in No$
2		addscut.2	$⊢ φ \to Y \in No$
3	1 2	addscut	$⊢ φ \to (X +_{s} Y \in No \land (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{X +_{s} Y\} \land \{X +_{s} Y\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}))$
4		3anass	$⊢ (X +_{s} Y \in No \land (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{X +_{s} Y\} \land \{X +_{s} Y\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})) \leftrightarrow (X +_{s} Y \in No \land ((\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{X +_{s} Y\} \land \{X +_{s} Y\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})))$
5	3 4	sylib	$⊢ φ \to (X +_{s} Y \in No \land ((\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{X +_{s} Y\} \land \{X +_{s} Y\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})))$
6	5	simprd	$⊢ φ \to ((\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{X +_{s} Y\} \land \{X +_{s} Y\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}))$
7		ovex	$⊢ X +_{s} Y \in V$
8	7	snnz	$⊢ \{X +_{s} Y\} \neq \emptyset$
9		sslttr	$⊢ ((\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{X +_{s} Y\} \land \{X +_{s} Y\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}) \land \{X +_{s} Y\} \neq \emptyset) \to (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})$
10	8 9	mp3an3	$⊢ ((\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{X +_{s} Y\} \land \{X +_{s} Y\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})) \to (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})$
11	6 10	syl	$⊢ φ \to (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})$