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 35773

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 2737	. . . . . 6 ⊢ (mRSubst‘𝑇) = (mRSubst‘𝑇)
3		msubvrs.s	. . . . . 6 ⊢ 𝑆 = (mSubst‘𝑇)
4	1, 2, 3	elmsubrn 35741	. . . . 5 ⊢ ran 𝑆 = ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
5	4	eleq2i 2829	. . . 4 ⊢ (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)))
6		eqid 2737	. . . . 5 ⊢ (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) = (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
7	1	fvexi 6856	. . . . . 6 ⊢ 𝐸 ∈ V
8	7	mptex 7179	. . . . 5 ⊢ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) ∈ V
9	6, 8	elrnmpti 5919	. . . 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 1138	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑓 ∈ ran (mRSubst‘𝑇))
12		simp3 1139	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑋 ∈ 𝐸)
13		eqid 2737	. . . . . . . . . . . 12 ⊢ (mTC‘𝑇) = (mTC‘𝑇)
14		eqid 2737	. . . . . . . . . . . 12 ⊢ (mREx‘𝑇) = (mREx‘𝑇)
15	13, 1, 14	mexval 35715	. . . . . . . . . . 11 ⊢ 𝐸 = ((mTC‘𝑇) × (mREx‘𝑇))
16	12, 15	eleqtrdi 2847	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
17		xp2nd 7976	. . . . . . . . . 10 ⊢ (𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
18	16, 17	syl 17	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
19		eqid 2737	. . . . . . . . . 10 ⊢ (mVR‘𝑇) = (mVR‘𝑇)
20	2, 19, 14	mrsubvrs 35735	. . . . . . . . 9 ⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ (2^nd ‘𝑋) ∈ (mREx‘𝑇)) → (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
21	11, 18, 20	syl2anc 585	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
22		fveq2 6842	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑋 → (1^st ‘𝑒) = (1^st ‘𝑋))
23		2fveq3 6847	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑋 → (𝑓‘(2^nd ‘𝑒)) = (𝑓‘(2^nd ‘𝑋)))
24	22, 23	opeq12d 4839	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑋 → ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ = ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩)
25		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)
26		opex 5419	. . . . . . . . . . . 12 ⊢ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ ∈ V
27	24, 25, 26	fvmpt3i 6955	. . . . . . . . . . 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 6846	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = (𝑉‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩))
30		xp1st 7975	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (1^st ‘𝑋) ∈ (mTC‘𝑇))
31	16, 30	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (1^st ‘𝑋) ∈ (mTC‘𝑇))
32	2, 14	mrsubf 35730	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ran (mRSubst‘𝑇) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇))
33	11, 32	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇))
34	17, 15	eleq2s 2855	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ 𝐸 → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
35	12, 34	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2^nd ‘𝑋) ∈ (mREx‘𝑇))
36	33, 35	ffvelcdmd 7039	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑓‘(2^nd ‘𝑋)) ∈ (mREx‘𝑇))
37		opelxpi 5669	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑋) ∈ (mTC‘𝑇) ∧ (𝑓‘(2^nd ‘𝑋)) ∈ (mREx‘𝑇)) → ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩ ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
38	31, 36, 37	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩ ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
39	38, 15	eleqtrrdi 2848	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩ ∈ 𝐸)
40		msubvrs.v	. . . . . . . . . . 11 ⊢ 𝑉 = (mVars‘𝑇)
41	19, 1, 40	mvrsval 35718	. . . . . . . . . 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 6855	. . . . . . . . . . . . 13 ⊢ (1^st ‘𝑋) ∈ V
44		fvex 6855	. . . . . . . . . . . . 13 ⊢ (𝑓‘(2^nd ‘𝑋)) ∈ V
45	43, 44	op2nd 7952	. . . . . . . . . . . 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 5895	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ran (2^nd ‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) = ran (𝑓‘(2^nd ‘𝑋)))
48	47	ineq1d 4173	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (ran (2^nd ‘⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩) ∩ (mVR‘𝑇)) = (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)))
49	29, 42, 48	3eqtrd 2776	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = (ran (𝑓‘(2^nd ‘𝑋)) ∩ (mVR‘𝑇)))
50	19, 1, 40	mvrsval 35718	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝐸 → (𝑉‘𝑋) = (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)))
51	12, 50	syl 17	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘𝑋) = (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)))
52	51	iuneq1d 4976	. . . . . . . . 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 35771	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ mFS → 𝐻:(mVR‘𝑇)⟶𝐸)
55	54	3ad2ant1 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝐻:(mVR‘𝑇)⟶𝐸)
56		inss2 4192	. . . . . . . . . . . . . . . 16 ⊢ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)) ⊆ (mVR‘𝑇)
57	56	sseli 3931	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)) → 𝑥 ∈ (mVR‘𝑇))
58		ffvelcdm 7035	. . . . . . . . . . . . . . 15 ⊢ ((𝐻:(mVR‘𝑇)⟶𝐸 ∧ 𝑥 ∈ (mVR‘𝑇)) → (𝐻‘𝑥) ∈ 𝐸)
59	55, 57, 58	syl2an 597	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝐻‘𝑥) ∈ 𝐸)
60		fveq2 6842	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝐻‘𝑥) → (1^st ‘𝑒) = (1^st ‘(𝐻‘𝑥)))
61		2fveq3 6847	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝐻‘𝑥) → (𝑓‘(2^nd ‘𝑒)) = (𝑓‘(2^nd ‘(𝐻‘𝑥))))
62	60, 61	opeq12d 4839	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝐻‘𝑥) → ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ = ⟨(1^st ‘(𝐻‘𝑥)), (𝑓‘(2^nd ‘(𝐻‘𝑥)))⟩)
63	62, 25, 26	fvmpt3i 6955	. . . . . . . . . . . . . 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 2737	. . . . . . . . . . . . . . . . 17 ⊢ (mType‘𝑇) = (mType‘𝑇)
67	19, 66, 53	mvhval 35747	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (mVR‘𝑇) → (𝐻‘𝑥) = ⟨((mType‘𝑇)‘𝑥), ⟨“𝑥”⟩⟩)
68	65, 67	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝐻‘𝑥) = ⟨((mType‘𝑇)‘𝑥), ⟨“𝑥”⟩⟩)
69		fvex 6855	. . . . . . . . . . . . . . . 16 ⊢ ((mType‘𝑇)‘𝑥) ∈ V
70		s1cli 14541	. . . . . . . . . . . . . . . . 17 ⊢ ⟨“𝑥”⟩ ∈ Word V
71	70	elexi 3465	. . . . . . . . . . . . . . . 16 ⊢ ⟨“𝑥”⟩ ∈ V
72	69, 71	op1std 7953	. . . . . . . . . . . . . . 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 7954	. . . . . . . . . . . . . . . 16 ⊢ ((𝐻‘𝑥) = ⟨((mType‘𝑇)‘𝑥), ⟨“𝑥”⟩⟩ → (2^nd ‘(𝐻‘𝑥)) = ⟨“𝑥”⟩)
75	68, 74	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (2^nd ‘(𝐻‘𝑥)) = ⟨“𝑥”⟩)
76	75	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑓‘(2^nd ‘(𝐻‘𝑥))) = (𝑓‘⟨“𝑥”⟩))
77	73, 76	opeq12d 4839	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨(1^st ‘(𝐻‘𝑥)), (𝑓‘(2^nd ‘(𝐻‘𝑥)))⟩ = ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩)
78	64, 77	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥)) = ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩)
79	78	fveq2d 6846	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = (𝑉‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩))
80		simpl1 1193	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑇 ∈ mFS)
81	19, 13, 66	mtyf2 35764	. . . . . . . . . . . . . . . 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 7039	. . . . . . . . . . . . . 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 4137	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (mVR‘𝑇) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)))
86	65, 85	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)))
87	86	s1cld 14539	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨“𝑥”⟩ ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
88		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (mCN‘𝑇) = (mCN‘𝑇)
89	88, 19, 14	mrexval 35714	. . . . . . . . . . . . . . . . 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 2840	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨“𝑥”⟩ ∈ (mREx‘𝑇))
92	84, 91	ffvelcdmd 7039	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑓‘⟨“𝑥”⟩) ∈ (mREx‘𝑇))
93		opelxpi 5669	. . . . . . . . . . . . . 14 ⊢ ((((mType‘𝑇)‘𝑥) ∈ (mTC‘𝑇) ∧ (𝑓‘⟨“𝑥”⟩) ∈ (mREx‘𝑇)) → ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩ ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
94	83, 92, 93	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩ ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
95	94, 15	eleqtrrdi 2848	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩ ∈ 𝐸)
96	19, 1, 40	mvrsval 35718	. . . . . . . . . . . 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 6855	. . . . . . . . . . . . . . 15 ⊢ (𝑓‘⟨“𝑥”⟩) ∈ V
99	69, 98	op2nd 7952	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = (𝑓‘⟨“𝑥”⟩)
100	99	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = (𝑓‘⟨“𝑥”⟩))
101	100	rneqd 5895	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ran (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) = ran (𝑓‘⟨“𝑥”⟩))
102	101	ineq1d 4173	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (ran (2^nd ‘⟨((mType‘𝑇)‘𝑥), (𝑓‘⟨“𝑥”⟩)⟩) ∩ (mVR‘𝑇)) = (ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
103	79, 97, 102	3eqtrd 2776	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = (ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
104	103	iuneq2dv 4973	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
105	52, 104	eqtrd 2772	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))) = ∪ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘⟨“𝑥”⟩) ∩ (mVR‘𝑇)))
106	21, 49, 105	3eqtr4d 2782	. . . . . . 7 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))))
107		fveq1 6841	. . . . . . . . 9 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝐹‘𝑋) = ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋))
108	107	fveq2d 6846	. . . . . . . 8 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑉‘(𝐹‘𝑋)) = (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘𝑋)))
109		fveq1 6841	. . . . . . . . . 10 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝐹‘(𝐻‘𝑥)) = ((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥)))
110	109	fveq2d 6846	. . . . . . . . 9 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑉‘(𝐹‘(𝐻‘𝑥))) = (𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))))
111	110	iuneq2d 4979	. . . . . . . 8 ⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)‘(𝐻‘𝑥))))
112	108, 111	eqeq12d 2753	. . . . . . 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 1122	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇)) → (𝑋 ∈ 𝐸 → (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))))
115	114	com23 86	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇)) → (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))))
116	115	rexlimdva 3139	. . 3 ⊢ (𝑇 ∈ mFS → (∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))))
117	10, 116	biimtrid 242	. 2 ⊢ (𝑇 ∈ mFS → (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))))
118	117	3imp 1111	1 ⊢ ((𝑇 ∈ mFS ∧ 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝐸) → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∃wrex 3062 Vcvv 3442 ∪ cun 3901 ∩ cin 3902 ⟨cop 4588 ∪ ciun 4948 ↦ cmpt 5181 × cxp 5630 ran crn 5633 ⟶wf 6496 ‘cfv 6500 1^st c1st 7941 2^nd c2nd 7942 Word cword 14448 ⟨“cs1 14531 mCNcmcn 35673 mVRcmvar 35674 mTypecmty 35675 mTCcmtc 35677 mRExcmrex 35679 mExcmex 35680 mVarscmvrs 35682 mRSubstcmrsub 35683 mSubstcmsub 35684 mVHcmvh 35685 mFScmfs 35689

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-er 8645 df-map 8777 df-pm 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-nn 12158 df-2 12220 df-n0 12414 df-xnn0 12487 df-z 12501 df-uz 12764 df-fz 13436 df-fzo 13583 df-seq 13937 df-hash 14266 df-word 14449 df-lsw 14498 df-concat 14506 df-s1 14532 df-substr 14577 df-pfx 14607 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-0g 17373 df-gsum 17374 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-submnd 18721 df-frmd 18786 df-mrex 35699 df-mex 35700 df-mvrs 35702 df-mrsub 35703 df-msub 35704 df-mvh 35705 df-mfs 35709

This theorem is referenced by: mclsppslem 35796

W3C validator