msubvrs

Description: The set of variables in a substitution is the union, indexed by the variables in the original expression, of the variables in the substitution to that variable. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msubvrs.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
	msubvrs.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
	msubvrs.v	⊢ 𝑉 = ( mVars ‘ 𝑇 )
	msubvrs.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
Assertion	msubvrs	⊢ ( ( 𝑇 ∈ mFS ∧ 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝐸 ) → ( 𝑉 ‘ ( 𝐹 ‘ 𝑋 ) ) = ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		msubvrs.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
2		msubvrs.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
3		msubvrs.v	⊢ 𝑉 = ( mVars ‘ 𝑇 )
4		msubvrs.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
5		eqid	⊢ ( mRSubst ‘ 𝑇 ) = ( mRSubst ‘ 𝑇 )
6	2 5 1	elmsubrn	⊢ ran 𝑆 = ran ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )
7	6	eleq2i	⊢ ( 𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ran ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
8		eqid	⊢ ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) = ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )
9	2	fvexi	⊢ 𝐸 ∈ V
10	9	mptex	⊢ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ∈ V
11	8 10	elrnmpti	⊢ ( 𝐹 ∈ ran ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) ↔ ∃ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) 𝐹 = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )
12	7 11	bitri	⊢ ( 𝐹 ∈ ran 𝑆 ↔ ∃ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) 𝐹 = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )
13		simp2	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) )
14		simp3	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → 𝑋 ∈ 𝐸 )
15		eqid	⊢ ( mTC ‘ 𝑇 ) = ( mTC ‘ 𝑇 )
16		eqid	⊢ ( mREx ‘ 𝑇 ) = ( mREx ‘ 𝑇 )
17	15 2 16	mexval	⊢ 𝐸 = ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) )
18	14 17	eleqtrdi	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → 𝑋 ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) )
19		xp2nd	⊢ ( 𝑋 ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) → ( 2^nd ‘ 𝑋 ) ∈ ( mREx ‘ 𝑇 ) )
20	18 19	syl	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( 2^nd ‘ 𝑋 ) ∈ ( mREx ‘ 𝑇 ) )
21		eqid	⊢ ( mVR ‘ 𝑇 ) = ( mVR ‘ 𝑇 )
22	5 21 16	mrsubvrs	⊢ ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ( mREx ‘ 𝑇 ) ) → ( ran ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ∩ ( mVR ‘ 𝑇 ) ) = ∪ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ( ran ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ∩ ( mVR ‘ 𝑇 ) ) )
23	13 20 22	syl2anc	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( ran ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ∩ ( mVR ‘ 𝑇 ) ) = ∪ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ( ran ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ∩ ( mVR ‘ 𝑇 ) ) )
24		fveq2	⊢ ( 𝑒 = 𝑋 → ( 1^st ‘ 𝑒 ) = ( 1^st ‘ 𝑋 ) )
25		2fveq3	⊢ ( 𝑒 = 𝑋 → ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) = ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) )
26	24 25	opeq12d	⊢ ( 𝑒 = 𝑋 → ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ = ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ )
27		eqid	⊢ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ )
28		opex	⊢ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ∈ V
29	26 27 28	fvmpt3i	⊢ ( 𝑋 ∈ 𝐸 → ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ 𝑋 ) = ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ )
30	14 29	syl	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ 𝑋 ) = ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ )
31	30	fveq2d	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ 𝑋 ) ) = ( 𝑉 ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ) )
32		xp1st	⊢ ( 𝑋 ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) → ( 1^st ‘ 𝑋 ) ∈ ( mTC ‘ 𝑇 ) )
33	18 32	syl	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( 1^st ‘ 𝑋 ) ∈ ( mTC ‘ 𝑇 ) )
34	5 16	mrsubf	⊢ ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) → 𝑓 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) )
35	13 34	syl	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → 𝑓 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) )
36	19 17	eleq2s	⊢ ( 𝑋 ∈ 𝐸 → ( 2^nd ‘ 𝑋 ) ∈ ( mREx ‘ 𝑇 ) )
37	14 36	syl	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( 2^nd ‘ 𝑋 ) ∈ ( mREx ‘ 𝑇 ) )
38	35 37	ffvelcdmd	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ( mREx ‘ 𝑇 ) )
39		opelxpi	⊢ ( ( ( 1^st ‘ 𝑋 ) ∈ ( mTC ‘ 𝑇 ) ∧ ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ( mREx ‘ 𝑇 ) ) → ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) )
40	33 38 39	syl2anc	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) )
41	40 17	eleqtrrdi	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ∈ 𝐸 )
42	21 2 3	mvrsval	⊢ ( ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ∈ 𝐸 → ( 𝑉 ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ) = ( ran ( 2^nd ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ) ∩ ( mVR ‘ 𝑇 ) ) )
43	41 42	syl	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( 𝑉 ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ) = ( ran ( 2^nd ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ) ∩ ( mVR ‘ 𝑇 ) ) )
44		fvex	⊢ ( 1^st ‘ 𝑋 ) ∈ V
45		fvex	⊢ ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ∈ V
46	44 45	op2nd	⊢ ( 2^nd ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ) = ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) )
47	46	a1i	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( 2^nd ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ) = ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) )
48	47	rneqd	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ran ( 2^nd ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ) = ran ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) )
49	48	ineq1d	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( ran ( 2^nd ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ) ∩ ( mVR ‘ 𝑇 ) ) = ( ran ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ∩ ( mVR ‘ 𝑇 ) ) )
50	31 43 49	3eqtrd	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ 𝑋 ) ) = ( ran ( 𝑓 ‘ ( 2^nd ‘ 𝑋 ) ) ∩ ( mVR ‘ 𝑇 ) ) )
51	21 2 3	mvrsval	⊢ ( 𝑋 ∈ 𝐸 → ( 𝑉 ‘ 𝑋 ) = ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) )
52	14 51	syl	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( 𝑉 ‘ 𝑋 ) = ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) )
53	52	iuneq1d	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) = ∪ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
54	21 2 4	mvhf	⊢ ( 𝑇 ∈ mFS → 𝐻 : ( mVR ‘ 𝑇 ) ⟶ 𝐸 )
55	54	3ad2ant1	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → 𝐻 : ( mVR ‘ 𝑇 ) ⟶ 𝐸 )
56		inss2	⊢ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ⊆ ( mVR ‘ 𝑇 )
57	56	sseli	⊢ ( 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) → 𝑥 ∈ ( mVR ‘ 𝑇 ) )
58		ffvelcdm	⊢ ( ( 𝐻 : ( mVR ‘ 𝑇 ) ⟶ 𝐸 ∧ 𝑥 ∈ ( mVR ‘ 𝑇 ) ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐸 )
59	55 57 58	syl2an	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐸 )
60		fveq2	⊢ ( 𝑒 = ( 𝐻 ‘ 𝑥 ) → ( 1^st ‘ 𝑒 ) = ( 1^st ‘ ( 𝐻 ‘ 𝑥 ) ) )
61		2fveq3	⊢ ( 𝑒 = ( 𝐻 ‘ 𝑥 ) → ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) = ( 𝑓 ‘ ( 2^nd ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
62	60 61	opeq12d	⊢ ( 𝑒 = ( 𝐻 ‘ 𝑥 ) → ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ = ⟨ ( 1^st ‘ ( 𝐻 ‘ 𝑥 ) ) , ( 𝑓 ‘ ( 2^nd ‘ ( 𝐻 ‘ 𝑥 ) ) ) ⟩ )
63	62 27 28	fvmpt3i	⊢ ( ( 𝐻 ‘ 𝑥 ) ∈ 𝐸 → ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) = ⟨ ( 1^st ‘ ( 𝐻 ‘ 𝑥 ) ) , ( 𝑓 ‘ ( 2^nd ‘ ( 𝐻 ‘ 𝑥 ) ) ) ⟩ )
64	59 63	syl	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) = ⟨ ( 1^st ‘ ( 𝐻 ‘ 𝑥 ) ) , ( 𝑓 ‘ ( 2^nd ‘ ( 𝐻 ‘ 𝑥 ) ) ) ⟩ )
65	57	adantl	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → 𝑥 ∈ ( mVR ‘ 𝑇 ) )
66		eqid	⊢ ( mType ‘ 𝑇 ) = ( mType ‘ 𝑇 )
67	21 66 4	mvhval	⊢ ( 𝑥 ∈ ( mVR ‘ 𝑇 ) → ( 𝐻 ‘ 𝑥 ) = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ⟩ )
68	65 67	syl	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( 𝐻 ‘ 𝑥 ) = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ⟩ )
69		fvex	⊢ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) ∈ V
70		s1cli	⊢ ⟨“ 𝑥 ”⟩ ∈ Word V
71	70	elexi	⊢ ⟨“ 𝑥 ”⟩ ∈ V
72	69 71	op1std	⊢ ( ( 𝐻 ‘ 𝑥 ) = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ⟩ → ( 1^st ‘ ( 𝐻 ‘ 𝑥 ) ) = ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) )
73	68 72	syl	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( 1^st ‘ ( 𝐻 ‘ 𝑥 ) ) = ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) )
74	69 71	op2ndd	⊢ ( ( 𝐻 ‘ 𝑥 ) = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ⟩ → ( 2^nd ‘ ( 𝐻 ‘ 𝑥 ) ) = ⟨“ 𝑥 ”⟩ )
75	68 74	syl	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( 2^nd ‘ ( 𝐻 ‘ 𝑥 ) ) = ⟨“ 𝑥 ”⟩ )
76	75	fveq2d	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( 𝑓 ‘ ( 2^nd ‘ ( 𝐻 ‘ 𝑥 ) ) ) = ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) )
77	73 76	opeq12d	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ⟨ ( 1^st ‘ ( 𝐻 ‘ 𝑥 ) ) , ( 𝑓 ‘ ( 2^nd ‘ ( 𝐻 ‘ 𝑥 ) ) ) ⟩ = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ )
78	64 77	eqtrd	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ )
79	78	fveq2d	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) = ( 𝑉 ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ ) )
80		simpl1	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → 𝑇 ∈ mFS )
81	21 15 66	mtyf2	⊢ ( 𝑇 ∈ mFS → ( mType ‘ 𝑇 ) : ( mVR ‘ 𝑇 ) ⟶ ( mTC ‘ 𝑇 ) )
82	80 81	syl	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( mType ‘ 𝑇 ) : ( mVR ‘ 𝑇 ) ⟶ ( mTC ‘ 𝑇 ) )
83	82 65	ffvelcdmd	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( mTC ‘ 𝑇 ) )
84	35	adantr	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → 𝑓 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) )
85		elun2	⊢ ( 𝑥 ∈ ( mVR ‘ 𝑇 ) → 𝑥 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
86	65 85	syl	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → 𝑥 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
87	86	s1cld	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ⟨“ 𝑥 ”⟩ ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
88		eqid	⊢ ( mCN ‘ 𝑇 ) = ( mCN ‘ 𝑇 )
89	88 21 16	mrexval	⊢ ( 𝑇 ∈ mFS → ( mREx ‘ 𝑇 ) = Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
90	80 89	syl	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( mREx ‘ 𝑇 ) = Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
91	87 90	eleqtrrd	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ⟨“ 𝑥 ”⟩ ∈ ( mREx ‘ 𝑇 ) )
92	84 91	ffvelcdmd	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ∈ ( mREx ‘ 𝑇 ) )
93		opelxpi	⊢ ( ( ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( mTC ‘ 𝑇 ) ∧ ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ∈ ( mREx ‘ 𝑇 ) ) → ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) )
94	83 92 93	syl2anc	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) )
95	94 17	eleqtrrdi	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ ∈ 𝐸 )
96	21 2 3	mvrsval	⊢ ( ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ ∈ 𝐸 → ( 𝑉 ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ ) = ( ran ( 2^nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ ) ∩ ( mVR ‘ 𝑇 ) ) )
97	95 96	syl	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( 𝑉 ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ ) = ( ran ( 2^nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ ) ∩ ( mVR ‘ 𝑇 ) ) )
98		fvex	⊢ ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ∈ V
99	69 98	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ ) = ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ )
100	99	a1i	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( 2^nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ ) = ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) )
101	100	rneqd	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ran ( 2^nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ ) = ran ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) )
102	101	ineq1d	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( ran ( 2^nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑥 ) , ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ⟩ ) ∩ ( mVR ‘ 𝑇 ) ) = ( ran ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ∩ ( mVR ‘ 𝑇 ) ) )
103	79 97 102	3eqtrd	⊢ ( ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ) → ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) = ( ran ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ∩ ( mVR ‘ 𝑇 ) ) )
104	103	iuneq2dv	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ∪ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) = ∪ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ( ran ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ∩ ( mVR ‘ 𝑇 ) ) )
105	53 104	eqtrd	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) = ∪ 𝑥 ∈ ( ran ( 2^nd ‘ 𝑋 ) ∩ ( mVR ‘ 𝑇 ) ) ( ran ( 𝑓 ‘ ⟨“ 𝑥 ”⟩ ) ∩ ( mVR ‘ 𝑇 ) ) )
106	23 50 105	3eqtr4d	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ 𝑋 ) ) = ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
107		fveq1	⊢ ( 𝐹 = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) → ( 𝐹 ‘ 𝑋 ) = ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ 𝑋 ) )
108	107	fveq2d	⊢ ( 𝐹 = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) → ( 𝑉 ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ 𝑋 ) ) )
109		fveq1	⊢ ( 𝐹 = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) → ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) = ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) )
110	109	fveq2d	⊢ ( 𝐹 = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) → ( 𝑉 ‘ ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) ) = ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
111	110	iuneq2d	⊢ ( 𝐹 = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) → ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) ) = ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
112	108 111	eqeq12d	⊢ ( 𝐹 = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) → ( ( 𝑉 ‘ ( 𝐹 ‘ 𝑋 ) ) = ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ↔ ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ 𝑋 ) ) = ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) )
113	106 112	syl5ibrcom	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑋 ∈ 𝐸 ) → ( 𝐹 = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) → ( 𝑉 ‘ ( 𝐹 ‘ 𝑋 ) ) = ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) )
114	113	3expia	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ) → ( 𝑋 ∈ 𝐸 → ( 𝐹 = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) → ( 𝑉 ‘ ( 𝐹 ‘ 𝑋 ) ) = ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) ) )
115	114	com23	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ) → ( 𝐹 = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) → ( 𝑋 ∈ 𝐸 → ( 𝑉 ‘ ( 𝐹 ‘ 𝑋 ) ) = ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) ) )
116	115	rexlimdva	⊢ ( 𝑇 ∈ mFS → ( ∃ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) 𝐹 = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) → ( 𝑋 ∈ 𝐸 → ( 𝑉 ‘ ( 𝐹 ‘ 𝑋 ) ) = ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) ) )
117	12 116	biimtrid	⊢ ( 𝑇 ∈ mFS → ( 𝐹 ∈ ran 𝑆 → ( 𝑋 ∈ 𝐸 → ( 𝑉 ‘ ( 𝐹 ‘ 𝑋 ) ) = ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) ) )
118	117	3imp	⊢ ( ( 𝑇 ∈ mFS ∧ 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝐸 ) → ( 𝑉 ‘ ( 𝐹 ‘ 𝑋 ) ) = ∪ 𝑥 ∈ ( 𝑉 ‘ 𝑋 ) ( 𝑉 ‘ ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem msubvrs

Proof