negsproplem4

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis when A is simpler than B . (Contributed by Scott Fenton, 2-Feb-2025)

	Ref	Expression
Hypotheses	negsproplem.1	$⊢ φ \to \forall x \in No \forall y \in No (bday (x) \cup bday (y) \in (bday (A) \cup bday (B)) \to (+_{s} (x) \in No \land (x <_{s} y \to +_{s} (y) <_{s} +_{s} (x))))$
	negsproplem4.1	$⊢ φ \to A \in No$
	negsproplem4.2	$⊢ φ \to B \in No$
	negsproplem4.3	$⊢ φ \to A <_{s} B$
	negsproplem4.4	$⊢ φ \to bday (A) \in bday (B)$
Assertion	negsproplem4	$⊢ φ \to +_{s} (B) <_{s} +_{s} (A)$

Proof

Step	Hyp	Ref	Expression
1		negsproplem.1	$⊢ φ \to \forall x \in No \forall y \in No (bday (x) \cup bday (y) \in (bday (A) \cup bday (B)) \to (+_{s} (x) \in No \land (x <_{s} y \to +_{s} (y) <_{s} +_{s} (x))))$
2		negsproplem4.1	$⊢ φ \to A \in No$
3		negsproplem4.2	$⊢ φ \to B \in No$
4		negsproplem4.3	$⊢ φ \to A <_{s} B$
5		negsproplem4.4	$⊢ φ \to bday (A) \in bday (B)$
6		uncom	$⊢ bday (A) \cup bday (B) = bday (B) \cup bday (A)$
7	6	eleq2i	$⊢ bday (x) \cup bday (y) \in (bday (A) \cup bday (B)) \leftrightarrow bday (x) \cup bday (y) \in (bday (B) \cup bday (A))$
8	7	imbi1i	$⊢ (bday (x) \cup bday (y) \in (bday (A) \cup bday (B)) \to (+_{s} (x) \in No \land (x <_{s} y \to +_{s} (y) <_{s} +_{s} (x)))) \leftrightarrow (bday (x) \cup bday (y) \in (bday (B) \cup bday (A)) \to (+_{s} (x) \in No \land (x <_{s} y \to +_{s} (y) <_{s} +_{s} (x))))$
9	8	2ralbii	$⊢ \forall x \in No \forall y \in No (bday (x) \cup bday (y) \in (bday (A) \cup bday (B)) \to (+_{s} (x) \in No \land (x <_{s} y \to +_{s} (y) <_{s} +_{s} (x)))) \leftrightarrow \forall x \in No \forall y \in No (bday (x) \cup bday (y) \in (bday (B) \cup bday (A)) \to (+_{s} (x) \in No \land (x <_{s} y \to +_{s} (y) <_{s} +_{s} (x))))$
10	1 9	sylib	$⊢ φ \to \forall x \in No \forall y \in No (bday (x) \cup bday (y) \in (bday (B) \cup bday (A)) \to (+_{s} (x) \in No \land (x <_{s} y \to +_{s} (y) <_{s} +_{s} (x))))$
11	10 3	negsproplem3	$⊢ φ \to (+_{s} (B) \in No \land +_{s} [R (B)] ≪_{s} \{+_{s} (B)\} \land \{+_{s} (B)\} ≪_{s} +_{s} [L (B)])$
12	11	simp3d	$⊢ φ \to \{+_{s} (B)\} ≪_{s} +_{s} [L (B)]$
13		fvex	$⊢ +_{s} (B) \in V$
14	13	snid	$⊢ +_{s} (B) \in \{+_{s} (B)\}$
15	14	a1i	$⊢ φ \to +_{s} (B) \in \{+_{s} (B)\}$
16		negsfn	$⊢ +_{s} Fn No$
17		leftssno	$⊢ L (B) \subseteq No$
18		bdayelon	$⊢ bday (B) \in On$
19		oldbday	$⊢ (bday (B) \in On \land A \in No) \to (A \in Old (bday (B)) \leftrightarrow bday (A) \in bday (B))$
20	18 2 19	sylancr	$⊢ φ \to (A \in Old (bday (B)) \leftrightarrow bday (A) \in bday (B))$
21	5 20	mpbird	$⊢ φ \to A \in Old (bday (B))$
22		breq1	$⊢ a = A \to (a <_{s} B \leftrightarrow A <_{s} B)$
23		leftval	$⊢ L (B) = \{a \in Old (bday (B)) \| a <_{s} B\}$
24	22 23	elrab2	$⊢ A \in L (B) \leftrightarrow (A \in Old (bday (B)) \land A <_{s} B)$
25	21 4 24	sylanbrc	$⊢ φ \to A \in L (B)$
26		fnfvima	$⊢ (+_{s} Fn No \land L (B) \subseteq No \land A \in L (B)) \to +_{s} (A) \in +_{s} [L (B)]$
27	16 17 25 26	mp3an12i	$⊢ φ \to +_{s} (A) \in +_{s} [L (B)]$
28	12 15 27	ssltsepcd	$⊢ φ \to +_{s} (B) <_{s} +_{s} (A)$

Metamath Proof Explorer

Theorem negsproplem4

Proof