nosep2o

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

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

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (A \in No \land B \in No \land A \neq B) \to B \in No$
2		simp1	$⊢ (A \in No \land B \in No \land A \neq B) \to A \in No$
3		simp3	$⊢ (A \in No \land B \in No \land A \neq B) \to A \neq B$
4	3	necomd	$⊢ (A \in No \land B \in No \land A \neq B) \to B \neq A$
5		nosepne	$⊢ (B \in No \land A \in No \land B \neq A) \to B (⋂ \{x \in On \| B (x) \neq A (x)\}) \neq A (⋂ \{x \in On \| B (x) \neq A (x)\})$
6	1 2 4 5	syl3anc	$⊢ (A \in No \land B \in No \land A \neq B) \to B (⋂ \{x \in On \| B (x) \neq A (x)\}) \neq A (⋂ \{x \in On \| B (x) \neq A (x)\})$
7	6	adantr	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to B (⋂ \{x \in On \| B (x) \neq A (x)\}) \neq A (⋂ \{x \in On \| B (x) \neq A (x)\})$
8		simpr	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}$
9	7 8	neeqtrd	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to B (⋂ \{x \in On \| B (x) \neq A (x)\}) \neq 2_{𝑜}$
10	9	neneqd	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to \neg B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}$
11		simpl2	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to B \in No$
12		nofv	$⊢ B \in No \to (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \lor B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \lor B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜})$
13	11 12	syl	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \lor B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \lor B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜})$
14		3orel3	$⊢ \neg B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜} \to ((B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \lor B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \lor B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \lor B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜}))$
15	10 13 14	sylc	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \lor B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜})$
16	15	orcomd	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \lor B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset)$
17	16 8	jca	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to ((B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \lor B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜})$
18		andir	$⊢ ((B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \lor B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \leftrightarrow ((B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \lor (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}))$
19	17 18	sylib	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to ((B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \lor (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}))$
20		3mix2	$⊢ (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to ((B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset) \lor (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \lor (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}))$
21		3mix3	$⊢ (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to ((B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset) \lor (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \lor (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}))$
22	20 21	jaoi	$⊢ ((B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \lor (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜})) \to ((B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset) \lor (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \lor (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}))$
23	19 22	syl	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to ((B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset) \lor (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \lor (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}))$
24		fvex	$⊢ B (⋂ \{x \in On \| B (x) \neq A (x)\}) \in V$
25		fvex	$⊢ A (⋂ \{x \in On \| B (x) \neq A (x)\}) \in V$
26	24 25	brtp	$⊢ B (⋂ \{x \in On \| B (x) \neq A (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} A (⋂ \{x \in On \| B (x) \neq A (x)\}) \leftrightarrow ((B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset) \lor (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = 1_{𝑜} \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \lor (B (⋂ \{x \in On \| B (x) \neq A (x)\}) = \emptyset \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}))$
27	23 26	sylibr	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to B (⋂ \{x \in On \| B (x) \neq A (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} A (⋂ \{x \in On \| B (x) \neq A (x)\})$
28		simpl1	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to A \in No$
29		ltsval2	$⊢ (B \in No \land A \in No) \to (B <_{s} A \leftrightarrow B (⋂ \{x \in On \| B (x) \neq A (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} A (⋂ \{x \in On \| B (x) \neq A (x)\}))$
30	11 28 29	syl2anc	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to (B <_{s} A \leftrightarrow B (⋂ \{x \in On \| B (x) \neq A (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} A (⋂ \{x \in On \| B (x) \neq A (x)\}))$
31	27 30	mpbird	$⊢ ((A \in No \land B \in No \land A \neq B) \land A (⋂ \{x \in On \| B (x) \neq A (x)\}) = 2_{𝑜}) \to B <_{s} A$

Metamath Proof Explorer

Theorem nosep2o

Proof