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	$⊢ S = mSubst (T)$
	msubvrs.e	$⊢ E = mEx (T)$
	msubvrs.v	$⊢ V = mVars (T)$
	msubvrs.h	$⊢ H = mVH (T)$
Assertion	msubvrs	$⊢ (T \in mFS \land F \in ran S \land X \in E) \to V (F (X)) = ⋃_{x \in V (X)} V (F (H (x)))$

Proof

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

Metamath Proof Explorer

Theorem msubvrs

Proof