Theorem cntzssv

Description: The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	cntzrcl.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	cntzrcl.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion	cntzssv	⊢ ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵

Proof

Step	Hyp	Ref	Expression
1		cntzrcl.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		cntzrcl.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
3		0ss	⊢ ∅ ⊆ 𝐵
4		sseq1	⊢ ( ( 𝑍 ‘ 𝑆 ) = ∅ → ( ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 ↔ ∅ ⊆ 𝐵 ) )
5	3 4	mpbiri	⊢ ( ( 𝑍 ‘ 𝑆 ) = ∅ → ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 )
6		n0	⊢ ( ( 𝑍 ‘ 𝑆 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) )
7	1 2	cntzrcl	⊢ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵 ) )
8		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
9	1 8 2	cntzval	⊢ ( 𝑆 ⊆ 𝐵 → ( 𝑍 ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) } )
10	7 9	simpl2im	⊢ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝑍 ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) } )
11		ssrab2	⊢ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) } ⊆ 𝐵
12	10 11	eqsstrdi	⊢ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 )
13	12	exlimiv	⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 )
14	6 13	sylbi	⊢ ( ( 𝑍 ‘ 𝑆 ) ≠ ∅ → ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 )
15	5 14	pm2.61ine	⊢ ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵