nosepnelem

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

Proof

Step	Hyp	Ref	Expression
1		sltval2	$⊢ (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)\}))$
2		fvex	$⊢ A (⋂ \{x \in On \| A (x) \neq B (x)\}) \in V$
3		fvex	$⊢ B (⋂ \{x \in On \| A (x) \neq B (x)\}) \in V$
4	2 3	brtp	$⊢ A (⋂ \{x \in On \| A (x) \neq B (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{x \in On \| A (x) \neq B (x)\}) \leftrightarrow ((A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \lor (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \lor (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
5		1n0	$⊢ 1_{𝑜} \neq \emptyset$
6		simpl	$⊢ (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}$
7		simpr	$⊢ (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \to B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset$
8	6 7	neeq12d	$⊢ (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \to (A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq B (⋂ \{x \in On \| A (x) \neq B (x)\}) \leftrightarrow 1_{𝑜} \neq \emptyset)$
9	5 8	mpbiri	$⊢ (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq B (⋂ \{x \in On \| A (x) \neq B (x)\})$
10		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
11		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
12	10 11	eqeq12i	$⊢ 2_{𝑜} = 1_{𝑜} \leftrightarrow suc 1_{𝑜} = suc \emptyset$
13		1on	$⊢ 1_{𝑜} \in On$
14		0elon	$⊢ \emptyset \in On$
15		suc11	$⊢ (1_{𝑜} \in On \land \emptyset \in On) \to (suc 1_{𝑜} = suc \emptyset \leftrightarrow 1_{𝑜} = \emptyset)$
16	13 14 15	mp2an	$⊢ suc 1_{𝑜} = suc \emptyset \leftrightarrow 1_{𝑜} = \emptyset$
17	12 16	bitri	$⊢ 2_{𝑜} = 1_{𝑜} \leftrightarrow 1_{𝑜} = \emptyset$
18	17	necon3bii	$⊢ 2_{𝑜} \neq 1_{𝑜} \leftrightarrow 1_{𝑜} \neq \emptyset$
19	5 18	mpbir	$⊢ 2_{𝑜} \neq 1_{𝑜}$
20	19	necomi	$⊢ 1_{𝑜} \neq 2_{𝑜}$
21		simpl	$⊢ (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}$
22		simpr	$⊢ (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \to B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}$
23	21 22	neeq12d	$⊢ (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \to (A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq B (⋂ \{x \in On \| A (x) \neq B (x)\}) \leftrightarrow 1_{𝑜} \neq 2_{𝑜})$
24	20 23	mpbiri	$⊢ (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq B (⋂ \{x \in On \| A (x) \neq B (x)\})$
25		2on	$⊢ 2_{𝑜} \in On$
26	25	elexi	$⊢ 2_{𝑜} \in V$
27	26	prid2	$⊢ 2_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
28	27	nosgnn0i	$⊢ \emptyset \neq 2_{𝑜}$
29		simpl	$⊢ (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset$
30		simpr	$⊢ (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \to B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}$
31	29 30	neeq12d	$⊢ (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \to (A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq B (⋂ \{x \in On \| A (x) \neq B (x)\}) \leftrightarrow \emptyset \neq 2_{𝑜})$
32	28 31	mpbiri	$⊢ (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq B (⋂ \{x \in On \| A (x) \neq B (x)\})$
33	9 24 32	3jaoi	$⊢ ((A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \lor (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \lor (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜})) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq B (⋂ \{x \in On \| A (x) \neq B (x)\})$
34	4 33	sylbi	$⊢ A (⋂ \{x \in On \| A (x) \neq B (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{x \in On \| A (x) \neq B (x)\}) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq B (⋂ \{x \in On \| A (x) \neq B (x)\})$
35	1 34	syl6bi	$⊢ (A \in No \land B \in No) \to (A <_{s} B \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq B (⋂ \{x \in On \| A (x) \neq B (x)\}))$
36	35	3impia	$⊢ (A \in No \land B \in No \land A <_{s} B) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq B (⋂ \{x \in On \| A (x) \neq B (x)\})$

Metamath Proof Explorer

Theorem nosepnelem

Proof