nosepdmlem

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

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		df-3or	$⊢ ((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_{𝑜})) \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_{𝑜}))$
6		ndmfv	$⊢ \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset$
7		1oex	$⊢ 1_{𝑜} \in V$
8	7	prid1	$⊢ 1_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
9	8	nosgnn0i	$⊢ \emptyset \neq 1_{𝑜}$
10		neeq1	$⊢ A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \to (A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq 1_{𝑜} \leftrightarrow \emptyset \neq 1_{𝑜})$
11	9 10	mpbiri	$⊢ A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq 1_{𝑜}$
12	11	neneqd	$⊢ A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \to \neg A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜}$
13	12	intnanrd	$⊢ A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \to \neg (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset)$
14	12	intnanrd	$⊢ A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \to \neg (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜})$
15		ioran	$⊢ \neg ((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_{𝑜})) \leftrightarrow (\neg (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset) \land \neg (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = 1_{𝑜} \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
16	13 14 15	sylanbrc	$⊢ A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \to \neg ((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_{𝑜}))$
17	6 16	syl	$⊢ \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A \to \neg ((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_{𝑜}))$
18	17	adantl	$⊢ ((A \in No \land B \in No) \land \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A) \to \neg ((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_{𝑜}))$
19		orel1	$⊢ \neg ((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_{𝑜})) \to ((((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)\}) = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
20	18 19	syl	$⊢ ((A \in No \land B \in No) \land \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A) \to ((((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)\}) = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
21	5 20	syl5bi	$⊢ ((A \in No \land B \in No) \land \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A) \to (((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)\}) = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}))$
22		ndmfv	$⊢ \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B \to B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset$
23		2on	$⊢ 2_{𝑜} \in On$
24	23	elexi	$⊢ 2_{𝑜} \in V$
25	24	prid2	$⊢ 2_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
26	25	nosgnn0i	$⊢ \emptyset \neq 2_{𝑜}$
27		neeq1	$⊢ B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \to (B (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq 2_{𝑜} \leftrightarrow \emptyset \neq 2_{𝑜})$
28	26 27	mpbiri	$⊢ B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \to B (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq 2_{𝑜}$
29	22 28	syl	$⊢ \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B \to B (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq 2_{𝑜}$
30	29	neneqd	$⊢ \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B \to \neg B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}$
31	30	con4i	$⊢ B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜} \to ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B$
32	31	adantl	$⊢ (A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset \land B (⋂ \{x \in On \| A (x) \neq B (x)\}) = 2_{𝑜}) \to ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B$
33	21 32	syl6	$⊢ ((A \in No \land B \in No) \land \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A) \to (((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 ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B)$
34	33	ex	$⊢ (A \in No \land B \in No) \to (\neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A \to (((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 ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B))$
35	34	com23	$⊢ (A \in No \land B \in No) \to (((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 (\neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A \to ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B))$
36	4 35	syl5bi	$⊢ (A \in No \land B \in No) \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)\}) \to (\neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A \to ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B))$
37	1 36	sylbid	$⊢ (A \in No \land B \in No) \to (A <_{s} B \to (\neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A \to ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B))$
38	37	3impia	$⊢ (A \in No \land B \in No \land A <_{s} B) \to (\neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A \to ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B)$
39	38	orrd	$⊢ (A \in No \land B \in No \land A <_{s} B) \to (⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A \lor ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B)$
40		elun	$⊢ ⋂ \{x \in On \| A (x) \neq B (x)\} \in (dom A \cup dom B) \leftrightarrow (⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A \lor ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B)$
41	39 40	sylibr	$⊢ (A \in No \land B \in No \land A <_{s} B) \to ⋂ \{x \in On \| A (x) \neq B (x)\} \in (dom A \cup dom B)$

Metamath Proof Explorer

Theorem nosepdmlem

Proof