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 35758

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 35726	. . . . 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 6848	. . . . . 6 ⊢ 𝐸 ∈ V
8	7	mptex 7171	. . . . 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 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 35700	. . . . . . . . . . 11 ⊢ 𝐸 = ((mTC‘𝑇) × (mREx‘𝑇))
16	12, 15	eleqtrdi 2847	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)))
17		xp2nd 7968	. . . . . . . . . 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 35720	. . . . . . . . 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 6834	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑋 → (1^st ‘𝑒) = (1^st ‘𝑋))
23		2fveq3 6839	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑋 → (𝑓‘(2^nd ‘𝑒)) = (𝑓‘(2^nd ‘𝑋)))
24	22, 23	opeq12d 4825	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑋 → ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ = ⟨(1^st ‘𝑋), (𝑓‘(2^nd ‘𝑋))⟩)
25		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)
26		opex 5411	. . . . . . . . . . . 12 ⊢ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ ∈ V
27	24, 25, 26	fvmpt3i 6947	. . . . . . . . . . 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 7967	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (1^st ‘𝑋) ∈ (mTC‘𝑇))
31	16, 30	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (1^st ‘𝑋) ∈ (mTC‘𝑇))
32	2, 14	mrsubf 35715	. . . . . . . . . . . . . 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 7031	. . . . . . . . . . . 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 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 35703	. . . . . . . . . 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 7944	. . . . . . . . . . . 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 4160	. . . . . . . . 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 35703	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝐸 → (𝑉‘𝑋) = (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)))
51	12, 50	syl 17	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘𝑋) = (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)))
52	51	iuneq1d 4962	. . . . . . . . 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 35756	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ mFS → 𝐻:(mVR‘𝑇)⟶𝐸)
55	54	3ad2ant1 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝐻:(mVR‘𝑇)⟶𝐸)
56		inss2 4179	. . . . . . . . . . . . . . . 16 ⊢ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)) ⊆ (mVR‘𝑇)
57	56	sseli 3918	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇)) → 𝑥 ∈ (mVR‘𝑇))
58		ffvelcdm 7027	. . . . . . . . . . . . . . 15 ⊢ ((𝐻:(mVR‘𝑇)⟶𝐸 ∧ 𝑥 ∈ (mVR‘𝑇)) → (𝐻‘𝑥) ∈ 𝐸)
59	55, 57, 58	syl2an 597	. . . . . . . . . . . . . 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 4825	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝐻‘𝑥) → ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ = ⟨(1^st ‘(𝐻‘𝑥)), (𝑓‘(2^nd ‘(𝐻‘𝑥)))⟩)
63	62, 25, 26	fvmpt3i 6947	. . . . . . . . . . . . . 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 35732	. . . . . . . . . . . . . . . 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 14559	. . . . . . . . . . . . . . . . 17 ⊢ ⟨“𝑥”⟩ ∈ Word V
71	70	elexi 3453	. . . . . . . . . . . . . . . 16 ⊢ ⟨“𝑥”⟩ ∈ V
72	69, 71	op1std 7945	. . . . . . . . . . . . . . 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 7946	. . . . . . . . . . . . . . . 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 4825	. . . . . . . . . . . . 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 6838	. . . . . . . . . . 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 35749	. . . . . . . . . . . . . . . 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 7031	. . . . . . . . . . . . . 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 4124	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (mVR‘𝑇) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)))
86	65, 85	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)))
87	86	s1cld 14557	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → ⟨“𝑥”⟩ ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
88		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (mCN‘𝑇) = (mCN‘𝑇)
89	88, 19, 14	mrexval 35699	. . . . . . . . . . . . . . . . 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 7031	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2^nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑓‘⟨“𝑥”⟩) ∈ (mREx‘𝑇))
93		opelxpi 5661	. . . . . . . . . . . . . 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 35703	. . . . . . . . . . . 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 7944	. . . . . . . . . . . . . 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 4160	. . . . . . . . . . 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 4959	. . . . . . . . 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 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 4965	. . . . . . . 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 3430 ∪ cun 3888 ∩ cin 3889 ⟨cop 4574 ∪ ciun 4934 ↦ cmpt 5167 × cxp 5622 ran crn 5625 ⟶wf 6488 ‘cfv 6492 1^st c1st 7933 2^nd c2nd 7934 Word cword 14466 ⟨“cs1 14549 mCNcmcn 35658 mVRcmvar 35659 mTypecmty 35660 mTCcmtc 35662 mRExcmrex 35664 mExcmex 35665 mVarscmvrs 35667 mRSubstcmrsub 35668 mSubstcmsub 35669 mVHcmvh 35670 mFScmfs 35674

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 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106

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 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 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 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-er 8636 df-map 8768 df-pm 8769 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12166 df-2 12235 df-n0 12429 df-xnn0 12502 df-z 12516 df-uz 12780 df-fz 13453 df-fzo 13600 df-seq 13955 df-hash 14284 df-word 14467 df-lsw 14516 df-concat 14524 df-s1 14550 df-substr 14595 df-pfx 14625 df-struct 17108 df-sets 17125 df-slot 17143 df-ndx 17155 df-base 17171 df-ress 17192 df-plusg 17224 df-0g 17395 df-gsum 17396 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-submnd 18743 df-frmd 18808 df-mrex 35684 df-mex 35685 df-mvrs 35687 df-mrsub 35688 df-msub 35689 df-mvh 35690 df-mfs 35694

This theorem is referenced by: mclsppslem 35781

W3C validator