cntrval

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

Step	Hyp	Ref	Expression
1		cntrval.b	$⊢ B = {Base}_{M}$
2		cntrval.z	$⊢ Z = Cntz (M)$
3		fveq2	$⊢ m = M \to Cntz (m) = Cntz (M)$
4	3 2	eqtr4di	$⊢ m = M \to Cntz (m) = Z$
5		fveq2	$⊢ m = M \to {Base}_{m} = {Base}_{M}$
6	5 1	eqtr4di	$⊢ m = M \to {Base}_{m} = B$
7	4 6	fveq12d	$⊢ m = M \to Cntz (m) ({Base}_{m}) = Z (B)$
8		df-cntr	$⊢ Cntr = (m \in V ⟼ Cntz (m) ({Base}_{m}))$
9		fvex	$⊢ Z (B) \in V$
10	7 8 9	fvmpt	$⊢ M \in V \to Cntr (M) = Z (B)$
11	10	eqcomd	$⊢ M \in V \to Z (B) = Cntr (M)$
12		0fv	$⊢ \emptyset (B) = \emptyset$
13		fvprc	$⊢ \neg M \in V \to Cntz (M) = \emptyset$
14	2 13	eqtrid	$⊢ \neg M \in V \to Z = \emptyset$
15	14	fveq1d	$⊢ \neg M \in V \to Z (B) = \emptyset (B)$
16		fvprc	$⊢ \neg M \in V \to Cntr (M) = \emptyset$
17	12 15 16	3eqtr4a	$⊢ \neg M \in V \to Z (B) = Cntr (M)$
18	11 17	pm2.61i	$⊢ Z (B) = Cntr (M)$

Metamath Proof Explorer