2arwcatlem1

		Ref	Expression
	Hypothesis	2arwcatlem1.x	$⊢ X H X = \{\underset{˙}{0}, \underset{˙}{1}\}$
	Assertion	2arwcatlem1	$⊢ (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1}))) \leftrightarrow ((x \in \{X\} \land y \in \{X\}) \land (z \in \{X\} \land w \in \{X\}) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))$

Proof

Step	Hyp	Ref	Expression
1		2arwcatlem1.x	$⊢ X H X = \{\underset{˙}{0}, \underset{˙}{1}\}$
2		df-3an	$⊢ ((x \in \{X\} \land y \in \{X\}) \land (z \in \{X\} \land w \in \{X\}) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w))) \leftrightarrow (((x \in \{X\} \land y \in \{X\}) \land (z \in \{X\} \land w \in \{X\})) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))$
3		velsn	$⊢ x \in \{X\} \leftrightarrow x = X$
4		velsn	$⊢ y \in \{X\} \leftrightarrow y = X$
5	3 4	anbi12i	$⊢ (x \in \{X\} \land y \in \{X\}) \leftrightarrow (x = X \land y = X)$
6		velsn	$⊢ z \in \{X\} \leftrightarrow z = X$
7		velsn	$⊢ w \in \{X\} \leftrightarrow w = X$
8	6 7	anbi12i	$⊢ (z \in \{X\} \land w \in \{X\}) \leftrightarrow (z = X \land w = X)$
9	5 8	anbi12i	$⊢ ((x \in \{X\} \land y \in \{X\}) \land (z \in \{X\} \land w \in \{X\})) \leftrightarrow ((x = X \land y = X) \land (z = X \land w = X))$
10	9	anbi1i	$⊢ (((x \in \{X\} \land y \in \{X\}) \land (z \in \{X\} \land w \in \{X\})) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w))) \leftrightarrow (((x = X \land y = X) \land (z = X \land w = X)) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))$
11		simpll	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to x = X$
12		simplr	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to y = X$
13	11 12	oveq12d	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to x H y = X H X$
14	13 1	eqtrdi	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to x H y = \{\underset{˙}{0}, \underset{˙}{1}\}$
15	14	eleq2d	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to (f \in (x H y) \leftrightarrow f \in \{\underset{˙}{0}, \underset{˙}{1}\})$
16		simprl	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to z = X$
17	12 16	oveq12d	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to y H z = X H X$
18	17 1	eqtrdi	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to y H z = \{\underset{˙}{0}, \underset{˙}{1}\}$
19	18	eleq2d	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to (g \in (y H z) \leftrightarrow g \in \{\underset{˙}{0}, \underset{˙}{1}\})$
20		simprr	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to w = X$
21	16 20	oveq12d	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to z H w = X H X$
22	21 1	eqtrdi	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to z H w = \{\underset{˙}{0}, \underset{˙}{1}\}$
23	22	eleq2d	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to (k \in (z H w) \leftrightarrow k \in \{\underset{˙}{0}, \underset{˙}{1}\})$
24	15 19 23	3anbi123d	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to ((f \in (x H y) \land g \in (y H z) \land k \in (z H w)) \leftrightarrow (f \in \{\underset{˙}{0}, \underset{˙}{1}\} \land g \in \{\underset{˙}{0}, \underset{˙}{1}\} \land k \in \{\underset{˙}{0}, \underset{˙}{1}\}))$
25		vex	$⊢ f \in V$
26	25	elpr	$⊢ f \in \{\underset{˙}{0}, \underset{˙}{1}\} \leftrightarrow (f = \underset{˙}{0} \lor f = \underset{˙}{1})$
27		vex	$⊢ g \in V$
28	27	elpr	$⊢ g \in \{\underset{˙}{0}, \underset{˙}{1}\} \leftrightarrow (g = \underset{˙}{0} \lor g = \underset{˙}{1})$
29		vex	$⊢ k \in V$
30	29	elpr	$⊢ k \in \{\underset{˙}{0}, \underset{˙}{1}\} \leftrightarrow (k = \underset{˙}{0} \lor k = \underset{˙}{1})$
31	26 28 30	3anbi123i	$⊢ (f \in \{\underset{˙}{0}, \underset{˙}{1}\} \land g \in \{\underset{˙}{0}, \underset{˙}{1}\} \land k \in \{\underset{˙}{0}, \underset{˙}{1}\}) \leftrightarrow ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1}))$
32	24 31	bitrdi	$⊢ ((x = X \land y = X) \land (z = X \land w = X)) \to ((f \in (x H y) \land g \in (y H z) \land k \in (z H w)) \leftrightarrow ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))$
33	32	pm5.32i	$⊢ (((x = X \land y = X) \land (z = X \land w = X)) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w))) \leftrightarrow (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))$
34	2 10 33	3bitrri	$⊢ (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1}))) \leftrightarrow ((x \in \{X\} \land y \in \{X\}) \land (z \in \{X\} \land w \in \{X\}) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))$

Metamath Proof Explorer

Theorem 2arwcatlem1

Proof