mrsubvrs - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mrsubvrs		Structured version Visualization version GIF version

Theorem mrsubvrs 34116

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.)

**Hypotheses**
Ref	Expression
mrsubco.s	⊢ 𝑆 = (mRSubst‘𝑇)
mrsubvrs.v	⊢ 𝑉 = (mVR‘𝑇)
mrsubvrs.r	⊢ 𝑅 = (mREx‘𝑇)

**Assertion**
Ref	Expression
mrsubvrs	⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))

Distinct variable groups: 𝑥,𝐹 𝑥,𝑆 𝑥,𝑇 𝑥,𝑉 𝑥,𝑋 Allowed substitution hint: 𝑅(𝑥)

Proof of Theorem mrsubvrs Dummy variables 𝑣 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		n0i 4293	. . . . . 6 ⊢ (𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅)
2		mrsubco.s	. . . . . . 7 ⊢ 𝑆 = (mRSubst‘𝑇)
3	2	rnfvprc 6836	. . . . . 6 ⊢ (¬ 𝑇 ∈ V → ran 𝑆 = ∅)
4	1, 3	nsyl2 141	. . . . 5 ⊢ (𝐹 ∈ ran 𝑆 → 𝑇 ∈ V)
5		eqid 2736	. . . . . 6 ⊢ (mCN‘𝑇) = (mCN‘𝑇)
6		mrsubvrs.v	. . . . . 6 ⊢ 𝑉 = (mVR‘𝑇)
7		mrsubvrs.r	. . . . . 6 ⊢ 𝑅 = (mREx‘𝑇)
8	5, 6, 7	mrexval 34095	. . . . 5 ⊢ (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
9	4, 8	syl 17	. . . 4 ⊢ (𝐹 ∈ ran 𝑆 → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
10	9	eleq2d 2823	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝑅 ↔ 𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉)))
11		fveq2 6842	. . . . . . . . 9 ⊢ (𝑣 = ∅ → (𝐹‘𝑣) = (𝐹‘∅))
12	11	rneqd 5893	. . . . . . . 8 ⊢ (𝑣 = ∅ → ran (𝐹‘𝑣) = ran (𝐹‘∅))
13	12	ineq1d 4171	. . . . . . 7 ⊢ (𝑣 = ∅ → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘∅) ∩ 𝑉))
14		rneq 5891	. . . . . . . . . . . 12 ⊢ (𝑣 = ∅ → ran 𝑣 = ran ∅)
15		rn0 5881	. . . . . . . . . . . 12 ⊢ ran ∅ = ∅
16	14, 15	eqtrdi 2792	. . . . . . . . . . 11 ⊢ (𝑣 = ∅ → ran 𝑣 = ∅)
17	16	ineq1d 4171	. . . . . . . . . 10 ⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = (∅ ∩ 𝑉))
18		0in 4353	. . . . . . . . . 10 ⊢ (∅ ∩ 𝑉) = ∅
19	17, 18	eqtrdi 2792	. . . . . . . . 9 ⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = ∅)
20	19	iuneq1d 4981	. . . . . . . 8 ⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
21		0iun 5023	. . . . . . . 8 ⊢ ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∅
22	20, 21	eqtrdi 2792	. . . . . . 7 ⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∅)
23	13, 22	eqeq12d 2752	. . . . . 6 ⊢ (𝑣 = ∅ → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘∅) ∩ 𝑉) = ∅))
24	23	imbi2d 340	. . . . 5 ⊢ (𝑣 = ∅ → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = ∅)))
25		fveq2 6842	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → (𝐹‘𝑣) = (𝐹‘𝑦))
26	25	rneqd 5893	. . . . . . . 8 ⊢ (𝑣 = 𝑦 → ran (𝐹‘𝑣) = ran (𝐹‘𝑦))
27	26	ineq1d 4171	. . . . . . 7 ⊢ (𝑣 = 𝑦 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑦) ∩ 𝑉))
28		rneq 5891	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → ran 𝑣 = ran 𝑦)
29	28	ineq1d 4171	. . . . . . . 8 ⊢ (𝑣 = 𝑦 → (ran 𝑣 ∩ 𝑉) = (ran 𝑦 ∩ 𝑉))
30	29	iuneq1d 4981	. . . . . . 7 ⊢ (𝑣 = 𝑦 → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
31	27, 30	eqeq12d 2752	. . . . . 6 ⊢ (𝑣 = 𝑦 → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
32	31	imbi2d 340	. . . . 5 ⊢ (𝑣 = 𝑦 → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
33		fveq2 6842	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (𝐹‘𝑣) = (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)))
34	33	rneqd 5893	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ran (𝐹‘𝑣) = ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)))
35	34	ineq1d 4171	. . . . . . 7 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉))
36		rneq 5891	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ran 𝑣 = ran (𝑦 ++ ⟨“𝑧”⟩))
37	36	ineq1d 4171	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (ran 𝑣 ∩ 𝑉) = (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉))
38	37	iuneq1d 4981	. . . . . . 7 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
39	35, 38	eqeq12d 2752	. . . . . 6 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
40	39	imbi2d 340	. . . . 5 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
41		fveq2 6842	. . . . . . . . 9 ⊢ (𝑣 = 𝑋 → (𝐹‘𝑣) = (𝐹‘𝑋))
42	41	rneqd 5893	. . . . . . . 8 ⊢ (𝑣 = 𝑋 → ran (𝐹‘𝑣) = ran (𝐹‘𝑋))
43	42	ineq1d 4171	. . . . . . 7 ⊢ (𝑣 = 𝑋 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑋) ∩ 𝑉))
44		rneq 5891	. . . . . . . . 9 ⊢ (𝑣 = 𝑋 → ran 𝑣 = ran 𝑋)
45	44	ineq1d 4171	. . . . . . . 8 ⊢ (𝑣 = 𝑋 → (ran 𝑣 ∩ 𝑉) = (ran 𝑋 ∩ 𝑉))
46	45	iuneq1d 4981	. . . . . . 7 ⊢ (𝑣 = 𝑋 → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
47	43, 46	eqeq12d 2752	. . . . . 6 ⊢ (𝑣 = 𝑋 → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
48	47	imbi2d 340	. . . . 5 ⊢ (𝑣 = 𝑋 → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
49	2	mrsub0 34110	. . . . . . . . 9 ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅)
50	49	rneqd 5893	. . . . . . . 8 ⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ran ∅)
51	50, 15	eqtrdi 2792	. . . . . . 7 ⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ∅)
52	51	ineq1d 4171	. . . . . 6 ⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = (∅ ∩ 𝑉))
53	52, 18	eqtrdi 2792	. . . . 5 ⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = ∅)
54		uneq1 4116	. . . . . . . 8 ⊢ ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) → ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
55		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝐹 ∈ ran 𝑆)
56		simprl 769	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉))
57	9	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
58	56, 57	eleqtrrd 2841	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑦 ∈ 𝑅)
59		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))
60	59	s1cld 14491	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ⟨“𝑧”⟩ ∈ Word ((mCN‘𝑇) ∪ 𝑉))
61	60, 57	eleqtrrd 2841	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ⟨“𝑧”⟩ ∈ 𝑅)
62	2, 7	mrsubccat 34112	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑦 ∈ 𝑅 ∧ ⟨“𝑧”⟩ ∈ 𝑅) → (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
63	55, 58, 61, 62	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
64	63	rneqd 5893	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ran ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
65	2, 7	mrsubf 34111	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
66	65	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝐹:𝑅⟶𝑅)
67	66, 58	ffvelcdmd 7036	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ 𝑅)
68	67, 57	eleqtrd 2840	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ Word ((mCN‘𝑇) ∪ 𝑉))
69	66, 61	ffvelcdmd 7036	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘⟨“𝑧”⟩) ∈ 𝑅)
70	69, 57	eleqtrd 2840	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘⟨“𝑧”⟩) ∈ Word ((mCN‘𝑇) ∪ 𝑉))
71		ccatrn 14477	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑦) ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ (𝐹‘⟨“𝑧”⟩) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) → ran ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)))
72	68, 70, 71	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)))
73	64, 72	eqtrd 2776	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)))
74	73	ineq1d 4171	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)) ∩ 𝑉))
75		indir 4235	. . . . . . . . . 10 ⊢ ((ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
76	74, 75	eqtrdi 2792	. . . . . . . . 9 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
77		ccatrn 14477	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ ⟨“𝑧”⟩ ∈ Word ((mCN‘𝑇) ∪ 𝑉)) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ ran ⟨“𝑧”⟩))
78	56, 60, 77	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ ran ⟨“𝑧”⟩))
79		s1rn 14487	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) → ran ⟨“𝑧”⟩ = {𝑧})
80	79	ad2antll 727	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran ⟨“𝑧”⟩ = {𝑧})
81	80	uneq2d 4123	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran 𝑦 ∪ ran ⟨“𝑧”⟩) = (ran 𝑦 ∪ {𝑧}))
82	78, 81	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ {𝑧}))
83	82	ineq1d 4171	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉) = ((ran 𝑦 ∪ {𝑧}) ∩ 𝑉))
84		indir 4235	. . . . . . . . . . . . 13 ⊢ ((ran 𝑦 ∪ {𝑧}) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))
85	83, 84	eqtrdi 2792	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉)))
86	85	iuneq1d 4981	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
87		iunxun 5054	. . . . . . . . . . 11 ⊢ ∪ 𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
88	86, 87	eqtrdi 2792	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
89		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → 𝑧 ∈ 𝑉)
90	89	snssd 4769	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → {𝑧} ⊆ 𝑉)
91		df-ss 3927	. . . . . . . . . . . . . . 15 ⊢ ({𝑧} ⊆ 𝑉 ↔ ({𝑧} ∩ 𝑉) = {𝑧})
92	90, 91	sylib 217	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = {𝑧})
93	92	iuneq1d 4981	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ {𝑧} (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
94		vex 3449	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
95		s1eq 14488	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ⟨“𝑥”⟩ = ⟨“𝑧”⟩)
96	95	fveq2d 6846	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐹‘⟨“𝑥”⟩) = (𝐹‘⟨“𝑧”⟩))
97	96	rneqd 5893	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ran (𝐹‘⟨“𝑥”⟩) = ran (𝐹‘⟨“𝑧”⟩))
98	97	ineq1d 4171	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
99	94, 98	iunxsn 5051	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ {𝑧} (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)
100	93, 99	eqtrdi 2792	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
101		incom 4161	. . . . . . . . . . . . . . 15 ⊢ ({𝑧} ∩ 𝑉) = (𝑉 ∩ {𝑧})
102		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ¬ 𝑧 ∈ 𝑉)
103		disjsn 4672	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑉)
104	102, 103	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝑉 ∩ {𝑧}) = ∅)
105	101, 104	eqtrid 2788	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = ∅)
106	105	iuneq1d 4981	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
107	55	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝐹 ∈ ran 𝑆)
108		eldif 3920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉) ↔ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉))
109	108	biimpri 227	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉))
110	59, 109	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉))
111		difun2 4440	. . . . . . . . . . . . . . . . . . 19 ⊢ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉) = ((mCN‘𝑇) ∖ 𝑉)
112	110, 111	eleqtrdi 2848	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉))
113	2, 7, 6, 5	mrsubcn 34113	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉)) → (𝐹‘⟨“𝑧”⟩) = ⟨“𝑧”⟩)
114	107, 112, 113	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝐹‘⟨“𝑧”⟩) = ⟨“𝑧”⟩)
115	114	rneqd 5893	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘⟨“𝑧”⟩) = ran ⟨“𝑧”⟩)
116	80	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran ⟨“𝑧”⟩ = {𝑧})
117	115, 116	eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘⟨“𝑧”⟩) = {𝑧})
118	117	ineq1d 4171	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉) = ({𝑧} ∩ 𝑉))
119	118, 105	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉) = ∅)
120	21, 106, 119	3eqtr4a 2802	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
121	100, 120	pm2.61dan 811	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
122	121	uneq2d 4123	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
123	88, 122	eqtrd 2776	. . . . . . . . 9 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
124	76, 123	eqeq12d 2752	. . . . . . . 8 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ((ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))))
125	54, 124	syl5ibr 245	. . . . . . 7 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
126	125	expcom 414	. . . . . 6 ⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉)) → (𝐹 ∈ ran 𝑆 → ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
127	126	a2d 29	. . . . 5 ⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉)) → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) → (𝐹 ∈ ran 𝑆 → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
128	24, 32, 40, 48, 53, 127	wrdind 14610	. . . 4 ⊢ (𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉) → (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
129	128	com12 32	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
130	10, 129	sylbid 239	. 2 ⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝑅 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
131	130	imp 407	1 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 Vcvv 3445 ∖ cdif 3907 ∪ cun 3908 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 {csn 4586 ∪ ciun 4954 ran crn 5634 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 Word cword 14402 ++ cconcat 14458 ⟨“cs1 14483 mCNcmcn 34054 mVRcmvar 34055 mRExcmrex 34060 mRSubstcmrsub 34064

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-er 8648 df-map 8767 df-pm 8768 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-nn 12154 df-2 12216 df-n0 12414 df-xnn0 12486 df-z 12500 df-uz 12764 df-fz 13425 df-fzo 13568 df-seq 13907 df-hash 14231 df-word 14403 df-lsw 14451 df-concat 14459 df-s1 14484 df-substr 14529 df-pfx 14559 df-struct 17019 df-sets 17036 df-slot 17054 df-ndx 17066 df-base 17084 df-ress 17113 df-plusg 17146 df-0g 17323 df-gsum 17324 df-mgm 18497 df-sgrp 18546 df-mnd 18557 df-submnd 18602 df-frmd 18659 df-mrex 34080 df-mrsub 34084

This theorem is referenced by: msubvrs 34154

W3C validator