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 32807

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 2821	. . . . . 6 ⊢ (mRSubst‘𝑇) = (mRSubst‘𝑇)
3		msubvrs.s	. . . . . 6 ⊢ 𝑆 = (mSubst‘𝑇)
4	1, 2, 3	elmsubrn 32775	. . . . 5 ⊢ ran 𝑆 = ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
5	4	eleq2i 2904	. . . 4 ⊢ (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)))
6		eqid 2821	. . . . 5 ⊢ (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) = (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
7	1	fvexi 6684	. . . . . 6 ⊢ 𝐸 ∈ V
8	7	mptex 6986	. . . . 5 ⊢ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) ∈ V
9	6, 8	elrnmpti 5832	. . . 4 ⊢ (𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) ↔ ∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
10	5, 9	bitri 277	. . 3 ⊢ (𝐹 ∈ ran 𝑆 ↔ ∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
11		simp2 1133	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑓 ∈ ran (mRSubst‘𝑇))
12		simp3 1134	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑋 ∈ 𝐸)
13		eqid 2821	. . . . . . . . . . . 12 ⊢ (mTC‘𝑇) = (mTC‘𝑇)
14		eqid 2821	. . . . . . . . . . . 12 ⊢ (mREx‘𝑇) = (mREx‘𝑇)
15	13, 1, 14	mexval 32749	. . . . . . . . . . 11 ⊢ 𝐸 = ((mTC‘𝑇) × (mREx‘𝑇))
16	12, 15	eleqtrdi 2923	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
17		xp2nd 7722	. . . . . . . . . 10 ⊢ (𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
18	16, 17	syl 17	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
19		eqid 2821	. . . . . . . . . 10 ⊢ (mVR‘𝑇) = (mVR‘𝑇)
20	2, 19, 14	mrsubvrs 32769	. . . . . . . . 9 ⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ (2^nd ‘𝑋) ∈ (mREx‘𝑇)) → (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
21	11, 18, 20	syl2anc 586	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
22		fveq2 6670	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑋 → (1^st ‘𝑒) = (1^st ‘𝑋))
23		2fveq3 6675	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑋 → (𝑓‘(2^nd ‘𝑒)) = (𝑓‘(2^nd ‘𝑋)))
24	22, 23	opeq12d 4811	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑋 → ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ = ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩)
25		eqid 2821	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)
26		opex 5356	. . . . . . . . . . . 12 ⊢ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ ∈ V
27	24, 25, 26	fvmpt3i 6773	. . . . . . . . . . 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 6674	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = (𝑉‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩))
30		xp1st 7721	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (1^st ‘𝑋) ∈ (mTC‘𝑇))
31	16, 30	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (1^st ‘𝑋) ∈ (mTC‘𝑇))
32	2, 14	mrsubf 32764	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ran (mRSubst‘𝑇) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇))
33	11, 32	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇))
34	17, 15	eleq2s 2931	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ 𝐸 → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
35	12, 34	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
36	33, 35	ffvelrnd 6852	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑓‘(2^nd ‘𝑋)) ∈ (mREx‘𝑇))
37		opelxpi 5592	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑋) ∈ (mTC‘𝑇) ∧ (𝑓‘(2^nd ‘𝑋)) ∈ (mREx‘𝑇)) → ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩ ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
38	31, 36, 37	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩ ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
39	38, 15	eleqtrrdi 2924	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩ ∈ 𝐸)
40		msubvrs.v	. . . . . . . . . . 11 ⊢ 𝑉 = (mVars‘𝑇)
41	19, 1, 40	mvrsval 32752	. . . . . . . . . 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 6683	. . . . . . . . . . . . 13 ⊢ (1^st ‘𝑋) ∈ V
44		fvex 6683	. . . . . . . . . . . . 13 ⊢ (𝑓‘(2^nd ‘𝑋)) ∈ V
45	43, 44	op2nd 7698	. . . . . . . . . . . 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 5808	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ran (2^nd ‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) = ran (𝑓‘(2^nd ‘𝑋)))
48	47	ineq1d 4188	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (ran (2^nd ‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) ∩ (mVR‘𝑇)) = (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)))
49	29, 42, 48	3eqtrd 2860	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)))
50	19, 1, 40	mvrsval 32752	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝐸 → (𝑉‘𝑋) = (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)))
51	12, 50	syl 17	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘𝑋) = (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)))
52	51	iuneq1d 4946	. . . . . . . . 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 32805	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ mFS → 𝐻:(mVR‘𝑇)⟶𝐸)
55	54	3ad2ant1 1129	. . . . . . . . . . . . . . 15 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝐻:(mVR‘𝑇)⟶𝐸)
56		inss2 4206	. . . . . . . . . . . . . . . 16 ⊢ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)) ⊆ (mVR‘𝑇)
57	56	sseli 3963	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)) → 𝑥 ∈ (mVR‘𝑇))
58		ffvelrn 6849	. . . . . . . . . . . . . . 15 ⊢ ((𝐻:(mVR‘𝑇)⟶𝐸 ∧ 𝑥 ∈ (mVR‘𝑇)) → (𝐻‘𝑥) ∈ 𝐸)
59	55, 57, 58	syl2an 597	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝐻‘𝑥) ∈ 𝐸)
60		fveq2 6670	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝐻‘𝑥) → (1^st ‘𝑒) = (1^st ‘(𝐻‘𝑥)))
61		2fveq3 6675	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝐻‘𝑥) → (𝑓‘(2^nd ‘𝑒)) = (𝑓‘(2^nd ‘(𝐻‘𝑥))))
62	60, 61	opeq12d 4811	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝐻‘𝑥) → ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ = ⟨(1^st ‘(𝐻‘𝑥)), (𝑓‘(2^nd ‘(𝐻‘𝑥)))⟩)
63	62, 25, 26	fvmpt3i 6773	. . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑥 ∈ (mVR‘𝑇))
66		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (mType‘𝑇) = (mType‘𝑇)
67	19, 66, 53	mvhval 32781	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (mVR‘𝑇) → (𝐻‘𝑥) = ⟨((mType‘𝑇)‘𝑥), ⟨“𝑥”⟩⟩)
68	65, 67	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝐻‘𝑥) = ⟨((mType‘𝑇)‘𝑥), ⟨“𝑥”⟩⟩)
69		fvex 6683	. . . . . . . . . . . . . . . 16 ⊢ ((mType‘𝑇)‘𝑥) ∈ V
70		s1cli 13959	. . . . . . . . . . . . . . . . 17 ⊢ ⟨“𝑥”⟩ ∈ Word V
71	70	elexi 3513	. . . . . . . . . . . . . . . 16 ⊢ ⟨“𝑥”⟩ ∈ V
72	69, 71	op1std 7699	. . . . . . . . . . . . . . 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 7700	. . . . . . . . . . . . . . . 16 ⊢ ((𝐻‘𝑥) = ⟨((mType‘𝑇)‘𝑥), ⟨“𝑥”⟩⟩ → (2^nd ‘(𝐻‘𝑥)) = ⟨“𝑥”⟩)
75	68, 74	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (2^nd ‘(𝐻‘𝑥)) = ⟨“𝑥”⟩)
76	75	fveq2d 6674	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑓‘(2^nd ‘(𝐻‘𝑥))) = (𝑓‘⟨“𝑥”⟩))
77	73, 76	opeq12d 4811	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨(1^st ‘(𝐻‘𝑥)), (𝑓‘(2^nd ‘(𝐻‘𝑥)))⟩ = ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩)
78	64, 77	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥)) = ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩)
79	78	fveq2d 6674	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = (𝑉‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩))
80		simpl1 1187	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑇 ∈ mFS)
81	19, 13, 66	mtyf2 32798	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ mFS → (mType‘𝑇):(mVR‘𝑇)⟶(mTC‘𝑇))
82	80, 81	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (mType‘𝑇):(mVR‘𝑇)⟶(mTC‘𝑇))
83	82, 65	ffvelrnd 6852	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ((mType‘𝑇)‘𝑥) ∈ (mTC‘𝑇))
84	33	adantr 483	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇))
85		elun2 4153	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (mVR‘𝑇) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)))
86	65, 85	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)))
87	86	s1cld 13957	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨“𝑥”⟩ ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
88		eqid 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (mCN‘𝑇) = (mCN‘𝑇)
89	88, 19, 14	mrexval 32748	. . . . . . . . . . . . . . . . 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 2916	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨“𝑥”⟩ ∈ (mREx‘𝑇))
92	84, 91	ffvelrnd 6852	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑓‘⟨“𝑥”⟩) ∈ (mREx‘𝑇))
93		opelxpi 5592	. . . . . . . . . . . . . 14 ⊢ ((((mType‘𝑇)‘𝑥) ∈ (mTC‘𝑇) ∧ (𝑓‘⟨“𝑥”⟩) ∈ (mREx‘𝑇)) → ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩ ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
94	83, 92, 93	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩ ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
95	94, 15	eleqtrrdi 2924	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩ ∈ 𝐸)
96	19, 1, 40	mvrsval 32752	. . . . . . . . . . . 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 6683	. . . . . . . . . . . . . . 15 ⊢ (𝑓‘⟨“𝑥”⟩) ∈ V
99	69, 98	op2nd 7698	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = (𝑓‘⟨“𝑥”⟩)
100	99	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = (𝑓‘⟨“𝑥”⟩))
101	100	rneqd 5808	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ran (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = ran (𝑓‘⟨“𝑥”⟩))
102	101	ineq1d 4188	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (ran (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) ∩ (mVR‘𝑇)) = (ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
103	79, 97, 102	3eqtrd 2860	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = (ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
104	103	iuneq2dv 4943	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
105	52, 104	eqtrd 2856	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
106	21, 49, 105	3eqtr4d 2866	. . . . . . 7 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))))
107		fveq1 6669	. . . . . . . . 9 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝐹‘𝑋) = ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋))
108	107	fveq2d 6674	. . . . . . . 8 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑉‘(𝐹‘𝑋)) = (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)))
109		fveq1 6669	. . . . . . . . . 10 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝐹‘(𝐻‘𝑥)) = ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥)))
110	109	fveq2d 6674	. . . . . . . . 9 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑉‘(𝐹‘(𝐻‘𝑥))) = (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))))
111	110	iuneq2d 4948	. . . . . . . 8 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))))
112	108, 111	eqeq12d 2837	. . . . . . 7 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → ((𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))) ↔ (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥)))))
113	106, 112	syl5ibrcom 249	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥)))))
114	113	3expia 1117	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇)) → (𝑋 ∈ 𝐸 → (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))))
115	114	com23 86	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇)) → (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))))
116	115	rexlimdva 3284	. . 3 ⊢ (𝑇 ∈ mFS → (∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))))
117	10, 116	syl5bi 244	. 2 ⊢ (𝑇 ∈ mFS → (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))))
118	117	3imp 1107	1 ⊢ ((𝑇 ∈ mFS ∧ 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝐸) → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ∃wrex 3139 Vcvv 3494 ∪ cun 3934 ∩ cin 3935 ⟨cop 4573 ∪ ciun 4919 ↦ cmpt 5146 × cxp 5553 ran crn 5556 ⟶wf 6351 ‘cfv 6355 1^st c1st 7687 2^nd c2nd 7688 Word cword 13862 ⟨“cs1 13949 mCNcmcn 32707 mVRcmvar 32708 mTypecmty 32709 mTCcmtc 32711 mRExcmrex 32713 mExcmex 32714 mVarscmvrs 32716 mRSubstcmrsub 32717 mSubstcmsub 32718 mVHcmvh 32719 mFScmfs 32723

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 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-1st 7689 df-2nd 7690 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-oadd 8106 df-er 8289 df-map 8408 df-pm 8409 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-card 9368 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-nn 11639 df-2 11701 df-n0 11899 df-xnn0 11969 df-z 11983 df-uz 12245 df-fz 12894 df-fzo 13035 df-seq 13371 df-hash 13692 df-word 13863 df-lsw 13915 df-concat 13923 df-s1 13950 df-substr 14003 df-pfx 14033 df-struct 16485 df-ndx 16486 df-slot 16487 df-base 16489 df-sets 16490 df-ress 16491 df-plusg 16578 df-0g 16715 df-gsum 16716 df-mgm 17852 df-sgrp 17901 df-mnd 17912 df-submnd 17957 df-frmd 18014 df-mrex 32733 df-mex 32734 df-mvrs 32736 df-mrsub 32737 df-msub 32738 df-mvh 32739 df-mfs 32743

This theorem is referenced by: mclsppslem 32830

W3C validator