nodenselem8

Description: Lemma for nodense . Give a condition for surreal less-than when two surreals have the same birthday. (Contributed by Scott Fenton, 19-Jun-2011)

		Ref	Expression
	Assertion	nodenselem8	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A <_{s} B \leftrightarrow (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}))$

Proof

Step	Hyp	Ref	Expression
1		nodenselem5	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)$
2	1	exp32	$⊢ (A \in No \land B \in No) \to (bday (A) = bday (B) \to (A <_{s} B \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)))$
3	2	3impia	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A <_{s} B \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A))$
4		ltsval2	$⊢ (A \in No \land B \in No) \to (A <_{s} B \leftrightarrow A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
5	4	3adant3	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A <_{s} B \leftrightarrow A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
6		fvex	$⊢ A (⋂ \{a \in On \| A (a) \neq B (a)\}) \in V$
7		fvex	$⊢ B (⋂ \{a \in On \| A (a) \neq B (a)\}) \in V$
8	6 7	brtp	$⊢ A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}) \leftrightarrow ((A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}))$
9		eleq2	$⊢ bday (A) = bday (B) \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A) \leftrightarrow ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (B))$
10	9	biimpd	$⊢ bday (A) = bday (B) \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (B))$
11		nosgnn0	$⊢ \neg \emptyset \in \{1_{𝑜}, 2_{𝑜}\}$
12		nofnbday	$⊢ B \in No \to B Fn bday (B)$
13		fnfvelrn	$⊢ (B Fn bday (B) \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (B)) \to B (⋂ \{a \in On \| A (a) \neq B (a)\}) \in ran B$
14		eleq1	$⊢ B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \to (B (⋂ \{a \in On \| A (a) \neq B (a)\}) \in ran B \leftrightarrow \emptyset \in ran B)$
15	13 14	syl5ibcom	$⊢ (B Fn bday (B) \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (B)) \to (B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \to \emptyset \in ran B)$
16	12 15	sylan	$⊢ (B \in No \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (B)) \to (B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \to \emptyset \in ran B)$
17		norn	$⊢ B \in No \to ran B \subseteq \{1_{𝑜}, 2_{𝑜}\}$
18	17	sseld	$⊢ B \in No \to (\emptyset \in ran B \to \emptyset \in \{1_{𝑜}, 2_{𝑜}\})$
19	18	adantr	$⊢ (B \in No \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (B)) \to (\emptyset \in ran B \to \emptyset \in \{1_{𝑜}, 2_{𝑜}\})$
20	16 19	syld	$⊢ (B \in No \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (B)) \to (B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \to \emptyset \in \{1_{𝑜}, 2_{𝑜}\})$
21	11 20	mtoi	$⊢ (B \in No \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (B)) \to \neg B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset$
22	21	ex	$⊢ B \in No \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (B) \to \neg B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset)$
23	22	adantl	$⊢ (A \in No \land B \in No) \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (B) \to \neg B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset)$
24	10 23	syl9r	$⊢ (A \in No \land B \in No) \to (bday (A) = bday (B) \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A) \to \neg B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset))$
25	24	3impia	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A) \to \neg B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset)$
26	25	imp	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)) \to \neg B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset$
27	26	intnand	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)) \to \neg (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset)$
28		nofnbday	$⊢ A \in No \to A Fn bday (A)$
29		fnfvelrn	$⊢ (A Fn bday (A) \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)) \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) \in ran A$
30		eleq1	$⊢ A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) \in ran A \leftrightarrow \emptyset \in ran A)$
31	29 30	syl5ibcom	$⊢ (A Fn bday (A) \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \to \emptyset \in ran A)$
32	28 31	sylan	$⊢ (A \in No \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \to \emptyset \in ran A)$
33		norn	$⊢ A \in No \to ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}$
34	33	sseld	$⊢ A \in No \to (\emptyset \in ran A \to \emptyset \in \{1_{𝑜}, 2_{𝑜}\})$
35	34	adantr	$⊢ (A \in No \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)) \to (\emptyset \in ran A \to \emptyset \in \{1_{𝑜}, 2_{𝑜}\})$
36	32 35	syld	$⊢ (A \in No \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \to \emptyset \in \{1_{𝑜}, 2_{𝑜}\})$
37	11 36	mtoi	$⊢ (A \in No \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)) \to \neg A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset$
38	37	3ad2antl1	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)) \to \neg A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset$
39	38	intnanrd	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)) \to \neg (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})$
40		3orel13	$⊢ (\neg (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset) \land \neg (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})) \to (((A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}))$
41	27 39 40	syl2anc	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)) \to (((A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}))$
42	41	ex	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A) \to (((A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})))$
43	42	com23	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (((A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})) \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})))$
44	8 43	biimtrid	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}) \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})))$
45	5 44	sylbid	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A <_{s} B \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})))$
46	3 45	mpdd	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A <_{s} B \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}))$
47		3mix2	$⊢ (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \to ((A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}))$
48	47 8	sylibr	$⊢ (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})$
49	48 5	imbitrrid	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to ((A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \to A <_{s} B)$
50	46 49	impbid	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A <_{s} B \leftrightarrow (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}))$

Metamath Proof Explorer

Theorem nodenselem8

Proof