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 36374

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 4285	. . . . . 6 ⊢ (𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅)
2		mrsubco.s	. . . . . . 7 ⊢ 𝑆 = (mRSubst‘𝑇)
3	2	rnfvprc 6880	. . . . . 6 ⊢ (¬ 𝑇 ∈ V → ran 𝑆 = ∅)
4	1, 3	nsyl2 142	. . . . 5 ⊢ (𝐹 ∈ ran 𝑆 → 𝑇 ∈ V)
5		eqid 2760	. . . . . 6 ⊢ (mCN‘𝑇) = (mCN‘𝑇)
6		mrsubvrs.v	. . . . . 6 ⊢ 𝑉 = (mVR‘𝑇)
7		mrsubvrs.r	. . . . . 6 ⊢ 𝑅 = (mREx‘𝑇)
8	5, 6, 7	mrexval 36353	. . . . 5 ⊢ (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
9	4, 8	syl 18	. . . 4 ⊢ (𝐹 ∈ ran 𝑆 → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
10	9	eleq2d 2846	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝑅 ↔ 𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉)))
11		fveq2 6886	. . . . . . . . 9 ⊢ (𝑣 = ∅ → (𝐹‘𝑣) = (𝐹‘∅))
12	11	rneqd 5919	. . . . . . . 8 ⊢ (𝑣 = ∅ → ran (𝐹‘𝑣) = ran (𝐹‘∅))
13	12	ineq1d 4116	. . . . . . 7 ⊢ (𝑣 = ∅ → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘∅) ∩ 𝑉))
14		rneq 5917	. . . . . . . . . . . 12 ⊢ (𝑣 = ∅ → ran 𝑣 = ran ∅)
15		rn0 5907	. . . . . . . . . . . 12 ⊢ ran ∅ = ∅
16	14, 15	eqtrdi 2811	. . . . . . . . . . 11 ⊢ (𝑣 = ∅ → ran 𝑣 = ∅)
17	16	ineq1d 4116	. . . . . . . . . 10 ⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = (∅ ∩ 𝑉))
18		0in 4346	. . . . . . . . . 10 ⊢ (∅ ∩ 𝑉) = ∅
19	17, 18	eqtrdi 2811	. . . . . . . . 9 ⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = ∅)
20	19	iuneq1d 4978	. . . . . . . 8 ⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
21		0iun 5020	. . . . . . . 8 ⊢ ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∅
22	20, 21	eqtrdi 2811	. . . . . . 7 ⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∅)
23	13, 22	eqeq12d 2776	. . . . . 6 ⊢ (𝑣 = ∅ → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘∅) ∩ 𝑉) = ∅))
24	23	imbi2d 343	. . . . 5 ⊢ (𝑣 = ∅ → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = ∅)))
25		fveq2 6886	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → (𝐹‘𝑣) = (𝐹‘𝑦))
26	25	rneqd 5919	. . . . . . . 8 ⊢ (𝑣 = 𝑦 → ran (𝐹‘𝑣) = ran (𝐹‘𝑦))
27	26	ineq1d 4116	. . . . . . 7 ⊢ (𝑣 = 𝑦 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑦) ∩ 𝑉))
28		rneq 5917	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → ran 𝑣 = ran 𝑦)
29	28	ineq1d 4116	. . . . . . . 8 ⊢ (𝑣 = 𝑦 → (ran 𝑣 ∩ 𝑉) = (ran 𝑦 ∩ 𝑉))
30	29	iuneq1d 4978	. . . . . . 7 ⊢ (𝑣 = 𝑦 → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
31	27, 30	eqeq12d 2776	. . . . . 6 ⊢ (𝑣 = 𝑦 → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
32	31	imbi2d 343	. . . . 5 ⊢ (𝑣 = 𝑦 → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
33		fveq2 6886	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (𝐹‘𝑣) = (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)))
34	33	rneqd 5919	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ran (𝐹‘𝑣) = ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)))
35	34	ineq1d 4116	. . . . . . 7 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉))
36		rneq 5917	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ran 𝑣 = ran (𝑦 ++ ⟨“𝑧”⟩))
37	36	ineq1d 4116	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → (ran 𝑣 ∩ 𝑉) = (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉))
38	37	iuneq1d 4978	. . . . . . 7 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
39	35, 38	eqeq12d 2776	. . . . . 6 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
40	39	imbi2d 343	. . . . 5 ⊢ (𝑣 = (𝑦 ++ ⟨“𝑧”⟩) → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
41		fveq2 6886	. . . . . . . . 9 ⊢ (𝑣 = 𝑋 → (𝐹‘𝑣) = (𝐹‘𝑋))
42	41	rneqd 5919	. . . . . . . 8 ⊢ (𝑣 = 𝑋 → ran (𝐹‘𝑣) = ran (𝐹‘𝑋))
43	42	ineq1d 4116	. . . . . . 7 ⊢ (𝑣 = 𝑋 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑋) ∩ 𝑉))
44		rneq 5917	. . . . . . . . 9 ⊢ (𝑣 = 𝑋 → ran 𝑣 = ran 𝑋)
45	44	ineq1d 4116	. . . . . . . 8 ⊢ (𝑣 = 𝑋 → (ran 𝑣 ∩ 𝑉) = (ran 𝑋 ∩ 𝑉))
46	45	iuneq1d 4978	. . . . . . 7 ⊢ (𝑣 = 𝑋 → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
47	43, 46	eqeq12d 2776	. . . . . 6 ⊢ (𝑣 = 𝑋 → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
48	47	imbi2d 343	. . . . 5 ⊢ (𝑣 = 𝑋 → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
49	2	mrsub0 36368	. . . . . . . . 9 ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅)
50	49	rneqd 5919	. . . . . . . 8 ⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ran ∅)
51	50, 15	eqtrdi 2811	. . . . . . 7 ⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ∅)
52	51	ineq1d 4116	. . . . . 6 ⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = (∅ ∩ 𝑉))
53	52, 18	eqtrdi 2811	. . . . 5 ⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = ∅)
54		uneq1 4160	. . . . . . . 8 ⊢ ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) → ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
55		simpl 488	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝐹 ∈ ran 𝑆)
56		simprl 783	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉))
57	9	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
58	56, 57	eleqtrrd 2863	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑦 ∈ 𝑅)
59		simprr 785	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))
60	59	s1cld 14754	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ⟨“𝑧”⟩ ∈ Word ((mCN‘𝑇) ∪ 𝑉))
61	60, 57	eleqtrrd 2863	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ⟨“𝑧”⟩ ∈ 𝑅)
62	2, 7	mrsubccat 36370	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑦 ∈ 𝑅 ∧ ⟨“𝑧”⟩ ∈ 𝑅) → (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
63	55, 58, 61, 62	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
64	63	rneqd 5919	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = ran ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)))
65	2, 7	mrsubf 36369	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
66	65	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝐹:𝑅⟶𝑅)
67	66, 58	ffvelcdmd 7086	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ 𝑅)
68	67, 57	eleqtrd 2862	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ Word ((mCN‘𝑇) ∪ 𝑉))
69	66, 61	ffvelcdmd 7086	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘⟨“𝑧”⟩) ∈ 𝑅)
70	69, 57	eleqtrd 2862	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘⟨“𝑧”⟩) ∈ Word ((mCN‘𝑇) ∪ 𝑉))
71		ccatrn 14739	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑦) ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ (𝐹‘⟨“𝑧”⟩) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) → ran ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)))
72	68, 70, 71	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran ((𝐹‘𝑦) ++ (𝐹‘⟨“𝑧”⟩)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)))
73	64, 72	eqtrd 2795	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)))
74	73	ineq1d 4116	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)) ∩ 𝑉))
75		indir 4231	. . . . . . . . . 10 ⊢ ((ran (𝐹‘𝑦) ∪ ran (𝐹‘⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
76	74, 75	eqtrdi 2811	. . . . . . . . 9 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
77		ccatrn 14739	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ ⟨“𝑧”⟩ ∈ Word ((mCN‘𝑇) ∪ 𝑉)) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ ran ⟨“𝑧”⟩))
78	56, 60, 77	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ ran ⟨“𝑧”⟩))
79		s1rn 14750	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) → ran ⟨“𝑧”⟩ = {𝑧})
80	79	ad2antll 742	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran ⟨“𝑧”⟩ = {𝑧})
81	80	uneq2d 4167	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran 𝑦 ∪ ran ⟨“𝑧”⟩) = (ran 𝑦 ∪ {𝑧}))
82	78, 81	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ ⟨“𝑧”⟩) = (ran 𝑦 ∪ {𝑧}))
83	82	ineq1d 4116	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉) = ((ran 𝑦 ∪ {𝑧}) ∩ 𝑉))
84		indir 4231	. . . . . . . . . . . . 13 ⊢ ((ran 𝑦 ∪ {𝑧}) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))
85	83, 84	eqtrdi 2811	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉)))
86	85	iuneq1d 4978	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
87		iunxun 5053	. . . . . . . . . . 11 ⊢ ∪ 𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
88	86, 87	eqtrdi 2811	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
89		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → 𝑧 ∈ 𝑉)
90	89	snssd 4743	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → {𝑧} ⊆ 𝑉)
91		dfss2 4094	. . . . . . . . . . . . . . 15 ⊢ ({𝑧} ⊆ 𝑉 ↔ ({𝑧} ∩ 𝑉) = {𝑧})
92	90, 91	sylib 221	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = {𝑧})
93	92	iuneq1d 4978	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ {𝑧} (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
94		vex 3454	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
95		s1eq 14751	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ⟨“𝑥”⟩ = ⟨“𝑧”⟩)
96	95	fveq2d 6890	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐹‘⟨“𝑥”⟩) = (𝐹‘⟨“𝑧”⟩))
97	96	rneqd 5919	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ran (𝐹‘⟨“𝑥”⟩) = ran (𝐹‘⟨“𝑧”⟩))
98	97	ineq1d 4116	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
99	94, 98	iunxsn 5050	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ {𝑧} (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)
100	93, 99	eqtrdi 2811	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
101		incom 4106	. . . . . . . . . . . . . . 15 ⊢ ({𝑧} ∩ 𝑉) = (𝑉 ∩ {𝑧})
102		disjsn 4668	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑉)
103	102	bilanri 512	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝑉 ∩ {𝑧}) = ∅)
104	101, 103	eqtrid 2807	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = ∅)
105	104	iuneq1d 4978	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = ∪ 𝑥 ∈ ∅ (ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
106	55	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝐹 ∈ ran 𝑆)
107		eldif 4049	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉) ↔ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉))
108	107	biimpri 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉))
109	59, 108	sylan 592	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉))
110		difun2 4436	. . . . . . . . . . . . . . . . . . 19 ⊢ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉) = ((mCN‘𝑇) ∖ 𝑉)
111	109, 110	eleqtrdi 2870	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉))
112	2, 7, 6, 5	mrsubcn 36371	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉)) → (𝐹‘⟨“𝑧”⟩) = ⟨“𝑧”⟩)
113	106, 111, 112	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝐹‘⟨“𝑧”⟩) = ⟨“𝑧”⟩)
114	113	rneqd 5919	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘⟨“𝑧”⟩) = ran ⟨“𝑧”⟩)
115	80	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran ⟨“𝑧”⟩ = {𝑧})
116	114, 115	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘⟨“𝑧”⟩) = {𝑧})
117	116	ineq1d 4116	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉) = ({𝑧} ∩ 𝑉))
118	117, 104	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉) = ∅)
119	21, 105, 118	3eqtr4a 2821	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
120	100, 119	pm2.61dan 825	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))
121	120	uneq2d 4167	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
122	88, 121	eqtrd 2795	. . . . . . . . 9 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)))
123	76, 122	eqeq12d 2776	. . . . . . . 8 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ((ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ↔ ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉)) = (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) ∪ (ran (𝐹‘⟨“𝑧”⟩) ∩ 𝑉))))
124	54, 123	imbitrrid 249	. . . . . . 7 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
125	124	expcom 419	. . . . . 6 ⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉)) → (𝐹 ∈ ran 𝑆 → ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉) → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
126	125	a2d 30	. . . . 5 ⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉)) → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑦) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)) → (𝐹 ∈ ran 𝑆 → (ran (𝐹‘(𝑦 ++ ⟨“𝑧”⟩)) ∩ 𝑉) = ∪ 𝑥 ∈ (ran (𝑦 ++ ⟨“𝑧”⟩) ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))))
127	24, 32, 40, 48, 53, 126	wrdind 14876	. . . 4 ⊢ (𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉) → (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
128	127	com12 33	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
129	10, 128	sylbid 243	. 2 ⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝑅 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉)))
130	129	imp 412	1 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 Vcvv 3450 ⊆ wss 3895 ∖ cdif 4045 ∩ cin 4089 ∪ cun 4149 ∅c0 4278 {csn 4584 ∪ ciun 4950 ran crn 5651 ⟶wf 6535 ‘cfv 6539 (class class class)co 7421 Word cword 14662 ++ cconcat 14719 ⟨“cs1 14746 mCNcmcn 36312 mVRcmvar 36313 mRExcmrex 36318 mRSubstcmrsub 36322

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-er 8721 df-map 8853 df-pm 8854 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-card 10024 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-nn 12340 df-2 12409 df-n0 12611 df-xnn0 12684 df-z 12698 df-uz 12970 df-fz 13644 df-fzo 13793 df-seq 14149 df-hash 14479 df-word 14663 df-lsw 14712 df-concat 14720 df-s1 14747 df-substr 14794 df-pfx 14826 df-struct 17331 df-sets 17348 df-slot 17366 df-ndx 17378 df-base 17394 df-ress 17415 df-plusg 17447 df-0g 17618 df-gsum 17619 df-mgm 18822 df-sgrp 18914 df-mnd 18930 df-submnd 18985 df-frmd 19051 df-mrex 36338 df-mrsub 36342

This theorem is used by: msubvrs 36412

W3C validator