Theorem mvtval

Description: The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mvtval.f	⊢ 𝑉 = ( mVT ‘ 𝑇 )
	mvtval.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
Assertion	mvtval	⊢ 𝑉 = ran 𝑌

Proof

Step	Hyp	Ref	Expression
1		mvtval.f	⊢ 𝑉 = ( mVT ‘ 𝑇 )
2		mvtval.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
3		fveq2	⊢ ( 𝑡 = 𝑇 → ( mType ‘ 𝑡 ) = ( mType ‘ 𝑇 ) )
4	3	rneqd	⊢ ( 𝑡 = 𝑇 → ran ( mType ‘ 𝑡 ) = ran ( mType ‘ 𝑇 ) )
5		df-mvt	⊢ mVT = ( 𝑡 ∈ V ↦ ran ( mType ‘ 𝑡 ) )
6		fvex	⊢ ( mType ‘ 𝑇 ) ∈ V
7	6	rnex	⊢ ran ( mType ‘ 𝑇 ) ∈ V
8	4 5 7	fvmpt	⊢ ( 𝑇 ∈ V → ( mVT ‘ 𝑇 ) = ran ( mType ‘ 𝑇 ) )
9		rn0	⊢ ran ∅ = ∅
10	9	eqcomi	⊢ ∅ = ran ∅
11		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mVT ‘ 𝑇 ) = ∅ )
12		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mType ‘ 𝑇 ) = ∅ )
13	12	rneqd	⊢ ( ¬ 𝑇 ∈ V → ran ( mType ‘ 𝑇 ) = ran ∅ )
14	10 11 13	3eqtr4a	⊢ ( ¬ 𝑇 ∈ V → ( mVT ‘ 𝑇 ) = ran ( mType ‘ 𝑇 ) )
15	8 14	pm2.61i	⊢ ( mVT ‘ 𝑇 ) = ran ( mType ‘ 𝑇 )
16	2	rneqi	⊢ ran 𝑌 = ran ( mType ‘ 𝑇 )
17	15 1 16	3eqtr4i	⊢ 𝑉 = ran 𝑌