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 35704

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 4280	. . . . . 6 ⊢ (𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅)
2		mrsubco.s	. . . . . . 7 ⊢ 𝑆 = (mRSubst‘𝑇)
3	2	rnfvprc 6834	. . . . . 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 35683	. . . . 5 ⊢ (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
9	4, 8	syl 17	. . . 4 ⊢ (𝐹 ∈ ran 𝑆 → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
10	9	eleq2d 2822	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝑅 ↔ 𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉)))
11		fveq2 6840	. . . . . . . . 9 ⊢ (𝑣 = ∅ → (𝐹‘𝑣) = (𝐹‘∅))
12	11	rneqd 5893	. . . . . . . 8 ⊢ (𝑣 = ∅ → ran (𝐹‘𝑣) = ran (𝐹‘∅))
13	12	ineq1d 4159	. . . . . . 7 ⊢ (𝑣 = ∅ → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘∅) ∩ 𝑉))
14		rneq 5891	. . . . . . . . . . . 12 ⊢ (𝑣 = ∅ → ran 𝑣 = ran ∅)
15		rn0 5881	. . . . . . . . . . . 12 ⊢ ran ∅ = ∅
16	14, 15	eqtrdi 2787	. . . . . . . . . . 11 ⊢ (𝑣 = ∅ → ran 𝑣 = ∅)
17	16	ineq1d 4159	. . . . . . . . . 10 ⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = (∅ ∩ 𝑉))
18		0in 4337	. . . . . . . . . 10 ⊢ (∅ ∩ 𝑉) = ∅
19	17, 18	eqtrdi 2787	. . . . . . . . 9 ⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = ∅)
20	19	iuneq1d 4961	. . . . . . . 8 ⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
21		0iun 5005	. . . . . . . 8 ⊢ ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∅
22	20, 21	eqtrdi 2787	. . . . . . 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 6840	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → (𝐹‘𝑣) = (𝐹‘𝑦))
26	25	rneqd 5893	. . . . . . . 8 ⊢ (𝑣 = 𝑦 → ran (𝐹‘𝑣) = ran (𝐹‘𝑦))
27	26	ineq1d 4159	. . . . . . 7 ⊢ (𝑣 = 𝑦 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑦) ∩ 𝑉))
28		rneq 5891	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → ran 𝑣 = ran 𝑦)
29	28	ineq1d 4159	. . . . . . . 8 ⊢ (𝑣 = 𝑦 → (ran 𝑣 ∩ 𝑉) = (ran 𝑦 ∩ 𝑉))
30	29	iuneq1d 4961	. . . . . . 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 6840	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (𝐹‘𝑣) = (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)))
34	33	rneqd 5893	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ran (𝐹‘𝑣) = ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)))
35	34	ineq1d 4159	. . . . . . 7 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉))
36		rneq 5891	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ran 𝑣 = ran (𝑦 ++ ⟨“𝑧”⟩))
37	36	ineq1d 4159	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (ran 𝑣 ∩ 𝑉) = (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉))
38	37	iuneq1d 4961	. . . . . . 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 6840	. . . . . . . . 9 ⊢ (𝑣 = 𝑋 → (𝐹‘𝑣) = (𝐹‘𝑋))
42	41	rneqd 5893	. . . . . . . 8 ⊢ (𝑣 = 𝑋 → ran (𝐹‘𝑣) = ran (𝐹‘𝑋))
43	42	ineq1d 4159	. . . . . . 7 ⊢ (𝑣 = 𝑋 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑋) ∩ 𝑉))
44		rneq 5891	. . . . . . . . 9 ⊢ (𝑣 = 𝑋 → ran 𝑣 = ran 𝑋)
45	44	ineq1d 4159	. . . . . . . 8 ⊢ (𝑣 = 𝑋 → (ran 𝑣 ∩ 𝑉) = (ran 𝑋 ∩ 𝑉))
46	45	iuneq1d 4961	. . . . . . 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 35698	. . . . . . . . 9 ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅)
50	49	rneqd 5893	. . . . . . . 8 ⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ran ∅)
51	50, 15	eqtrdi 2787	. . . . . . 7 ⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ∅)
52	51	ineq1d 4159	. . . . . 6 ⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = (∅ ∩ 𝑉))
53	52, 18	eqtrdi 2787	. . . . 5 ⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = ∅)
54		uneq1 4101	. . . . . . . 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 2839	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑦 ∈ 𝑅)
59		simprr 773	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))
60	59	s1cld 14566	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ⟨“𝑧”⟩ ∈ Word ((mCN‘𝑇) ∪ 𝑉))
61	60, 57	eleqtrrd 2839	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ⟨“𝑧”⟩ ∈ 𝑅)
62	2, 7	mrsubccat 35700	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑦 ∈ 𝑅 ∧ ⟨“𝑧”⟩ ∈ 𝑅) → (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
63	55, 58, 61, 62	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
64	63	rneqd 5893	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ran ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
65	2, 7	mrsubf 35699	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
66	65	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝐹:𝑅⟶𝑅)
67	66, 58	ffvelcdmd 7037	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ 𝑅)
68	67, 57	eleqtrd 2838	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ Word ((mCN‘𝑇) ∪ 𝑉))
69	66, 61	ffvelcdmd 7037	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘⟨“𝑧”⟩) ∈ 𝑅)
70	69, 57	eleqtrd 2838	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘⟨“𝑧”⟩) ∈ Word ((mCN‘𝑇) ∪ 𝑉))
71		ccatrn 14552	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑦) ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ (𝐹‘⟨“𝑧”⟩) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) → ran ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)))
72	68, 70, 71	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)))
73	64, 72	eqtrd 2771	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)))
74	73	ineq1d 4159	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)) ∩ 𝑉))
75		indir 4226	. . . . . . . . . 10 ⊢ ((ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
76	74, 75	eqtrdi 2787	. . . . . . . . 9 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
77		ccatrn 14552	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ ⟨“𝑧”⟩ ∈ Word ((mCN‘𝑇) ∪ 𝑉)) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ ran ⟨“𝑧”⟩))
78	56, 60, 77	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ ran ⟨“𝑧”⟩))
79		s1rn 14562	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) → ran ⟨“𝑧”⟩ = {𝑧})
80	79	ad2antll 730	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran ⟨“𝑧”⟩ = {𝑧})
81	80	uneq2d 4108	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran 𝑦 ∪ ran ⟨“𝑧”⟩) = (ran 𝑦 ∪ {𝑧}))
82	78, 81	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ {𝑧}))
83	82	ineq1d 4159	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉) = ((ran 𝑦 ∪ {𝑧}) ∩ 𝑉))
84		indir 4226	. . . . . . . . . . . . 13 ⊢ ((ran 𝑦 ∪ {𝑧}) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))
85	83, 84	eqtrdi 2787	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉)))
86	85	iuneq1d 4961	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
87		iunxun 5036	. . . . . . . . . . 11 ⊢ ∪ 𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
88	86, 87	eqtrdi 2787	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
89		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → 𝑧 ∈ 𝑉)
90	89	snssd 4730	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → {𝑧} ⊆ 𝑉)
91		dfss2 3907	. . . . . . . . . . . . . . 15 ⊢ ({𝑧} ⊆ 𝑉 ↔ ({𝑧} ∩ 𝑉) = {𝑧})
92	90, 91	sylib 218	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = {𝑧})
93	92	iuneq1d 4961	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ {𝑧} (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
94		vex 3433	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
95		s1eq 14563	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ⟨“𝑥”⟩ = ⟨“𝑧”⟩)
96	95	fveq2d 6844	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐹‘⟨“𝑥”⟩) = (𝐹‘⟨“𝑧”⟩))
97	96	rneqd 5893	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ran (𝐹‘⟨“𝑥”⟩) = ran (𝐹‘⟨“𝑧”⟩))
98	97	ineq1d 4159	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
99	94, 98	iunxsn 5033	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ {𝑧} (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)
100	93, 99	eqtrdi 2787	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
101		incom 4149	. . . . . . . . . . . . . . 15 ⊢ ({𝑧} ∩ 𝑉) = (𝑉 ∩ {𝑧})
102		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ¬ 𝑧 ∈ 𝑉)
103		disjsn 4655	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑉)
104	102, 103	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝑉 ∩ {𝑧}) = ∅)
105	101, 104	eqtrid 2783	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = ∅)
106	105	iuneq1d 4961	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
107	55	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝐹 ∈ ran 𝑆)
108		eldif 3899	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉) ↔ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉))
109	108	biimpri 228	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉))
110	59, 109	sylan 581	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉))
111		difun2 4421	. . . . . . . . . . . . . . . . . . 19 ⊢ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉) = ((mCN‘𝑇) ∖ 𝑉)
112	110, 111	eleqtrdi 2846	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉))
113	2, 7, 6, 5	mrsubcn 35701	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉)) → (𝐹‘⟨“𝑧”⟩) = ⟨“𝑧”⟩)
114	107, 112, 113	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝐹‘⟨“𝑧”⟩) = ⟨“𝑧”⟩)
115	114	rneqd 5893	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘⟨“𝑧”⟩) = ran ⟨“𝑧”⟩)
116	80	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran ⟨“𝑧”⟩ = {𝑧})
117	115, 116	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘⟨“𝑧”⟩) = {𝑧})
118	117	ineq1d 4159	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉) = ({𝑧} ∩ 𝑉))
119	118, 105	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉) = ∅)
120	21, 106, 119	3eqtr4a 2797	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
121	100, 120	pm2.61dan 813	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
122	121	uneq2d 4108	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
123	88, 122	eqtrd 2771	. . . . . . . . 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	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 14684	. . . 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 1542 ∈ wcel 2114 Vcvv 3429 ∖ cdif 3886 ∪ cun 3887 ∩ cin 3888 ⊆ wss 3889 ∅c0 4273 {csn 4567 ∪ ciun 4933 ran crn 5632 ⟶wf 6494 ‘cfv 6498 (class class class)co 7367 Word cword 14475 ++ cconcat 14532 ⟨“cs1 14558 mCNcmcn 35642 mVRcmvar 35643 mRExcmrex 35648 mRSubstcmrsub 35652

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-er 8643 df-map 8775 df-pm 8776 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-2 12244 df-n0 12438 df-xnn0 12511 df-z 12525 df-uz 12789 df-fz 13462 df-fzo 13609 df-seq 13964 df-hash 14293 df-word 14476 df-lsw 14525 df-concat 14533 df-s1 14559 df-substr 14604 df-pfx 14634 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-0g 17404 df-gsum 17405 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-submnd 18752 df-frmd 18817 df-mrex 35668 df-mrsub 35672

This theorem is referenced by: msubvrs 35742

W3C validator