Theorem elnmz

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

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

Proof

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