fin2solem

		Ref	Expression
	Assertion	fin2solem	$⊢ (R Or x \land (y \in x \land z \in x)) \to (y R z \to \{w \in x \| w R y\} [\subset] \{w \in x \| w R z\})$

Proof

Step	Hyp	Ref	Expression
1		ancom	$⊢ ((y \in x \land z \in x) \land w \in x) \leftrightarrow (w \in x \land (y \in x \land z \in x))$
2		3anass	$⊢ (w \in x \land y \in x \land z \in x) \leftrightarrow (w \in x \land (y \in x \land z \in x))$
3	1 2	bitr4i	$⊢ ((y \in x \land z \in x) \land w \in x) \leftrightarrow (w \in x \land y \in x \land z \in x)$
4		sotr	$⊢ (R Or x \land (w \in x \land y \in x \land z \in x)) \to ((w R y \land y R z) \to w R z)$
5	3 4	sylan2b	$⊢ (R Or x \land ((y \in x \land z \in x) \land w \in x)) \to ((w R y \land y R z) \to w R z)$
6	5	anassrs	$⊢ ((R Or x \land (y \in x \land z \in x)) \land w \in x) \to ((w R y \land y R z) \to w R z)$
7	6	ancomsd	$⊢ ((R Or x \land (y \in x \land z \in x)) \land w \in x) \to ((y R z \land w R y) \to w R z)$
8	7	expdimp	$⊢ (((R Or x \land (y \in x \land z \in x)) \land w \in x) \land y R z) \to (w R y \to w R z)$
9	8	an32s	$⊢ (((R Or x \land (y \in x \land z \in x)) \land y R z) \land w \in x) \to (w R y \to w R z)$
10	9	ss2rabdv	$⊢ ((R Or x \land (y \in x \land z \in x)) \land y R z) \to \{w \in x \| w R y\} \subseteq \{w \in x \| w R z\}$
11		breq1	$⊢ w = y \to (w R z \leftrightarrow y R z)$
12	11	elrab	$⊢ y \in \{w \in x \| w R z\} \leftrightarrow (y \in x \land y R z)$
13	12	biimpri	$⊢ (y \in x \land y R z) \to y \in \{w \in x \| w R z\}$
14	13	adantll	$⊢ ((R Or x \land y \in x) \land y R z) \to y \in \{w \in x \| w R z\}$
15		sonr	$⊢ (R Or x \land y \in x) \to \neg y R y$
16		breq1	$⊢ w = y \to (w R y \leftrightarrow y R y)$
17	16	elrab	$⊢ y \in \{w \in x \| w R y\} \leftrightarrow (y \in x \land y R y)$
18	17	simprbi	$⊢ y \in \{w \in x \| w R y\} \to y R y$
19	15 18	nsyl	$⊢ (R Or x \land y \in x) \to \neg y \in \{w \in x \| w R y\}$
20	19	adantr	$⊢ ((R Or x \land y \in x) \land y R z) \to \neg y \in \{w \in x \| w R y\}$
21		nelne1	$⊢ (y \in \{w \in x \| w R z\} \land \neg y \in \{w \in x \| w R y\}) \to \{w \in x \| w R z\} \neq \{w \in x \| w R y\}$
22	21	necomd	$⊢ (y \in \{w \in x \| w R z\} \land \neg y \in \{w \in x \| w R y\}) \to \{w \in x \| w R y\} \neq \{w \in x \| w R z\}$
23	14 20 22	syl2anc	$⊢ ((R Or x \land y \in x) \land y R z) \to \{w \in x \| w R y\} \neq \{w \in x \| w R z\}$
24	23	adantlrr	$⊢ ((R Or x \land (y \in x \land z \in x)) \land y R z) \to \{w \in x \| w R y\} \neq \{w \in x \| w R z\}$
25		vex	$⊢ x \in V$
26	25	rabex	$⊢ \{w \in x \| w R z\} \in V$
27	26	brrpss	$⊢ \{w \in x \| w R y\} [\subset] \{w \in x \| w R z\} \leftrightarrow \{w \in x \| w R y\} \subset \{w \in x \| w R z\}$
28		df-pss	$⊢ \{w \in x \| w R y\} \subset \{w \in x \| w R z\} \leftrightarrow (\{w \in x \| w R y\} \subseteq \{w \in x \| w R z\} \land \{w \in x \| w R y\} \neq \{w \in x \| w R z\})$
29	27 28	bitri	$⊢ \{w \in x \| w R y\} [\subset] \{w \in x \| w R z\} \leftrightarrow (\{w \in x \| w R y\} \subseteq \{w \in x \| w R z\} \land \{w \in x \| w R y\} \neq \{w \in x \| w R z\})$
30	10 24 29	sylanbrc	$⊢ ((R Or x \land (y \in x \land z \in x)) \land y R z) \to \{w \in x \| w R y\} [\subset] \{w \in x \| w R z\}$
31	30	ex	$⊢ (R Or x \land (y \in x \land z \in x)) \to (y R z \to \{w \in x \| w R y\} [\subset] \{w \in x \| w R z\})$

Metamath Proof Explorer

Theorem fin2solem

Proof