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 35592

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 2731	. . . . . 6 ⊢ (mRSubst‘𝑇) = (mRSubst‘𝑇)
3		msubvrs.s	. . . . . 6 ⊢ 𝑆 = (mSubst‘𝑇)
4	1, 2, 3	elmsubrn 35560	. . . . 5 ⊢ ran 𝑆 = ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
5	4	eleq2i 2823	. . . 4 ⊢ (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)))
6		eqid 2731	. . . . 5 ⊢ (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) = (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
7	1	fvexi 6836	. . . . . 6 ⊢ 𝐸 ∈ V
8	7	mptex 7157	. . . . 5 ⊢ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) ∈ V
9	6, 8	elrnmpti 5902	. . . 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 2731	. . . . . . . . . . . 12 ⊢ (mTC‘𝑇) = (mTC‘𝑇)
14		eqid 2731	. . . . . . . . . . . 12 ⊢ (mREx‘𝑇) = (mREx‘𝑇)
15	13, 1, 14	mexval 35534	. . . . . . . . . . 11 ⊢ 𝐸 = ((mTC‘𝑇) × (mREx‘𝑇))
16	12, 15	eleqtrdi 2841	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
17		xp2nd 7954	. . . . . . . . . 10 ⊢ (𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
18	16, 17	syl 17	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
19		eqid 2731	. . . . . . . . . 10 ⊢ (mVR‘𝑇) = (mVR‘𝑇)
20	2, 19, 14	mrsubvrs 35554	. . . . . . . . 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 6822	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑋 → (1^st ‘𝑒) = (1^st ‘𝑋))
23		2fveq3 6827	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑋 → (𝑓‘(2^nd ‘𝑒)) = (𝑓‘(2^nd ‘𝑋)))
24	22, 23	opeq12d 4833	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑋 → ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ = ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩)
25		eqid 2731	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)
26		opex 5404	. . . . . . . . . . . 12 ⊢ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ ∈ V
27	24, 25, 26	fvmpt3i 6934	. . . . . . . . . . 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 6826	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = (𝑉‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩))
30		xp1st 7953	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (1^st ‘𝑋) ∈ (mTC‘𝑇))
31	16, 30	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (1^st ‘𝑋) ∈ (mTC‘𝑇))
32	2, 14	mrsubf 35549	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ran (mRSubst‘𝑇) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇))
33	11, 32	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇))
34	17, 15	eleq2s 2849	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ 𝐸 → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
35	12, 34	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
36	33, 35	ffvelcdmd 7018	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑓‘(2^nd ‘𝑋)) ∈ (mREx‘𝑇))
37		opelxpi 5653	. . . . . . . . . . . 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 2842	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩ ∈ 𝐸)
40		msubvrs.v	. . . . . . . . . . 11 ⊢ 𝑉 = (mVars‘𝑇)
41	19, 1, 40	mvrsval 35537	. . . . . . . . . 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 6835	. . . . . . . . . . . . 13 ⊢ (1^st ‘𝑋) ∈ V
44		fvex 6835	. . . . . . . . . . . . 13 ⊢ (𝑓‘(2^nd ‘𝑋)) ∈ V
45	43, 44	op2nd 7930	. . . . . . . . . . . 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 5878	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ran (2^nd ‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) = ran (𝑓‘(2^nd ‘𝑋)))
48	47	ineq1d 4169	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (ran (2^nd ‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) ∩ (mVR‘𝑇)) = (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)))
49	29, 42, 48	3eqtrd 2770	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)))
50	19, 1, 40	mvrsval 35537	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝐸 → (𝑉‘𝑋) = (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)))
51	12, 50	syl 17	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘𝑋) = (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)))
52	51	iuneq1d 4969	. . . . . . . . 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 35590	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ mFS → 𝐻:(mVR‘𝑇)⟶𝐸)
55	54	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝐻:(mVR‘𝑇)⟶𝐸)
56		inss2 4188	. . . . . . . . . . . . . . . 16 ⊢ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)) ⊆ (mVR‘𝑇)
57	56	sseli 3930	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)) → 𝑥 ∈ (mVR‘𝑇))
58		ffvelcdm 7014	. . . . . . . . . . . . . . 15 ⊢ ((𝐻:(mVR‘𝑇)⟶𝐸 ∧ 𝑥 ∈ (mVR‘𝑇)) → (𝐻‘𝑥) ∈ 𝐸)
59	55, 57, 58	syl2an 596	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝐻‘𝑥) ∈ 𝐸)
60		fveq2 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝐻‘𝑥) → (1^st ‘𝑒) = (1^st ‘(𝐻‘𝑥)))
61		2fveq3 6827	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝐻‘𝑥) → (𝑓‘(2^nd ‘𝑒)) = (𝑓‘(2^nd ‘(𝐻‘𝑥))))
62	60, 61	opeq12d 4833	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝐻‘𝑥) → ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ = ⟨(1^st ‘(𝐻‘𝑥)), (𝑓‘(2^nd ‘(𝐻‘𝑥)))⟩)
63	62, 25, 26	fvmpt3i 6934	. . . . . . . . . . . . . 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 2731	. . . . . . . . . . . . . . . . 17 ⊢ (mType‘𝑇) = (mType‘𝑇)
67	19, 66, 53	mvhval 35566	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (mVR‘𝑇) → (𝐻‘𝑥) = ⟨((mType‘𝑇)‘𝑥), ⟨“𝑥”⟩⟩)
68	65, 67	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝐻‘𝑥) = ⟨((mType‘𝑇)‘𝑥), ⟨“𝑥”⟩⟩)
69		fvex 6835	. . . . . . . . . . . . . . . 16 ⊢ ((mType‘𝑇)‘𝑥) ∈ V
70		s1cli 14510	. . . . . . . . . . . . . . . . 17 ⊢ ⟨“𝑥”⟩ ∈ Word V
71	70	elexi 3459	. . . . . . . . . . . . . . . 16 ⊢ ⟨“𝑥”⟩ ∈ V
72	69, 71	op1std 7931	. . . . . . . . . . . . . . 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 7932	. . . . . . . . . . . . . . . 16 ⊢ ((𝐻‘𝑥) = ⟨((mType‘𝑇)‘𝑥), ⟨“𝑥”⟩⟩ → (2^nd ‘(𝐻‘𝑥)) = ⟨“𝑥”⟩)
75	68, 74	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (2^nd ‘(𝐻‘𝑥)) = ⟨“𝑥”⟩)
76	75	fveq2d 6826	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑓‘(2^nd ‘(𝐻‘𝑥))) = (𝑓‘⟨“𝑥”⟩))
77	73, 76	opeq12d 4833	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨(1^st ‘(𝐻‘𝑥)), (𝑓‘(2^nd ‘(𝐻‘𝑥)))⟩ = ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩)
78	64, 77	eqtrd 2766	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥)) = ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩)
79	78	fveq2d 6826	. . . . . . . . . . 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 35583	. . . . . . . . . . . . . . . 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 7018	. . . . . . . . . . . . . 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 4133	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (mVR‘𝑇) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)))
86	65, 85	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)))
87	86	s1cld 14508	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨“𝑥”⟩ ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
88		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (mCN‘𝑇) = (mCN‘𝑇)
89	88, 19, 14	mrexval 35533	. . . . . . . . . . . . . . . . 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 2834	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨“𝑥”⟩ ∈ (mREx‘𝑇))
92	84, 91	ffvelcdmd 7018	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑓‘⟨“𝑥”⟩) ∈ (mREx‘𝑇))
93		opelxpi 5653	. . . . . . . . . . . . . 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 2842	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩ ∈ 𝐸)
96	19, 1, 40	mvrsval 35537	. . . . . . . . . . . 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 6835	. . . . . . . . . . . . . . 15 ⊢ (𝑓‘⟨“𝑥”⟩) ∈ V
99	69, 98	op2nd 7930	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = (𝑓‘⟨“𝑥”⟩)
100	99	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = (𝑓‘⟨“𝑥”⟩))
101	100	rneqd 5878	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ran (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = ran (𝑓‘⟨“𝑥”⟩))
102	101	ineq1d 4169	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (ran (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) ∩ (mVR‘𝑇)) = (ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
103	79, 97, 102	3eqtrd 2770	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = (ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
104	103	iuneq2dv 4966	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
105	52, 104	eqtrd 2766	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
106	21, 49, 105	3eqtr4d 2776	. . . . . . 7 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))))
107		fveq1 6821	. . . . . . . . 9 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝐹‘𝑋) = ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋))
108	107	fveq2d 6826	. . . . . . . 8 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑉‘(𝐹‘𝑋)) = (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)))
109		fveq1 6821	. . . . . . . . . 10 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝐹‘(𝐻‘𝑥)) = ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥)))
110	109	fveq2d 6826	. . . . . . . . 9 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑉‘(𝐹‘(𝐻‘𝑥))) = (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))))
111	110	iuneq2d 4972	. . . . . . . 8 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))))
112	108, 111	eqeq12d 2747	. . . . . . 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 3133	. . 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 2111 ∃wrex 3056 Vcvv 3436 ∪ cun 3900 ∩ cin 3901 ⟨cop 4582 ∪ ciun 4941 ↦ cmpt 5172 × cxp 5614 ran crn 5617 ⟶wf 6477 ‘cfv 6481 1^st c1st 7919 2^nd c2nd 7920 Word cword 14417 ⟨“cs1 14500 mCNcmcn 35492 mVRcmvar 35493 mTypecmty 35494 mTCcmtc 35496 mRExcmrex 35498 mExcmex 35499 mVarscmvrs 35501 mRSubstcmrsub 35502 mSubstcmsub 35503 mVHcmvh 35504 mFScmfs 35508

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 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-cnex 11059 ax-resscn 11060 ax-1cn 11061 ax-icn 11062 ax-addcl 11063 ax-addrcl 11064 ax-mulcl 11065 ax-mulrcl 11066 ax-mulcom 11067 ax-addass 11068 ax-mulass 11069 ax-distr 11070 ax-i2m1 11071 ax-1ne0 11072 ax-1rid 11073 ax-rnegex 11074 ax-rrecex 11075 ax-cnre 11076 ax-pre-lttri 11077 ax-pre-lttrn 11078 ax-pre-ltadd 11079 ax-pre-mulgt0 11080

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 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-int 4898 df-iun 4943 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-er 8622 df-map 8752 df-pm 8753 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-card 9829 df-pnf 11145 df-mnf 11146 df-xr 11147 df-ltxr 11148 df-le 11149 df-sub 11343 df-neg 11344 df-nn 12123 df-2 12185 df-n0 12379 df-xnn0 12452 df-z 12466 df-uz 12730 df-fz 13405 df-fzo 13552 df-seq 13906 df-hash 14235 df-word 14418 df-lsw 14467 df-concat 14475 df-s1 14501 df-substr 14546 df-pfx 14576 df-struct 17055 df-sets 17072 df-slot 17090 df-ndx 17102 df-base 17118 df-ress 17139 df-plusg 17171 df-0g 17342 df-gsum 17343 df-mgm 18545 df-sgrp 18624 df-mnd 18640 df-submnd 18689 df-frmd 18754 df-mrex 35518 df-mex 35519 df-mvrs 35521 df-mrsub 35522 df-msub 35523 df-mvh 35524 df-mfs 35528

This theorem is referenced by: mclsppslem 35615

W3C validator