nosep1o

Description: If the value of a surreal at a separator is 1o then the surreal is lesser. (Contributed by Scott Fenton, 7-Dec-2021)

		Ref	Expression
	Assertion	nosep1o	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to A <_{s} B$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}$
2		nosepne	$⊢ (A \in No \land B \in No \land A \neq B) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq B (⋂ \{x \in On \| A (x) \neq B (x)\})$
3	2	adantr	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq B (⋂ \{x \in On \| A (x) \neq B (x)\})$
4	1 3	eqnetrrd	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to 1_{𝑜} \neq B (⋂ \{x \in On \| A (x) \neq B (x)\})$
5	4	necomd	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to B (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq 1_{𝑜}$
6	5	neneqd	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to \neg B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}$
7		simpl2	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to B \in No$
8		nofv	$⊢ B \in No \to (B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \lor B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \lor B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜})$
9	7 8	syl	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to (B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \lor B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \lor B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜})$
10		3orel2	$⊢ \neg B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \to ((B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \lor B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \lor B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \to (B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \lor B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
11	6 9 10	sylc	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to (B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \lor B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜})$
12		eqid	$⊢ 1_{𝑜} = 1_{𝑜}$
13	11 12	jctil	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to (1_{𝑜} = 1_{𝑜} \land (B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \lor B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
14		andi	$⊢ (1_{𝑜} = 1_{𝑜} \land (B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \lor B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜})) \leftrightarrow ((1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \lor (1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
15	13 14	sylib	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to ((1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \lor (1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
16		3mix1	$⊢ (1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \to ((1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \lor (1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \lor (1_{𝑜} = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
17		3mix2	$⊢ (1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \to ((1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \lor (1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \lor (1_{𝑜} = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
18	16 17	jaoi	$⊢ ((1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \lor (1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜})) \to ((1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \lor (1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \lor (1_{𝑜} = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
19	15 18	syl	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to ((1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \lor (1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \lor (1_{𝑜} = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
20		1oex	$⊢ 1_{𝑜} \in V$
21		fvex	$⊢ B (⋂ \{x \in On \| A (x) \neq B (x)\}) \in V$
22	20 21	brtp	$⊢ 1_{𝑜} \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{x \in On \| A (x) \neq B (x)\}) \leftrightarrow ((1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \lor (1_{𝑜} = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \lor (1_{𝑜} = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
23	19 22	sylibr	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to 1_{𝑜} \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{x \in On \| A (x) \neq B (x)\})$
24	1 23	eqbrtrd	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{x \in On \| A (x) \neq B (x)\})$
25		simpl1	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to A \in No$
26		ltsval2	$⊢ (A \in No \land B \in No) \to (A <_{s} B \leftrightarrow A (⋂ \{x \in On \| A (x) \neq B (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{x \in On \| A (x) \neq B (x)\}))$
27	25 7 26	syl2anc	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to (A <_{s} B \leftrightarrow A (⋂ \{x \in On \| A (x) \neq B (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{x \in On \| A (x) \neq B (x)\}))$
28	24 27	mpbird	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}) \to A <_{s} B$

Metamath Proof Explorer

Theorem nosep1o

Proof