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 ⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
Assertion elnmz ( 𝐴 ∈ 𝑁 ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 elnmz.1 ⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
2 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 + 𝑦 ) = ( 𝑥 + 𝑧 ) )
3 2 eleq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑥 + 𝑧 ) ∈ 𝑆 ) )
4 oveq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 + 𝑥 ) = ( 𝑧 + 𝑥 ) )
5 4 eleq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 + 𝑥 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) )
6 3 5 bibi12d ⊢ ( 𝑦 = 𝑧 → ( ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ↔ ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ) )
7 6 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) )
8 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 + 𝑧 ) = ( 𝐴 + 𝑧 ) )
9 8 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝐴 + 𝑧 ) ∈ 𝑆 ) )
10 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑧 + 𝑥 ) = ( 𝑧 + 𝐴 ) )
11 10 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑧 + 𝑥 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) )
12 9 11 bibi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) ) )
13 12 ralbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) ) )
14 7 13 bitrid ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) ) )
15 14 1 elrab2 ⊢ ( 𝐴 ∈ 𝑁 ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) ) )