Theorem cntrval

Description: Substitute definition of the center. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	cntrval.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	cntrval.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion	cntrval	⊢ ( 𝑍 ‘ 𝐵 ) = ( Cntr ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		cntrval.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		cntrval.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
3		fveq2	⊢ ( 𝑚 = 𝑀 → ( Cntz ‘ 𝑚 ) = ( Cntz ‘ 𝑀 ) )
4	3 2	eqtr4di	⊢ ( 𝑚 = 𝑀 → ( Cntz ‘ 𝑚 ) = 𝑍 )
5		fveq2	⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
6	5 1	eqtr4di	⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = 𝐵 )
7	4 6	fveq12d	⊢ ( 𝑚 = 𝑀 → ( ( Cntz ‘ 𝑚 ) ‘ ( Base ‘ 𝑚 ) ) = ( 𝑍 ‘ 𝐵 ) )
8		df-cntr	⊢ Cntr = ( 𝑚 ∈ V ↦ ( ( Cntz ‘ 𝑚 ) ‘ ( Base ‘ 𝑚 ) ) )
9		fvex	⊢ ( 𝑍 ‘ 𝐵 ) ∈ V
10	7 8 9	fvmpt	⊢ ( 𝑀 ∈ V → ( Cntr ‘ 𝑀 ) = ( 𝑍 ‘ 𝐵 ) )
11	10	eqcomd	⊢ ( 𝑀 ∈ V → ( 𝑍 ‘ 𝐵 ) = ( Cntr ‘ 𝑀 ) )
12		0fv	⊢ ( ∅ ‘ 𝐵 ) = ∅
13		fvprc	⊢ ( ¬ 𝑀 ∈ V → ( Cntz ‘ 𝑀 ) = ∅ )
14	2 13	syl5eq	⊢ ( ¬ 𝑀 ∈ V → 𝑍 = ∅ )
15	14	fveq1d	⊢ ( ¬ 𝑀 ∈ V → ( 𝑍 ‘ 𝐵 ) = ( ∅ ‘ 𝐵 ) )
16		fvprc	⊢ ( ¬ 𝑀 ∈ V → ( Cntr ‘ 𝑀 ) = ∅ )
17	12 15 16	3eqtr4a	⊢ ( ¬ 𝑀 ∈ V → ( 𝑍 ‘ 𝐵 ) = ( Cntr ‘ 𝑀 ) )
18	11 17	pm2.61i	⊢ ( 𝑍 ‘ 𝐵 ) = ( Cntr ‘ 𝑀 )