mrsubvrs

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	mrsubco.s	$⊢ S = mRSubst (T)$
	mrsubvrs.v	$⊢ V = mVR (T)$
	mrsubvrs.r	$⊢ R = mREx (T)$
Assertion	mrsubvrs	$⊢ (F \in ran S \land X \in R) \to ran F (X) \cap V = ⋃_{x \in ran X \cap V} (ran F (⟨“ x ”⟩) \cap V)$

Proof

Step	Hyp	Ref	Expression
1		mrsubco.s	$⊢ S = mRSubst (T)$
2		mrsubvrs.v	$⊢ V = mVR (T)$
3		mrsubvrs.r	$⊢ R = mREx (T)$
4		n0i	$⊢ F \in ran S \to \neg ran S = \emptyset$
5	1	rnfvprc	$⊢ \neg T \in V \to ran S = \emptyset$
6	4 5	nsyl2	$⊢ F \in ran S \to T \in V$
7		eqid	$⊢ mCN (T) = mCN (T)$
8	7 2 3	mrexval	$⊢ T \in V \to R = Word (mCN (T) \cup V)$
9	6 8	syl	$⊢ F \in ran S \to R = Word (mCN (T) \cup V)$
10	9	eleq2d	$⊢ F \in ran S \to (X \in R \leftrightarrow X \in Word (mCN (T) \cup V))$
11		fveq2	$⊢ v = \emptyset \to F (v) = F (\emptyset)$
12	11	rneqd	$⊢ v = \emptyset \to ran F (v) = ran F (\emptyset)$
13	12	ineq1d	$⊢ v = \emptyset \to ran F (v) \cap V = ran F (\emptyset) \cap V$
14		rneq	$⊢ v = \emptyset \to ran v = ran \emptyset$
15		rn0	$⊢ ran \emptyset = \emptyset$
16	14 15	eqtrdi	$⊢ v = \emptyset \to ran v = \emptyset$
17	16	ineq1d	$⊢ v = \emptyset \to ran v \cap V = \emptyset \cap V$
18		0in	$⊢ \emptyset \cap V = \emptyset$
19	17 18	eqtrdi	$⊢ v = \emptyset \to ran v \cap V = \emptyset$
20	19	iuneq1d	$⊢ v = \emptyset \to ⋃_{x \in ran v \cap V} (ran F (⟨“ x ”⟩) \cap V) = ⋃_{x \in \emptyset} (ran F (⟨“ x ”⟩) \cap V)$
21		0iun	$⊢ ⋃_{x \in \emptyset} (ran F (⟨“ x ”⟩) \cap V) = \emptyset$
22	20 21	eqtrdi	$⊢ v = \emptyset \to ⋃_{x \in ran v \cap V} (ran F (⟨“ x ”⟩) \cap V) = \emptyset$
23	13 22	eqeq12d	$⊢ v = \emptyset \to (ran F (v) \cap V = ⋃_{x \in ran v \cap V} (ran F (⟨“ x ”⟩) \cap V) \leftrightarrow ran F (\emptyset) \cap V = \emptyset)$
24	23	imbi2d	$⊢ v = \emptyset \to ((F \in ran S \to ran F (v) \cap V = ⋃_{x \in ran v \cap V} (ran F (⟨“ x ”⟩) \cap V)) \leftrightarrow (F \in ran S \to ran F (\emptyset) \cap V = \emptyset))$
25		fveq2	$⊢ v = y \to F (v) = F (y)$
26	25	rneqd	$⊢ v = y \to ran F (v) = ran F (y)$
27	26	ineq1d	$⊢ v = y \to ran F (v) \cap V = ran F (y) \cap V$
28		rneq	$⊢ v = y \to ran v = ran y$
29	28	ineq1d	$⊢ v = y \to ran v \cap V = ran y \cap V$
30	29	iuneq1d	$⊢ v = y \to ⋃_{x \in ran v \cap V} (ran F (⟨“ x ”⟩) \cap V) = ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V)$
31	27 30	eqeq12d	$⊢ v = y \to (ran F (v) \cap V = ⋃_{x \in ran v \cap V} (ran F (⟨“ x ”⟩) \cap V) \leftrightarrow ran F (y) \cap V = ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V))$
32	31	imbi2d	$⊢ v = y \to ((F \in ran S \to ran F (v) \cap V = ⋃_{x \in ran v \cap V} (ran F (⟨“ x ”⟩) \cap V)) \leftrightarrow (F \in ran S \to ran F (y) \cap V = ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V)))$
33		fveq2	$⊢ v = y ++ ⟨“ z ”⟩ \to F (v) = F (y ++ ⟨“ z ”⟩)$
34	33	rneqd	$⊢ v = y ++ ⟨“ z ”⟩ \to ran F (v) = ran F (y ++ ⟨“ z ”⟩)$
35	34	ineq1d	$⊢ v = y ++ ⟨“ z ”⟩ \to ran F (v) \cap V = ran F (y ++ ⟨“ z ”⟩) \cap V$
36		rneq	$⊢ v = y ++ ⟨“ z ”⟩ \to ran v = ran (y ++ ⟨“ z ”⟩)$
37	36	ineq1d	$⊢ v = y ++ ⟨“ z ”⟩ \to ran v \cap V = ran (y ++ ⟨“ z ”⟩) \cap V$
38	37	iuneq1d	$⊢ v = y ++ ⟨“ z ”⟩ \to ⋃_{x \in ran v \cap V} (ran F (⟨“ x ”⟩) \cap V) = ⋃_{x \in ran (y ++ ⟨“ z ”⟩) \cap V} (ran F (⟨“ x ”⟩) \cap V)$
39	35 38	eqeq12d	$⊢ v = y ++ ⟨“ z ”⟩ \to (ran F (v) \cap V = ⋃_{x \in ran v \cap V} (ran F (⟨“ x ”⟩) \cap V) \leftrightarrow ran F (y ++ ⟨“ z ”⟩) \cap V = ⋃_{x \in ran (y ++ ⟨“ z ”⟩) \cap V} (ran F (⟨“ x ”⟩) \cap V))$
40	39	imbi2d	$⊢ v = y ++ ⟨“ z ”⟩ \to ((F \in ran S \to ran F (v) \cap V = ⋃_{x \in ran v \cap V} (ran F (⟨“ x ”⟩) \cap V)) \leftrightarrow (F \in ran S \to ran F (y ++ ⟨“ z ”⟩) \cap V = ⋃_{x \in ran (y ++ ⟨“ z ”⟩) \cap V} (ran F (⟨“ x ”⟩) \cap V)))$
41		fveq2	$⊢ v = X \to F (v) = F (X)$
42	41	rneqd	$⊢ v = X \to ran F (v) = ran F (X)$
43	42	ineq1d	$⊢ v = X \to ran F (v) \cap V = ran F (X) \cap V$
44		rneq	$⊢ v = X \to ran v = ran X$
45	44	ineq1d	$⊢ v = X \to ran v \cap V = ran X \cap V$
46	45	iuneq1d	$⊢ v = X \to ⋃_{x \in ran v \cap V} (ran F (⟨“ x ”⟩) \cap V) = ⋃_{x \in ran X \cap V} (ran F (⟨“ x ”⟩) \cap V)$
47	43 46	eqeq12d	$⊢ v = X \to (ran F (v) \cap V = ⋃_{x \in ran v \cap V} (ran F (⟨“ x ”⟩) \cap V) \leftrightarrow ran F (X) \cap V = ⋃_{x \in ran X \cap V} (ran F (⟨“ x ”⟩) \cap V))$
48	47	imbi2d	$⊢ v = X \to ((F \in ran S \to ran F (v) \cap V = ⋃_{x \in ran v \cap V} (ran F (⟨“ x ”⟩) \cap V)) \leftrightarrow (F \in ran S \to ran F (X) \cap V = ⋃_{x \in ran X \cap V} (ran F (⟨“ x ”⟩) \cap V)))$
49	1	mrsub0	$⊢ F \in ran S \to F (\emptyset) = \emptyset$
50	49	rneqd	$⊢ F \in ran S \to ran F (\emptyset) = ran \emptyset$
51	50 15	eqtrdi	$⊢ F \in ran S \to ran F (\emptyset) = \emptyset$
52	51	ineq1d	$⊢ F \in ran S \to ran F (\emptyset) \cap V = \emptyset \cap V$
53	52 18	eqtrdi	$⊢ F \in ran S \to ran F (\emptyset) \cap V = \emptyset$
54		uneq1	$⊢ ran F (y) \cap V = ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V) \to (ran F (y) \cap V) \cup (ran F (⟨“ z ”⟩) \cap V) = ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V) \cup (ran F (⟨“ z ”⟩) \cap V)$
55		simpl	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to F \in ran S$
56		simprl	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to y \in Word (mCN (T) \cup V)$
57	9	adantr	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to R = Word (mCN (T) \cup V)$
58	56 57	eleqtrrd	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to y \in R$
59		simprr	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to z \in (mCN (T) \cup V)$
60	59	s1cld	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ⟨“ z ”⟩ \in Word (mCN (T) \cup V)$
61	60 57	eleqtrrd	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ⟨“ z ”⟩ \in R$
62	1 3	mrsubccat	$⊢ (F \in ran S \land y \in R \land ⟨“ z ”⟩ \in R) \to F (y ++ ⟨“ z ”⟩) = F (y) ++ F (⟨“ z ”⟩)$
63	55 58 61 62	syl3anc	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to F (y ++ ⟨“ z ”⟩) = F (y) ++ F (⟨“ z ”⟩)$
64	63	rneqd	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ran F (y ++ ⟨“ z ”⟩) = ran (F (y) ++ F (⟨“ z ”⟩))$
65	1 3	mrsubf	$⊢ F \in ran S \to F : R ⟶ R$
66	65	adantr	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to F : R ⟶ R$
67	66 58	ffvelcdmd	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to F (y) \in R$
68	67 57	eleqtrd	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to F (y) \in Word (mCN (T) \cup V)$
69	66 61	ffvelcdmd	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to F (⟨“ z ”⟩) \in R$
70	69 57	eleqtrd	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to F (⟨“ z ”⟩) \in Word (mCN (T) \cup V)$
71		ccatrn	$⊢ (F (y) \in Word (mCN (T) \cup V) \land F (⟨“ z ”⟩) \in Word (mCN (T) \cup V)) \to ran (F (y) ++ F (⟨“ z ”⟩)) = ran F (y) \cup ran F (⟨“ z ”⟩)$
72	68 70 71	syl2anc	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ran (F (y) ++ F (⟨“ z ”⟩)) = ran F (y) \cup ran F (⟨“ z ”⟩)$
73	64 72	eqtrd	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ran F (y ++ ⟨“ z ”⟩) = ran F (y) \cup ran F (⟨“ z ”⟩)$
74	73	ineq1d	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ran F (y ++ ⟨“ z ”⟩) \cap V = (ran F (y) \cup ran F (⟨“ z ”⟩)) \cap V$
75		indir	$⊢ (ran F (y) \cup ran F (⟨“ z ”⟩)) \cap V = (ran F (y) \cap V) \cup (ran F (⟨“ z ”⟩) \cap V)$
76	74 75	eqtrdi	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ran F (y ++ ⟨“ z ”⟩) \cap V = (ran F (y) \cap V) \cup (ran F (⟨“ z ”⟩) \cap V)$
77		ccatrn	$⊢ (y \in Word (mCN (T) \cup V) \land ⟨“ z ”⟩ \in Word (mCN (T) \cup V)) \to ran (y ++ ⟨“ z ”⟩) = ran y \cup ran ⟨“ z ”⟩$
78	56 60 77	syl2anc	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ran (y ++ ⟨“ z ”⟩) = ran y \cup ran ⟨“ z ”⟩$
79		s1rn	$⊢ z \in (mCN (T) \cup V) \to ran ⟨“ z ”⟩ = \{z\}$
80	79	ad2antll	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ran ⟨“ z ”⟩ = \{z\}$
81	80	uneq2d	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ran y \cup ran ⟨“ z ”⟩ = ran y \cup \{z\}$
82	78 81	eqtrd	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ran (y ++ ⟨“ z ”⟩) = ran y \cup \{z\}$
83	82	ineq1d	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ran (y ++ ⟨“ z ”⟩) \cap V = (ran y \cup \{z\}) \cap V$
84		indir	$⊢ (ran y \cup \{z\}) \cap V = (ran y \cap V) \cup (\{z\} \cap V)$
85	83 84	eqtrdi	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ran (y ++ ⟨“ z ”⟩) \cap V = (ran y \cap V) \cup (\{z\} \cap V)$
86	85	iuneq1d	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ⋃_{x \in ran (y ++ ⟨“ z ”⟩) \cap V} (ran F (⟨“ x ”⟩) \cap V) = ⋃_{x \in (ran y \cap V) \cup (\{z\} \cap V)} (ran F (⟨“ x ”⟩) \cap V)$
87		iunxun	$⊢ ⋃_{x \in (ran y \cap V) \cup (\{z\} \cap V)} (ran F (⟨“ x ”⟩) \cap V) = ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V) \cup ⋃_{x \in \{z\} \cap V} (ran F (⟨“ x ”⟩) \cap V)$
88	86 87	eqtrdi	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ⋃_{x \in ran (y ++ ⟨“ z ”⟩) \cap V} (ran F (⟨“ x ”⟩) \cap V) = ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V) \cup ⋃_{x \in \{z\} \cap V} (ran F (⟨“ x ”⟩) \cap V)$
89		simpr	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land z \in V) \to z \in V$
90	89	snssd	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land z \in V) \to \{z\} \subseteq V$
91		dfss2	$⊢ \{z\} \subseteq V \leftrightarrow \{z\} \cap V = \{z\}$
92	90 91	sylib	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land z \in V) \to \{z\} \cap V = \{z\}$
93	92	iuneq1d	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land z \in V) \to ⋃_{x \in \{z\} \cap V} (ran F (⟨“ x ”⟩) \cap V) = ⋃_{x \in \{z\}} (ran F (⟨“ x ”⟩) \cap V)$
94		vex	$⊢ z \in V$
95		s1eq	$⊢ x = z \to ⟨“ x ”⟩ = ⟨“ z ”⟩$
96	95	fveq2d	$⊢ x = z \to F (⟨“ x ”⟩) = F (⟨“ z ”⟩)$
97	96	rneqd	$⊢ x = z \to ran F (⟨“ x ”⟩) = ran F (⟨“ z ”⟩)$
98	97	ineq1d	$⊢ x = z \to ran F (⟨“ x ”⟩) \cap V = ran F (⟨“ z ”⟩) \cap V$
99	94 98	iunxsn	$⊢ ⋃_{x \in \{z\}} (ran F (⟨“ x ”⟩) \cap V) = ran F (⟨“ z ”⟩) \cap V$
100	93 99	eqtrdi	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land z \in V) \to ⋃_{x \in \{z\} \cap V} (ran F (⟨“ x ”⟩) \cap V) = ran F (⟨“ z ”⟩) \cap V$
101		incom	$⊢ \{z\} \cap V = V \cap \{z\}$
102		disjsn	$⊢ V \cap \{z\} = \emptyset \leftrightarrow \neg z \in V$
103	102	bilanri	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land \neg z \in V) \to V \cap \{z\} = \emptyset$
104	101 103	eqtrid	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land \neg z \in V) \to \{z\} \cap V = \emptyset$
105	104	iuneq1d	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land \neg z \in V) \to ⋃_{x \in \{z\} \cap V} (ran F (⟨“ x ”⟩) \cap V) = ⋃_{x \in \emptyset} (ran F (⟨“ x ”⟩) \cap V)$
106	55	adantr	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land \neg z \in V) \to F \in ran S$
107		eldif	$⊢ z \in ((mCN (T) \cup V) ∖ V) \leftrightarrow (z \in (mCN (T) \cup V) \land \neg z \in V)$
108	107	biimpri	$⊢ (z \in (mCN (T) \cup V) \land \neg z \in V) \to z \in ((mCN (T) \cup V) ∖ V)$
109	59 108	sylan	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land \neg z \in V) \to z \in ((mCN (T) \cup V) ∖ V)$
110		difun2	$⊢ (mCN (T) \cup V) ∖ V = mCN (T) ∖ V$
111	109 110	eleqtrdi	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land \neg z \in V) \to z \in (mCN (T) ∖ V)$
112	1 3 2 7	mrsubcn	$⊢ (F \in ran S \land z \in (mCN (T) ∖ V)) \to F (⟨“ z ”⟩) = ⟨“ z ”⟩$
113	106 111 112	syl2anc	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land \neg z \in V) \to F (⟨“ z ”⟩) = ⟨“ z ”⟩$
114	113	rneqd	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land \neg z \in V) \to ran F (⟨“ z ”⟩) = ran ⟨“ z ”⟩$
115	80	adantr	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land \neg z \in V) \to ran ⟨“ z ”⟩ = \{z\}$
116	114 115	eqtrd	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land \neg z \in V) \to ran F (⟨“ z ”⟩) = \{z\}$
117	116	ineq1d	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land \neg z \in V) \to ran F (⟨“ z ”⟩) \cap V = \{z\} \cap V$
118	117 104	eqtrd	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land \neg z \in V) \to ran F (⟨“ z ”⟩) \cap V = \emptyset$
119	21 105 118	3eqtr4a	$⊢ ((F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \land \neg z \in V) \to ⋃_{x \in \{z\} \cap V} (ran F (⟨“ x ”⟩) \cap V) = ran F (⟨“ z ”⟩) \cap V$
120	100 119	pm2.61dan	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ⋃_{x \in \{z\} \cap V} (ran F (⟨“ x ”⟩) \cap V) = ran F (⟨“ z ”⟩) \cap V$
121	120	uneq2d	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V) \cup ⋃_{x \in \{z\} \cap V} (ran F (⟨“ x ”⟩) \cap V) = ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V) \cup (ran F (⟨“ z ”⟩) \cap V)$
122	88 121	eqtrd	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to ⋃_{x \in ran (y ++ ⟨“ z ”⟩) \cap V} (ran F (⟨“ x ”⟩) \cap V) = ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V) \cup (ran F (⟨“ z ”⟩) \cap V)$
123	76 122	eqeq12d	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to (ran F (y ++ ⟨“ z ”⟩) \cap V = ⋃_{x \in ran (y ++ ⟨“ z ”⟩) \cap V} (ran F (⟨“ x ”⟩) \cap V) \leftrightarrow (ran F (y) \cap V) \cup (ran F (⟨“ z ”⟩) \cap V) = ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V) \cup (ran F (⟨“ z ”⟩) \cap V))$
124	54 123	imbitrrid	$⊢ (F \in ran S \land (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V))) \to (ran F (y) \cap V = ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V) \to ran F (y ++ ⟨“ z ”⟩) \cap V = ⋃_{x \in ran (y ++ ⟨“ z ”⟩) \cap V} (ran F (⟨“ x ”⟩) \cap V))$
125	124	expcom	$⊢ (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V)) \to (F \in ran S \to (ran F (y) \cap V = ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V) \to ran F (y ++ ⟨“ z ”⟩) \cap V = ⋃_{x \in ran (y ++ ⟨“ z ”⟩) \cap V} (ran F (⟨“ x ”⟩) \cap V)))$
126	125	a2d	$⊢ (y \in Word (mCN (T) \cup V) \land z \in (mCN (T) \cup V)) \to ((F \in ran S \to ran F (y) \cap V = ⋃_{x \in ran y \cap V} (ran F (⟨“ x ”⟩) \cap V)) \to (F \in ran S \to ran F (y ++ ⟨“ z ”⟩) \cap V = ⋃_{x \in ran (y ++ ⟨“ z ”⟩) \cap V} (ran F (⟨“ x ”⟩) \cap V)))$
127	24 32 40 48 53 126	wrdind	$⊢ X \in Word (mCN (T) \cup V) \to (F \in ran S \to ran F (X) \cap V = ⋃_{x \in ran X \cap V} (ran F (⟨“ x ”⟩) \cap V))$
128	127	com12	$⊢ F \in ran S \to (X \in Word (mCN (T) \cup V) \to ran F (X) \cap V = ⋃_{x \in ran X \cap V} (ran F (⟨“ x ”⟩) \cap V))$
129	10 128	sylbid	$⊢ F \in ran S \to (X \in R \to ran F (X) \cap V = ⋃_{x \in ran X \cap V} (ran F (⟨“ x ”⟩) \cap V))$
130	129	imp	$⊢ (F \in ran S \land X \in R) \to ran F (X) \cap V = ⋃_{x \in ran X \cap V} (ran F (⟨“ x ”⟩) \cap V)$

Metamath Proof Explorer

Theorem mrsubvrs

Proof