Theorem mexval2

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

	Ref	Expression
Hypotheses	mexval.k	⊢ 𝐾 = ( mTC ‘ 𝑇 )
	mexval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
	mexval2.c	⊢ 𝐶 = ( mCN ‘ 𝑇 )
	mexval2.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
Assertion	mexval2	⊢ 𝐸 = ( 𝐾 × Word ( 𝐶 ∪ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		mexval.k	⊢ 𝐾 = ( mTC ‘ 𝑇 )
2		mexval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
3		mexval2.c	⊢ 𝐶 = ( mCN ‘ 𝑇 )
4		mexval2.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
5		eqid	⊢ ( mREx ‘ 𝑇 ) = ( mREx ‘ 𝑇 )
6	1 2 5	mexval	⊢ 𝐸 = ( 𝐾 × ( mREx ‘ 𝑇 ) )
7	3 4 5	mrexval	⊢ ( 𝑇 ∈ V → ( mREx ‘ 𝑇 ) = Word ( 𝐶 ∪ 𝑉 ) )
8	7	xpeq2d	⊢ ( 𝑇 ∈ V → ( 𝐾 × ( mREx ‘ 𝑇 ) ) = ( 𝐾 × Word ( 𝐶 ∪ 𝑉 ) ) )
9	6 8	syl5eq	⊢ ( 𝑇 ∈ V → 𝐸 = ( 𝐾 × Word ( 𝐶 ∪ 𝑉 ) ) )
10		0xp	⊢ ( ∅ × Word ( 𝐶 ∪ 𝑉 ) ) = ∅
11	10	eqcomi	⊢ ∅ = ( ∅ × Word ( 𝐶 ∪ 𝑉 ) )
12		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mEx ‘ 𝑇 ) = ∅ )
13	2 12	syl5eq	⊢ ( ¬ 𝑇 ∈ V → 𝐸 = ∅ )
14		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mTC ‘ 𝑇 ) = ∅ )
15	1 14	syl5eq	⊢ ( ¬ 𝑇 ∈ V → 𝐾 = ∅ )
16	15	xpeq1d	⊢ ( ¬ 𝑇 ∈ V → ( 𝐾 × Word ( 𝐶 ∪ 𝑉 ) ) = ( ∅ × Word ( 𝐶 ∪ 𝑉 ) ) )
17	11 13 16	3eqtr4a	⊢ ( ¬ 𝑇 ∈ V → 𝐸 = ( 𝐾 × Word ( 𝐶 ∪ 𝑉 ) ) )
18	9 17	pm2.61i	⊢ 𝐸 = ( 𝐾 × Word ( 𝐶 ∪ 𝑉 ) )