This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elnmz

Description: Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015)

		Ref	Expression
	Hypothesis	elnmz.1	$⊢ N = \{x \in X \| \forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S)\}$
	Assertion	elnmz	$⊢ A \in N \leftrightarrow (A \in X \land \forall z \in X (A \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} A \in S))$

Proof

Step	Hyp	Ref	Expression
1		elnmz.1	$⊢ N = \{x \in X \| \forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S)\}$
2		oveq2	$⊢ y = z \to x \underset{˙}{+} y = x \underset{˙}{+} z$
3	2	eleq1d	$⊢ y = z \to (x \underset{˙}{+} y \in S \leftrightarrow x \underset{˙}{+} z \in S)$
4		oveq1	$⊢ y = z \to y \underset{˙}{+} x = z \underset{˙}{+} x$
5	4	eleq1d	$⊢ y = z \to (y \underset{˙}{+} x \in S \leftrightarrow z \underset{˙}{+} x \in S)$
6	3 5	bibi12d	$⊢ y = z \to ((x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S) \leftrightarrow (x \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} x \in S))$
7	6	cbvralvw	$⊢ \forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S) \leftrightarrow \forall z \in X (x \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} x \in S)$
8		oveq1	$⊢ x = A \to x \underset{˙}{+} z = A \underset{˙}{+} z$
9	8	eleq1d	$⊢ x = A \to (x \underset{˙}{+} z \in S \leftrightarrow A \underset{˙}{+} z \in S)$
10		oveq2	$⊢ x = A \to z \underset{˙}{+} x = z \underset{˙}{+} A$
11	10	eleq1d	$⊢ x = A \to (z \underset{˙}{+} x \in S \leftrightarrow z \underset{˙}{+} A \in S)$
12	9 11	bibi12d	$⊢ x = A \to ((x \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} x \in S) \leftrightarrow (A \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} A \in S))$
13	12	ralbidv	$⊢ x = A \to (\forall z \in X (x \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} x \in S) \leftrightarrow \forall z \in X (A \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} A \in S))$
14	7 13	bitrid	$⊢ x = A \to (\forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S) \leftrightarrow \forall z \in X (A \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} A \in S))$
15	14 1	elrab2	$⊢ A \in N \leftrightarrow (A \in X \land \forall z \in X (A \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} A \in S))$