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 35506

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 4345	. . . . . 6 ⊢ (𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅)
2		mrsubco.s	. . . . . . 7 ⊢ 𝑆 = (mRSubst‘𝑇)
3	2	rnfvprc 6900	. . . . . 6 ⊢ (¬ 𝑇 ∈ V → ran 𝑆 = ∅)
4	1, 3	nsyl2 141	. . . . 5 ⊢ (𝐹 ∈ ran 𝑆 → 𝑇 ∈ V)
5		eqid 2734	. . . . . 6 ⊢ (mCN‘𝑇) = (mCN‘𝑇)
6		mrsubvrs.v	. . . . . 6 ⊢ 𝑉 = (mVR‘𝑇)
7		mrsubvrs.r	. . . . . 6 ⊢ 𝑅 = (mREx‘𝑇)
8	5, 6, 7	mrexval 35485	. . . . 5 ⊢ (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
9	4, 8	syl 17	. . . 4 ⊢ (𝐹 ∈ ran 𝑆 → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
10	9	eleq2d 2824	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝑅 ↔ 𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉)))
11		fveq2 6906	. . . . . . . . 9 ⊢ (𝑣 = ∅ → (𝐹‘𝑣) = (𝐹‘∅))
12	11	rneqd 5951	. . . . . . . 8 ⊢ (𝑣 = ∅ → ran (𝐹‘𝑣) = ran (𝐹‘∅))
13	12	ineq1d 4226	. . . . . . 7 ⊢ (𝑣 = ∅ → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘∅) ∩ 𝑉))
14		rneq 5949	. . . . . . . . . . . 12 ⊢ (𝑣 = ∅ → ran 𝑣 = ran ∅)
15		rn0 5938	. . . . . . . . . . . 12 ⊢ ran ∅ = ∅
16	14, 15	eqtrdi 2790	. . . . . . . . . . 11 ⊢ (𝑣 = ∅ → ran 𝑣 = ∅)
17	16	ineq1d 4226	. . . . . . . . . 10 ⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = (∅ ∩ 𝑉))
18		0in 4402	. . . . . . . . . 10 ⊢ (∅ ∩ 𝑉) = ∅
19	17, 18	eqtrdi 2790	. . . . . . . . 9 ⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = ∅)
20	19	iuneq1d 5023	. . . . . . . 8 ⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
21		0iun 5067	. . . . . . . 8 ⊢ ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∅
22	20, 21	eqtrdi 2790	. . . . . . 7 ⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∅)
23	13, 22	eqeq12d 2750	. . . . . 6 ⊢ (𝑣 = ∅ → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘∅) ∩ 𝑉) = ∅))
24	23	imbi2d 340	. . . . 5 ⊢ (𝑣 = ∅ → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = ∅)))
25		fveq2 6906	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → (𝐹‘𝑣) = (𝐹‘𝑦))
26	25	rneqd 5951	. . . . . . . 8 ⊢ (𝑣 = 𝑦 → ran (𝐹‘𝑣) = ran (𝐹‘𝑦))
27	26	ineq1d 4226	. . . . . . 7 ⊢ (𝑣 = 𝑦 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑦) ∩ 𝑉))
28		rneq 5949	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → ran 𝑣 = ran 𝑦)
29	28	ineq1d 4226	. . . . . . . 8 ⊢ (𝑣 = 𝑦 → (ran 𝑣 ∩ 𝑉) = (ran 𝑦 ∩ 𝑉))
30	29	iuneq1d 5023	. . . . . . 7 ⊢ (𝑣 = 𝑦 → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
31	27, 30	eqeq12d 2750	. . . . . 6 ⊢ (𝑣 = 𝑦 → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
32	31	imbi2d 340	. . . . 5 ⊢ (𝑣 = 𝑦 → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
33		fveq2 6906	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (𝐹‘𝑣) = (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)))
34	33	rneqd 5951	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ran (𝐹‘𝑣) = ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)))
35	34	ineq1d 4226	. . . . . . 7 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉))
36		rneq 5949	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ran 𝑣 = ran (𝑦 ++ ⟨“𝑧”⟩))
37	36	ineq1d 4226	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (ran 𝑣 ∩ 𝑉) = (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉))
38	37	iuneq1d 5023	. . . . . . 7 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
39	35, 38	eqeq12d 2750	. . . . . 6 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
40	39	imbi2d 340	. . . . 5 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
41		fveq2 6906	. . . . . . . . 9 ⊢ (𝑣 = 𝑋 → (𝐹‘𝑣) = (𝐹‘𝑋))
42	41	rneqd 5951	. . . . . . . 8 ⊢ (𝑣 = 𝑋 → ran (𝐹‘𝑣) = ran (𝐹‘𝑋))
43	42	ineq1d 4226	. . . . . . 7 ⊢ (𝑣 = 𝑋 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑋) ∩ 𝑉))
44		rneq 5949	. . . . . . . . 9 ⊢ (𝑣 = 𝑋 → ran 𝑣 = ran 𝑋)
45	44	ineq1d 4226	. . . . . . . 8 ⊢ (𝑣 = 𝑋 → (ran 𝑣 ∩ 𝑉) = (ran 𝑋 ∩ 𝑉))
46	45	iuneq1d 5023	. . . . . . 7 ⊢ (𝑣 = 𝑋 → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
47	43, 46	eqeq12d 2750	. . . . . 6 ⊢ (𝑣 = 𝑋 → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
48	47	imbi2d 340	. . . . 5 ⊢ (𝑣 = 𝑋 → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
49	2	mrsub0 35500	. . . . . . . . 9 ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅)
50	49	rneqd 5951	. . . . . . . 8 ⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ran ∅)
51	50, 15	eqtrdi 2790	. . . . . . 7 ⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ∅)
52	51	ineq1d 4226	. . . . . 6 ⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = (∅ ∩ 𝑉))
53	52, 18	eqtrdi 2790	. . . . 5 ⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = ∅)
54		uneq1 4170	. . . . . . . 8 ⊢ ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) → ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
55		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝐹 ∈ ran 𝑆)
56		simprl 771	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉))
57	9	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
58	56, 57	eleqtrrd 2841	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑦 ∈ 𝑅)
59		simprr 773	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))
60	59	s1cld 14637	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ⟨“𝑧”⟩ ∈ Word ((mCN‘𝑇) ∪ 𝑉))
61	60, 57	eleqtrrd 2841	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ⟨“𝑧”⟩ ∈ 𝑅)
62	2, 7	mrsubccat 35502	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑦 ∈ 𝑅 ∧ ⟨“𝑧”⟩ ∈ 𝑅) → (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
63	55, 58, 61, 62	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
64	63	rneqd 5951	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ran ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
65	2, 7	mrsubf 35501	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
66	65	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝐹:𝑅⟶𝑅)
67	66, 58	ffvelcdmd 7104	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ 𝑅)
68	67, 57	eleqtrd 2840	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ Word ((mCN‘𝑇) ∪ 𝑉))
69	66, 61	ffvelcdmd 7104	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘⟨“𝑧”⟩) ∈ 𝑅)
70	69, 57	eleqtrd 2840	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘⟨“𝑧”⟩) ∈ Word ((mCN‘𝑇) ∪ 𝑉))
71		ccatrn 14623	. . . . . . . . . . . . 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 2774	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)))
74	73	ineq1d 4226	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)) ∩ 𝑉))
75		indir 4291	. . . . . . . . . 10 ⊢ ((ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
76	74, 75	eqtrdi 2790	. . . . . . . . 9 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
77		ccatrn 14623	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ ⟨“𝑧”⟩ ∈ Word ((mCN‘𝑇) ∪ 𝑉)) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ ran ⟨“𝑧”⟩))
78	56, 60, 77	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ ran ⟨“𝑧”⟩))
79		s1rn 14633	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) → ran ⟨“𝑧”⟩ = {𝑧})
80	79	ad2antll 729	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran ⟨“𝑧”⟩ = {𝑧})
81	80	uneq2d 4177	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran 𝑦 ∪ ran ⟨“𝑧”⟩) = (ran 𝑦 ∪ {𝑧}))
82	78, 81	eqtrd 2774	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ {𝑧}))
83	82	ineq1d 4226	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉) = ((ran 𝑦 ∪ {𝑧}) ∩ 𝑉))
84		indir 4291	. . . . . . . . . . . . 13 ⊢ ((ran 𝑦 ∪ {𝑧}) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))
85	83, 84	eqtrdi 2790	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉)))
86	85	iuneq1d 5023	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
87		iunxun 5098	. . . . . . . . . . 11 ⊢ ∪ 𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
88	86, 87	eqtrdi 2790	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
89		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → 𝑧 ∈ 𝑉)
90	89	snssd 4813	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → {𝑧} ⊆ 𝑉)
91		dfss2 3980	. . . . . . . . . . . . . . 15 ⊢ ({𝑧} ⊆ 𝑉 ↔ ({𝑧} ∩ 𝑉) = {𝑧})
92	90, 91	sylib 218	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = {𝑧})
93	92	iuneq1d 5023	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ {𝑧} (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
94		vex 3481	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
95		s1eq 14634	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ⟨“𝑥”⟩ = ⟨“𝑧”⟩)
96	95	fveq2d 6910	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐹‘⟨“𝑥”⟩) = (𝐹‘⟨“𝑧”⟩))
97	96	rneqd 5951	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ran (𝐹‘⟨“𝑥”⟩) = ran (𝐹‘⟨“𝑧”⟩))
98	97	ineq1d 4226	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
99	94, 98	iunxsn 5095	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ {𝑧} (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)
100	93, 99	eqtrdi 2790	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
101		incom 4216	. . . . . . . . . . . . . . 15 ⊢ ({𝑧} ∩ 𝑉) = (𝑉 ∩ {𝑧})
102		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ¬ 𝑧 ∈ 𝑉)
103		disjsn 4715	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑉)
104	102, 103	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝑉 ∩ {𝑧}) = ∅)
105	101, 104	eqtrid 2786	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = ∅)
106	105	iuneq1d 5023	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
107	55	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝐹 ∈ ran 𝑆)
108		eldif 3972	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉) ↔ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉))
109	108	biimpri 228	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉))
110	59, 109	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉))
111		difun2 4486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉) = ((mCN‘𝑇) ∖ 𝑉)
112	110, 111	eleqtrdi 2848	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉))
113	2, 7, 6, 5	mrsubcn 35503	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉)) → (𝐹‘⟨“𝑧”⟩) = ⟨“𝑧”⟩)
114	107, 112, 113	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝐹‘⟨“𝑧”⟩) = ⟨“𝑧”⟩)
115	114	rneqd 5951	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘⟨“𝑧”⟩) = ran ⟨“𝑧”⟩)
116	80	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran ⟨“𝑧”⟩ = {𝑧})
117	115, 116	eqtrd 2774	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘⟨“𝑧”⟩) = {𝑧})
118	117	ineq1d 4226	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉) = ({𝑧} ∩ 𝑉))
119	118, 105	eqtrd 2774	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉) = ∅)
120	21, 106, 119	3eqtr4a 2800	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
121	100, 120	pm2.61dan 813	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
122	121	uneq2d 4177	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
123	88, 122	eqtrd 2774	. . . . . . . . 9 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
124	76, 123	eqeq12d 2750	. . . . . . . 8 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ((ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))))
125	54, 124	imbitrrid 246	. . . . . . 7 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
126	125	expcom 413	. . . . . 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 14756	. . . 4 ⊢ (𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉) → (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
129	128	com12 32	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
130	10, 129	sylbid 240	. 2 ⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝑅 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
131	130	imp 406	1 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1536 ∈ wcel 2105 Vcvv 3477 ∖ cdif 3959 ∪ cun 3960 ∩ cin 3961 ⊆ wss 3962 ∅c0 4338 {csn 4630 ∪ ciun 4995 ran crn 5689 ⟶wf 6558 ‘cfv 6562 (class class class)co 7430 Word cword 14548 ++ cconcat 14604 ⟨“cs1 14629 mCNcmcn 35444 mVRcmvar 35445 mRExcmrex 35450 mRSubstcmrsub 35454

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-rep 5284 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-cnex 11208 ax-resscn 11209 ax-1cn 11210 ax-icn 11211 ax-addcl 11212 ax-addrcl 11213 ax-mulcl 11214 ax-mulrcl 11215 ax-mulcom 11216 ax-addass 11217 ax-mulass 11218 ax-distr 11219 ax-i2m1 11220 ax-1ne0 11221 ax-1rid 11222 ax-rnegex 11223 ax-rrecex 11224 ax-cnre 11225 ax-pre-lttri 11226 ax-pre-lttrn 11227 ax-pre-ltadd 11228 ax-pre-mulgt0 11229

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-pss 3982 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-int 4951 df-iun 4997 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5640 df-we 5642 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-pred 6322 df-ord 6388 df-on 6389 df-lim 6390 df-suc 6391 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-om 7887 df-1st 8012 df-2nd 8013 df-frecs 8304 df-wrecs 8335 df-recs 8409 df-rdg 8448 df-1o 8504 df-er 8743 df-map 8866 df-pm 8867 df-en 8984 df-dom 8985 df-sdom 8986 df-fin 8987 df-card 9976 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11491 df-neg 11492 df-nn 12264 df-2 12326 df-n0 12524 df-xnn0 12597 df-z 12611 df-uz 12876 df-fz 13544 df-fzo 13691 df-seq 14039 df-hash 14366 df-word 14549 df-lsw 14597 df-concat 14605 df-s1 14630 df-substr 14675 df-pfx 14705 df-struct 17180 df-sets 17197 df-slot 17215 df-ndx 17227 df-base 17245 df-ress 17274 df-plusg 17310 df-0g 17487 df-gsum 17488 df-mgm 18665 df-sgrp 18744 df-mnd 18760 df-submnd 18809 df-frmd 18874 df-mrex 35470 df-mrsub 35474

This theorem is referenced by: msubvrs 35544

W3C validator