Theorem mexval

Description: The set of expressions, which are pairs whose first element is a typecode, and whose second element is a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mexval.k	⊢ 𝐾 = ( mTC ‘ 𝑇 )
	mexval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
	mexval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
Assertion	mexval	⊢ 𝐸 = ( 𝐾 × 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		mexval.k	⊢ 𝐾 = ( mTC ‘ 𝑇 )
2		mexval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
3		mexval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
4		fveq2	⊢ ( 𝑡 = 𝑇 → ( mTC ‘ 𝑡 ) = ( mTC ‘ 𝑇 ) )
5	4 1	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mTC ‘ 𝑡 ) = 𝐾 )
6		fveq2	⊢ ( 𝑡 = 𝑇 → ( mREx ‘ 𝑡 ) = ( mREx ‘ 𝑇 ) )
7	6 3	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mREx ‘ 𝑡 ) = 𝑅 )
8	5 7	xpeq12d	⊢ ( 𝑡 = 𝑇 → ( ( mTC ‘ 𝑡 ) × ( mREx ‘ 𝑡 ) ) = ( 𝐾 × 𝑅 ) )
9		df-mex	⊢ mEx = ( 𝑡 ∈ V ↦ ( ( mTC ‘ 𝑡 ) × ( mREx ‘ 𝑡 ) ) )
10		fvex	⊢ ( mTC ‘ 𝑡 ) ∈ V
11		fvex	⊢ ( mREx ‘ 𝑡 ) ∈ V
12	10 11	xpex	⊢ ( ( mTC ‘ 𝑡 ) × ( mREx ‘ 𝑡 ) ) ∈ V
13	8 9 12	fvmpt3i	⊢ ( 𝑇 ∈ V → ( mEx ‘ 𝑇 ) = ( 𝐾 × 𝑅 ) )
14		xp0	⊢ ( 𝐾 × ∅ ) = ∅
15	14	eqcomi	⊢ ∅ = ( 𝐾 × ∅ )
16		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mEx ‘ 𝑇 ) = ∅ )
17		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mREx ‘ 𝑇 ) = ∅ )
18	3 17	syl5eq	⊢ ( ¬ 𝑇 ∈ V → 𝑅 = ∅ )
19	18	xpeq2d	⊢ ( ¬ 𝑇 ∈ V → ( 𝐾 × 𝑅 ) = ( 𝐾 × ∅ ) )
20	15 16 19	3eqtr4a	⊢ ( ¬ 𝑇 ∈ V → ( mEx ‘ 𝑇 ) = ( 𝐾 × 𝑅 ) )
21	13 20	pm2.61i	⊢ ( mEx ‘ 𝑇 ) = ( 𝐾 × 𝑅 )
22	2 21	eqtri	⊢ 𝐸 = ( 𝐾 × 𝑅 )