msubvrs - Mathbox for Mario Carneiro

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

Theorem msubvrs 35754

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
msubvrs.s	⊢ 𝑆 = (mSubst‘𝑇)
msubvrs.e	⊢ 𝐸 = (mEx‘𝑇)
msubvrs.v	⊢ 𝑉 = (mVars‘𝑇)
msubvrs.h	⊢ 𝐻 = (mVH‘𝑇)

**Assertion**
Ref	Expression
msubvrs	⊢ ((𝑇 ∈ mFS ∧ 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝐸) → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))

Distinct variable groups: 𝑥,𝐸 𝑥,𝐹 𝑥,𝑇 𝑥,𝑋 𝑥,𝑉 Allowed substitution hints: 𝑆(𝑥) 𝐻(𝑥)

Proof of Theorem msubvrs Dummy variables 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		msubvrs.e	. . . . . 6 ⊢ 𝐸 = (mEx‘𝑇)
2		eqid 2736	. . . . . 6 ⊢ (mRSubst‘𝑇) = (mRSubst‘𝑇)
3		msubvrs.s	. . . . . 6 ⊢ 𝑆 = (mSubst‘𝑇)
4	1, 2, 3	elmsubrn 35722	. . . . 5 ⊢ ran 𝑆 = ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
5	4	eleq2i 2828	. . . 4 ⊢ (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)))
6		eqid 2736	. . . . 5 ⊢ (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) = (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
7	1	fvexi 6848	. . . . . 6 ⊢ 𝐸 ∈ V
8	7	mptex 7169	. . . . 5 ⊢ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) ∈ V
9	6, 8	elrnmpti 5911	. . . 4 ⊢ (𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) ↔ ∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
10	5, 9	bitri 275	. . 3 ⊢ (𝐹 ∈ ran 𝑆 ↔ ∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
11		simp2 1137	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑓 ∈ ran (mRSubst‘𝑇))
12		simp3 1138	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑋 ∈ 𝐸)
13		eqid 2736	. . . . . . . . . . . 12 ⊢ (mTC‘𝑇) = (mTC‘𝑇)
14		eqid 2736	. . . . . . . . . . . 12 ⊢ (mREx‘𝑇) = (mREx‘𝑇)
15	13, 1, 14	mexval 35696	. . . . . . . . . . 11 ⊢ 𝐸 = ((mTC‘𝑇) × (mREx‘𝑇))
16	12, 15	eleqtrdi 2846	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
17		xp2nd 7966	. . . . . . . . . 10 ⊢ (𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
18	16, 17	syl 17	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
19		eqid 2736	. . . . . . . . . 10 ⊢ (mVR‘𝑇) = (mVR‘𝑇)
20	2, 19, 14	mrsubvrs 35716	. . . . . . . . 9 ⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ (2^nd ‘𝑋) ∈ (mREx‘𝑇)) → (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
21	11, 18, 20	syl2anc 584	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
22		fveq2 6834	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑋 → (1^st ‘𝑒) = (1^st ‘𝑋))
23		2fveq3 6839	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑋 → (𝑓‘(2^nd ‘𝑒)) = (𝑓‘(2^nd ‘𝑋)))
24	22, 23	opeq12d 4837	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑋 → ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ = ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩)
25		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)
26		opex 5412	. . . . . . . . . . . 12 ⊢ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ ∈ V
27	24, 25, 26	fvmpt3i 6946	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝐸 → ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋) = ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩)
28	12, 27	syl 17	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋) = ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩)
29	28	fveq2d 6838	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = (𝑉‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩))
30		xp1st 7965	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (1^st ‘𝑋) ∈ (mTC‘𝑇))
31	16, 30	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (1^st ‘𝑋) ∈ (mTC‘𝑇))
32	2, 14	mrsubf 35711	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ran (mRSubst‘𝑇) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇))
33	11, 32	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇))
34	17, 15	eleq2s 2854	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ 𝐸 → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
35	12, 34	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
36	33, 35	ffvelcdmd 7030	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑓‘(2^nd ‘𝑋)) ∈ (mREx‘𝑇))
37		opelxpi 5661	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑋) ∈ (mTC‘𝑇) ∧ (𝑓‘(2^nd ‘𝑋)) ∈ (mREx‘𝑇)) → ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩ ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
38	31, 36, 37	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩ ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
39	38, 15	eleqtrrdi 2847	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩ ∈ 𝐸)
40		msubvrs.v	. . . . . . . . . . 11 ⊢ 𝑉 = (mVars‘𝑇)
41	19, 1, 40	mvrsval 35699	. . . . . . . . . 10 ⊢ (⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩ ∈ 𝐸 → (𝑉‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) = (ran (2^nd ‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) ∩ (mVR‘𝑇)))
42	39, 41	syl 17	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) = (ran (2^nd ‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) ∩ (mVR‘𝑇)))
43		fvex 6847	. . . . . . . . . . . . 13 ⊢ (1^st ‘𝑋) ∈ V
44		fvex 6847	. . . . . . . . . . . . 13 ⊢ (𝑓‘(2^nd ‘𝑋)) ∈ V
45	43, 44	op2nd 7942	. . . . . . . . . . . 12 ⊢ (2^nd ‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) = (𝑓‘(2^nd ‘𝑋))
46	45	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2^nd ‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) = (𝑓‘(2^nd ‘𝑋)))
47	46	rneqd 5887	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ran (2^nd ‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) = ran (𝑓‘(2^nd ‘𝑋)))
48	47	ineq1d 4171	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (ran (2^nd ‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) ∩ (mVR‘𝑇)) = (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)))
49	29, 42, 48	3eqtrd 2775	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)))
50	19, 1, 40	mvrsval 35699	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝐸 → (𝑉‘𝑋) = (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)))
51	12, 50	syl 17	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘𝑋) = (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)))
52	51	iuneq1d 4974	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))))
53		msubvrs.h	. . . . . . . . . . . . . . . . 17 ⊢ 𝐻 = (mVH‘𝑇)
54	19, 1, 53	mvhf 35752	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ mFS → 𝐻:(mVR‘𝑇)⟶𝐸)
55	54	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝐻:(mVR‘𝑇)⟶𝐸)
56		inss2 4190	. . . . . . . . . . . . . . . 16 ⊢ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)) ⊆ (mVR‘𝑇)
57	56	sseli 3929	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)) → 𝑥 ∈ (mVR‘𝑇))
58		ffvelcdm 7026	. . . . . . . . . . . . . . 15 ⊢ ((𝐻:(mVR‘𝑇)⟶𝐸 ∧ 𝑥 ∈ (mVR‘𝑇)) → (𝐻‘𝑥) ∈ 𝐸)
59	55, 57, 58	syl2an 596	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝐻‘𝑥) ∈ 𝐸)
60		fveq2 6834	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝐻‘𝑥) → (1^st ‘𝑒) = (1^st ‘(𝐻‘𝑥)))
61		2fveq3 6839	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝐻‘𝑥) → (𝑓‘(2^nd ‘𝑒)) = (𝑓‘(2^nd ‘(𝐻‘𝑥))))
62	60, 61	opeq12d 4837	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝐻‘𝑥) → ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ = ⟨(1^st ‘(𝐻‘𝑥)), (𝑓‘(2^nd ‘(𝐻‘𝑥)))⟩)
63	62, 25, 26	fvmpt3i 6946	. . . . . . . . . . . . . 14 ⊢ ((𝐻‘𝑥) ∈ 𝐸 → ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥)) = ⟨(1^st ‘(𝐻‘𝑥)), (𝑓‘(2^nd ‘(𝐻‘𝑥)))⟩)
64	59, 63	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥)) = ⟨(1^st ‘(𝐻‘𝑥)), (𝑓‘(2^nd ‘(𝐻‘𝑥)))⟩)
65	57	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑥 ∈ (mVR‘𝑇))
66		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (mType‘𝑇) = (mType‘𝑇)
67	19, 66, 53	mvhval 35728	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (mVR‘𝑇) → (𝐻‘𝑥) = ⟨((mType‘𝑇)‘𝑥), ⟨“𝑥”⟩⟩)
68	65, 67	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝐻‘𝑥) = ⟨((mType‘𝑇)‘𝑥), ⟨“𝑥”⟩⟩)
69		fvex 6847	. . . . . . . . . . . . . . . 16 ⊢ ((mType‘𝑇)‘𝑥) ∈ V
70		s1cli 14529	. . . . . . . . . . . . . . . . 17 ⊢ ⟨“𝑥”⟩ ∈ Word V
71	70	elexi 3463	. . . . . . . . . . . . . . . 16 ⊢ ⟨“𝑥”⟩ ∈ V
72	69, 71	op1std 7943	. . . . . . . . . . . . . . 15 ⊢ ((𝐻‘𝑥) = ⟨((mType‘𝑇)‘𝑥), ⟨“𝑥”⟩⟩ → (1^st ‘(𝐻‘𝑥)) = ((mType‘𝑇)‘𝑥))
73	68, 72	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (1^st ‘(𝐻‘𝑥)) = ((mType‘𝑇)‘𝑥))
74	69, 71	op2ndd 7944	. . . . . . . . . . . . . . . 16 ⊢ ((𝐻‘𝑥) = ⟨((mType‘𝑇)‘𝑥), ⟨“𝑥”⟩⟩ → (2^nd ‘(𝐻‘𝑥)) = ⟨“𝑥”⟩)
75	68, 74	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (2^nd ‘(𝐻‘𝑥)) = ⟨“𝑥”⟩)
76	75	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑓‘(2^nd ‘(𝐻‘𝑥))) = (𝑓‘⟨“𝑥”⟩))
77	73, 76	opeq12d 4837	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨(1^st ‘(𝐻‘𝑥)), (𝑓‘(2^nd ‘(𝐻‘𝑥)))⟩ = ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩)
78	64, 77	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥)) = ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩)
79	78	fveq2d 6838	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = (𝑉‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩))
80		simpl1 1192	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑇 ∈ mFS)
81	19, 13, 66	mtyf2 35745	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ mFS → (mType‘𝑇):(mVR‘𝑇)⟶(mTC‘𝑇))
82	80, 81	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (mType‘𝑇):(mVR‘𝑇)⟶(mTC‘𝑇))
83	82, 65	ffvelcdmd 7030	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ((mType‘𝑇)‘𝑥) ∈ (mTC‘𝑇))
84	33	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇))
85		elun2 4135	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (mVR‘𝑇) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)))
86	65, 85	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)))
87	86	s1cld 14527	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨“𝑥”⟩ ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
88		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (mCN‘𝑇) = (mCN‘𝑇)
89	88, 19, 14	mrexval 35695	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ∈ mFS → (mREx‘𝑇) = Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
90	80, 89	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (mREx‘𝑇) = Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
91	87, 90	eleqtrrd 2839	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨“𝑥”⟩ ∈ (mREx‘𝑇))
92	84, 91	ffvelcdmd 7030	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑓‘⟨“𝑥”⟩) ∈ (mREx‘𝑇))
93		opelxpi 5661	. . . . . . . . . . . . . 14 ⊢ ((((mType‘𝑇)‘𝑥) ∈ (mTC‘𝑇) ∧ (𝑓‘⟨“𝑥”⟩) ∈ (mREx‘𝑇)) → ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩ ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
94	83, 92, 93	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩ ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
95	94, 15	eleqtrrdi 2847	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩ ∈ 𝐸)
96	19, 1, 40	mvrsval 35699	. . . . . . . . . . . 12 ⊢ (⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩ ∈ 𝐸 → (𝑉‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = (ran (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) ∩ (mVR‘𝑇)))
97	95, 96	syl 17	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = (ran (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) ∩ (mVR‘𝑇)))
98		fvex 6847	. . . . . . . . . . . . . . 15 ⊢ (𝑓‘⟨“𝑥”⟩) ∈ V
99	69, 98	op2nd 7942	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = (𝑓‘⟨“𝑥”⟩)
100	99	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = (𝑓‘⟨“𝑥”⟩))
101	100	rneqd 5887	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ran (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = ran (𝑓‘⟨“𝑥”⟩))
102	101	ineq1d 4171	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (ran (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) ∩ (mVR‘𝑇)) = (ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
103	79, 97, 102	3eqtrd 2775	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = (ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
104	103	iuneq2dv 4971	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
105	52, 104	eqtrd 2771	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
106	21, 49, 105	3eqtr4d 2781	. . . . . . 7 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))))
107		fveq1 6833	. . . . . . . . 9 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝐹‘𝑋) = ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋))
108	107	fveq2d 6838	. . . . . . . 8 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑉‘(𝐹‘𝑋)) = (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)))
109		fveq1 6833	. . . . . . . . . 10 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝐹‘(𝐻‘𝑥)) = ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥)))
110	109	fveq2d 6838	. . . . . . . . 9 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑉‘(𝐹‘(𝐻‘𝑥))) = (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))))
111	110	iuneq2d 4977	. . . . . . . 8 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))))
112	108, 111	eqeq12d 2752	. . . . . . 7 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → ((𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))) ↔ (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥)))))
113	106, 112	syl5ibrcom 247	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥)))))
114	113	3expia 1121	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇)) → (𝑋 ∈ 𝐸 → (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))))
115	114	com23 86	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇)) → (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))))
116	115	rexlimdva 3137	. . 3 ⊢ (𝑇 ∈ mFS → (∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))))
117	10, 116	biimtrid 242	. 2 ⊢ (𝑇 ∈ mFS → (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))))
118	117	3imp 1110	1 ⊢ ((𝑇 ∈ mFS ∧ 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝐸) → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ∃wrex 3060 Vcvv 3440 ∪ cun 3899 ∩ cin 3900 ⟨cop 4586 ∪ ciun 4946 ↦ cmpt 5179 × cxp 5622 ran crn 5625 ⟶wf 6488 ‘cfv 6492 1^st c1st 7931 2^nd c2nd 7932 Word cword 14436 ⟨“cs1 14519 mCNcmcn 35654 mVRcmvar 35655 mTypecmty 35656 mTCcmtc 35658 mRExcmrex 35660 mExcmex 35661 mVarscmvrs 35663 mRSubstcmrsub 35664 mSubstcmsub 35665 mVHcmvh 35666 mFScmfs 35670

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 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 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-er 8635 df-map 8765 df-pm 8766 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-card 9851 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-nn 12146 df-2 12208 df-n0 12402 df-xnn0 12475 df-z 12489 df-uz 12752 df-fz 13424 df-fzo 13571 df-seq 13925 df-hash 14254 df-word 14437 df-lsw 14486 df-concat 14494 df-s1 14520 df-substr 14565 df-pfx 14595 df-struct 17074 df-sets 17091 df-slot 17109 df-ndx 17121 df-base 17137 df-ress 17158 df-plusg 17190 df-0g 17361 df-gsum 17362 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-submnd 18709 df-frmd 18774 df-mrex 35680 df-mex 35681 df-mvrs 35683 df-mrsub 35684 df-msub 35685 df-mvh 35686 df-mfs 35690

This theorem is referenced by: mclsppslem 35777

W3C validator