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 31419

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 3920	. . . . . 6 ⊢ (𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅)
2		mrsubco.s	. . . . . . . . 9 ⊢ 𝑆 = (mRSubst‘𝑇)
3		fvprc 6185	. . . . . . . . 9 ⊢ (¬ 𝑇 ∈ V → (mRSubst‘𝑇) = ∅)
4	2, 3	syl5eq 2668	. . . . . . . 8 ⊢ (¬ 𝑇 ∈ V → 𝑆 = ∅)
5	4	rneqd 5353	. . . . . . 7 ⊢ (¬ 𝑇 ∈ V → ran 𝑆 = ran ∅)
6		rn0 5377	. . . . . . 7 ⊢ ran ∅ = ∅
7	5, 6	syl6eq 2672	. . . . . 6 ⊢ (¬ 𝑇 ∈ V → ran 𝑆 = ∅)
8	1, 7	nsyl2 142	. . . . 5 ⊢ (𝐹 ∈ ran 𝑆 → 𝑇 ∈ V)
9		eqid 2622	. . . . . 6 ⊢ (mCN‘𝑇) = (mCN‘𝑇)
10		mrsubvrs.v	. . . . . 6 ⊢ 𝑉 = (mVR‘𝑇)
11		mrsubvrs.r	. . . . . 6 ⊢ 𝑅 = (mREx‘𝑇)
12	9, 10, 11	mrexval 31398	. . . . 5 ⊢ (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
13	8, 12	syl 17	. . . 4 ⊢ (𝐹 ∈ ran 𝑆 → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
14	13	eleq2d 2687	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝑅 ↔ 𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉)))
15		fveq2 6191	. . . . . . . . 9 ⊢ (𝑣 = ∅ → (𝐹‘𝑣) = (𝐹‘∅))
16	15	rneqd 5353	. . . . . . . 8 ⊢ (𝑣 = ∅ → ran (𝐹‘𝑣) = ran (𝐹‘∅))
17	16	ineq1d 3813	. . . . . . 7 ⊢ (𝑣 = ∅ → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘∅) ∩ 𝑉))
18		rneq 5351	. . . . . . . . . . . 12 ⊢ (𝑣 = ∅ → ran 𝑣 = ran ∅)
19	18, 6	syl6eq 2672	. . . . . . . . . . 11 ⊢ (𝑣 = ∅ → ran 𝑣 = ∅)
20	19	ineq1d 3813	. . . . . . . . . 10 ⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = (∅ ∩ 𝑉))
21		0in 3969	. . . . . . . . . 10 ⊢ (∅ ∩ 𝑉) = ∅
22	20, 21	syl6eq 2672	. . . . . . . . 9 ⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = ∅)
23	22	iuneq1d 4545	. . . . . . . 8 ⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
24		0iun 4577	. . . . . . . 8 ⊢ ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∅
25	23, 24	syl6eq 2672	. . . . . . 7 ⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∅)
26	17, 25	eqeq12d 2637	. . . . . 6 ⊢ (𝑣 = ∅ → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘∅) ∩ 𝑉) = ∅))
27	26	imbi2d 330	. . . . 5 ⊢ (𝑣 = ∅ → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = ∅)))
28		fveq2 6191	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → (𝐹‘𝑣) = (𝐹‘𝑦))
29	28	rneqd 5353	. . . . . . . 8 ⊢ (𝑣 = 𝑦 → ran (𝐹‘𝑣) = ran (𝐹‘𝑦))
30	29	ineq1d 3813	. . . . . . 7 ⊢ (𝑣 = 𝑦 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑦) ∩ 𝑉))
31		rneq 5351	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → ran 𝑣 = ran 𝑦)
32	31	ineq1d 3813	. . . . . . . 8 ⊢ (𝑣 = 𝑦 → (ran 𝑣 ∩ 𝑉) = (ran 𝑦 ∩ 𝑉))
33	32	iuneq1d 4545	. . . . . . 7 ⊢ (𝑣 = 𝑦 → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
34	30, 33	eqeq12d 2637	. . . . . 6 ⊢ (𝑣 = 𝑦 → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
35	34	imbi2d 330	. . . . 5 ⊢ (𝑣 = 𝑦 → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
36		fveq2 6191	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (𝐹‘𝑣) = (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)))
37	36	rneqd 5353	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ran (𝐹‘𝑣) = ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)))
38	37	ineq1d 3813	. . . . . . 7 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉))
39		rneq 5351	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ran 𝑣 = ran (𝑦 ++ ⟨“𝑧”⟩))
40	39	ineq1d 3813	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (ran 𝑣 ∩ 𝑉) = (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉))
41	40	iuneq1d 4545	. . . . . . 7 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
42	38, 41	eqeq12d 2637	. . . . . 6 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
43	42	imbi2d 330	. . . . 5 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
44		fveq2 6191	. . . . . . . . 9 ⊢ (𝑣 = 𝑋 → (𝐹‘𝑣) = (𝐹‘𝑋))
45	44	rneqd 5353	. . . . . . . 8 ⊢ (𝑣 = 𝑋 → ran (𝐹‘𝑣) = ran (𝐹‘𝑋))
46	45	ineq1d 3813	. . . . . . 7 ⊢ (𝑣 = 𝑋 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑋) ∩ 𝑉))
47		rneq 5351	. . . . . . . . 9 ⊢ (𝑣 = 𝑋 → ran 𝑣 = ran 𝑋)
48	47	ineq1d 3813	. . . . . . . 8 ⊢ (𝑣 = 𝑋 → (ran 𝑣 ∩ 𝑉) = (ran 𝑋 ∩ 𝑉))
49	48	iuneq1d 4545	. . . . . . 7 ⊢ (𝑣 = 𝑋 → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
50	46, 49	eqeq12d 2637	. . . . . 6 ⊢ (𝑣 = 𝑋 → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
51	50	imbi2d 330	. . . . 5 ⊢ (𝑣 = 𝑋 → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
52	2	mrsub0 31413	. . . . . . . . 9 ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅)
53	52	rneqd 5353	. . . . . . . 8 ⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ran ∅)
54	53, 6	syl6eq 2672	. . . . . . 7 ⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ∅)
55	54	ineq1d 3813	. . . . . 6 ⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = (∅ ∩ 𝑉))
56	55, 21	syl6eq 2672	. . . . 5 ⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = ∅)
57		uneq1 3760	. . . . . . . 8 ⊢ ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) → ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
58		simpl 473	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝐹 ∈ ran 𝑆)
59		simprl 794	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉))
60	13	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
61	59, 60	eleqtrrd 2704	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑦 ∈ 𝑅)
62		simprr 796	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))
63	62	s1cld 13383	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ⟨“𝑧”⟩ ∈ Word ((mCN‘𝑇) ∪ 𝑉))
64	63, 60	eleqtrrd 2704	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ⟨“𝑧”⟩ ∈ 𝑅)
65	2, 11	mrsubccat 31415	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑦 ∈ 𝑅 ∧ ⟨“𝑧”⟩ ∈ 𝑅) → (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
66	58, 61, 64, 65	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
67	66	rneqd 5353	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ran ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
68	2, 11	mrsubf 31414	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
69	68	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝐹:𝑅⟶𝑅)
70	69, 61	ffvelrnd 6360	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ 𝑅)
71	70, 60	eleqtrd 2703	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ Word ((mCN‘𝑇) ∪ 𝑉))
72	69, 64	ffvelrnd 6360	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘⟨“𝑧”⟩) ∈ 𝑅)
73	72, 60	eleqtrd 2703	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘⟨“𝑧”⟩) ∈ Word ((mCN‘𝑇) ∪ 𝑉))
74		ccatrn 13372	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑦) ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ (𝐹‘⟨“𝑧”⟩) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) → ran ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)))
75	71, 73, 74	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)))
76	67, 75	eqtrd 2656	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)))
77	76	ineq1d 3813	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)) ∩ 𝑉))
78		indir 3875	. . . . . . . . . 10 ⊢ ((ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
79	77, 78	syl6eq 2672	. . . . . . . . 9 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
80		ccatrn 13372	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ ⟨“𝑧”⟩ ∈ Word ((mCN‘𝑇) ∪ 𝑉)) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ ran ⟨“𝑧”⟩))
81	59, 63, 80	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ ran ⟨“𝑧”⟩))
82		s1rn 13379	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) → ran ⟨“𝑧”⟩ = {𝑧})
83	82	ad2antll 765	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran ⟨“𝑧”⟩ = {𝑧})
84	83	uneq2d 3767	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran 𝑦 ∪ ran ⟨“𝑧”⟩) = (ran 𝑦 ∪ {𝑧}))
85	81, 84	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ {𝑧}))
86	85	ineq1d 3813	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉) = ((ran 𝑦 ∪ {𝑧}) ∩ 𝑉))
87		indir 3875	. . . . . . . . . . . . 13 ⊢ ((ran 𝑦 ∪ {𝑧}) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))
88	86, 87	syl6eq 2672	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉)))
89	88	iuneq1d 4545	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
90		iunxun 4605	. . . . . . . . . . 11 ⊢ ∪ 𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
91	89, 90	syl6eq 2672	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
92		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → 𝑧 ∈ 𝑉)
93	92	snssd 4340	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → {𝑧} ⊆ 𝑉)
94		df-ss 3588	. . . . . . . . . . . . . . 15 ⊢ ({𝑧} ⊆ 𝑉 ↔ ({𝑧} ∩ 𝑉) = {𝑧})
95	93, 94	sylib 208	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = {𝑧})
96	95	iuneq1d 4545	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ {𝑧} (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
97		vex 3203	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
98		s1eq 13380	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ⟨“𝑥”⟩ = ⟨“𝑧”⟩)
99	98	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐹‘⟨“𝑥”⟩) = (𝐹‘⟨“𝑧”⟩))
100	99	rneqd 5353	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ran (𝐹‘⟨“𝑥”⟩) = ran (𝐹‘⟨“𝑧”⟩))
101	100	ineq1d 3813	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
102	97, 101	iunxsn 4603	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ {𝑧} (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)
103	96, 102	syl6eq 2672	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
104		incom 3805	. . . . . . . . . . . . . . 15 ⊢ ({𝑧} ∩ 𝑉) = (𝑉 ∩ {𝑧})
105		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ¬ 𝑧 ∈ 𝑉)
106		disjsn 4246	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑉)
107	105, 106	sylibr 224	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝑉 ∩ {𝑧}) = ∅)
108	104, 107	syl5eq 2668	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = ∅)
109	108	iuneq1d 4545	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
110	58	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝐹 ∈ ran 𝑆)
111		eldif 3584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉) ↔ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉))
112	111	biimpri 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉))
113	62, 112	sylan 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉))
114		difun2 4048	. . . . . . . . . . . . . . . . . . 19 ⊢ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉) = ((mCN‘𝑇) ∖ 𝑉)
115	113, 114	syl6eleq 2711	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉))
116	2, 11, 10, 9	mrsubcn 31416	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉)) → (𝐹‘⟨“𝑧”⟩) = ⟨“𝑧”⟩)
117	110, 115, 116	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝐹‘⟨“𝑧”⟩) = ⟨“𝑧”⟩)
118	117	rneqd 5353	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘⟨“𝑧”⟩) = ran ⟨“𝑧”⟩)
119	83	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran ⟨“𝑧”⟩ = {𝑧})
120	118, 119	eqtrd 2656	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘⟨“𝑧”⟩) = {𝑧})
121	120	ineq1d 3813	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉) = ({𝑧} ∩ 𝑉))
122	121, 108	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉) = ∅)
123	24, 109, 122	3eqtr4a 2682	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
124	103, 123	pm2.61dan 832	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
125	124	uneq2d 3767	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
126	91, 125	eqtrd 2656	. . . . . . . . 9 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
127	79, 126	eqeq12d 2637	. . . . . . . 8 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ((ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))))
128	57, 127	syl5ibr 236	. . . . . . 7 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
129	128	expcom 451	. . . . . 6 ⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉)) → (𝐹 ∈ ran 𝑆 → ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
130	129	a2d 29	. . . . 5 ⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉)) → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) → (𝐹 ∈ ran 𝑆 → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
131	27, 35, 43, 51, 56, 130	wrdind 13476	. . . 4 ⊢ (𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉) → (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
132	131	com12 32	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
133	14, 132	sylbid 230	. 2 ⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝑅 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
134	133	imp 445	1 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 {csn 4177 ∪ ciun 4520 ran crn 5115 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 Word cword 13291 ++ cconcat 13293 ⟨“cs1 13294 mCNcmcn 31357 mVRcmvar 31358 mRExcmrex 31363 mRSubstcmrsub 31367

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466 df-seq 12802 df-hash 13118 df-word 13299 df-lsw 13300 df-concat 13301 df-s1 13302 df-substr 13303 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-0g 16102 df-gsum 16103 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-frmd 17386 df-mrex 31383 df-mrsub 31387

This theorem is referenced by: msubvrs 31457

W3C validator