Step | Hyp | Ref
| Expression |
1 | | msubvrs.e |
. . . . . 6
⊢ 𝐸 = (mEx‘𝑇) |
2 | | eqid 2622 |
. . . . . 6
⊢
(mRSubst‘𝑇) =
(mRSubst‘𝑇) |
3 | | msubvrs.s |
. . . . . 6
⊢ 𝑆 = (mSubst‘𝑇) |
4 | 1, 2, 3 | elmsubrn 31425 |
. . . . 5
⊢ ran 𝑆 = ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) |
5 | 4 | eleq2i 2693 |
. . . 4
⊢ (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉))) |
6 | | eqid 2622 |
. . . . 5
⊢ (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) = (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) |
7 | | fvex 6201 |
. . . . . . 7
⊢
(mEx‘𝑇) ∈
V |
8 | 1, 7 | eqeltri 2697 |
. . . . . 6
⊢ 𝐸 ∈ V |
9 | 8 | mptex 6486 |
. . . . 5
⊢ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) ∈
V |
10 | 6, 9 | elrnmpti 5376 |
. . . 4
⊢ (𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) ↔ ∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) |
11 | 5, 10 | bitri 264 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 ↔ ∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) |
12 | | simp2 1062 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑓 ∈ ran (mRSubst‘𝑇)) |
13 | | simp3 1063 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑋 ∈ 𝐸) |
14 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(mTC‘𝑇) =
(mTC‘𝑇) |
15 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(mREx‘𝑇) =
(mREx‘𝑇) |
16 | 14, 1, 15 | mexval 31399 |
. . . . . . . . . . 11
⊢ 𝐸 = ((mTC‘𝑇) × (mREx‘𝑇)) |
17 | 13, 16 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇))) |
18 | | xp2nd 7199 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (2nd
‘𝑋) ∈
(mREx‘𝑇)) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2nd ‘𝑋) ∈ (mREx‘𝑇)) |
20 | | eqid 2622 |
. . . . . . . . . 10
⊢
(mVR‘𝑇) =
(mVR‘𝑇) |
21 | 2, 20, 15 | mrsubvrs 31419 |
. . . . . . . . 9
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ (2nd
‘𝑋) ∈
(mREx‘𝑇)) → (ran
(𝑓‘(2nd
‘𝑋)) ∩
(mVR‘𝑇)) = ∪ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘〈“𝑥”〉) ∩ (mVR‘𝑇))) |
22 | 12, 19, 21 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (ran (𝑓‘(2nd ‘𝑋)) ∩ (mVR‘𝑇)) = ∪ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘〈“𝑥”〉) ∩ (mVR‘𝑇))) |
23 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑒 = 𝑋 → (1st ‘𝑒) = (1st ‘𝑋)) |
24 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = 𝑋 → (2nd ‘𝑒) = (2nd ‘𝑋)) |
25 | 24 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑒 = 𝑋 → (𝑓‘(2nd ‘𝑒)) = (𝑓‘(2nd ‘𝑋))) |
26 | 23, 25 | opeq12d 4410 |
. . . . . . . . . . . 12
⊢ (𝑒 = 𝑋 → 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉 = 〈(1st
‘𝑋), (𝑓‘(2nd
‘𝑋))〉) |
27 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) |
28 | | opex 4932 |
. . . . . . . . . . . 12
⊢
〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉 ∈
V |
29 | 26, 27, 28 | fvmpt3i 6287 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐸 → ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋) = 〈(1st
‘𝑋), (𝑓‘(2nd
‘𝑋))〉) |
30 | 13, 29 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋) = 〈(1st
‘𝑋), (𝑓‘(2nd
‘𝑋))〉) |
31 | 30 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋)) = (𝑉‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉)) |
32 | | xp1st 7198 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (1st
‘𝑋) ∈
(mTC‘𝑇)) |
33 | 17, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (1st ‘𝑋) ∈ (mTC‘𝑇)) |
34 | 2, 15 | mrsubf 31414 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ran (mRSubst‘𝑇) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇)) |
35 | 12, 34 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇)) |
36 | 18, 16 | eleq2s 2719 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ 𝐸 → (2nd ‘𝑋) ∈ (mREx‘𝑇)) |
37 | 13, 36 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2nd ‘𝑋) ∈ (mREx‘𝑇)) |
38 | 35, 37 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑓‘(2nd ‘𝑋)) ∈ (mREx‘𝑇)) |
39 | | opelxpi 5148 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑋) ∈ (mTC‘𝑇) ∧ (𝑓‘(2nd ‘𝑋)) ∈ (mREx‘𝑇)) → 〈(1st
‘𝑋), (𝑓‘(2nd
‘𝑋))〉 ∈
((mTC‘𝑇) ×
(mREx‘𝑇))) |
40 | 33, 38, 39 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉 ∈
((mTC‘𝑇) ×
(mREx‘𝑇))) |
41 | 40, 16 | syl6eleqr 2712 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉 ∈ 𝐸) |
42 | | msubvrs.v |
. . . . . . . . . . 11
⊢ 𝑉 = (mVars‘𝑇) |
43 | 20, 1, 42 | mvrsval 31402 |
. . . . . . . . . 10
⊢
(〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉 ∈ 𝐸 → (𝑉‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) = (ran (2nd
‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) ∩ (mVR‘𝑇))) |
44 | 41, 43 | syl 17 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) = (ran (2nd
‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) ∩ (mVR‘𝑇))) |
45 | | fvex 6201 |
. . . . . . . . . . . . 13
⊢
(1st ‘𝑋) ∈ V |
46 | | fvex 6201 |
. . . . . . . . . . . . 13
⊢ (𝑓‘(2nd
‘𝑋)) ∈
V |
47 | 45, 46 | op2nd 7177 |
. . . . . . . . . . . 12
⊢
(2nd ‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) = (𝑓‘(2nd ‘𝑋)) |
48 | 47 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2nd
‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) = (𝑓‘(2nd ‘𝑋))) |
49 | 48 | rneqd 5353 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ran (2nd
‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) = ran (𝑓‘(2nd
‘𝑋))) |
50 | 49 | ineq1d 3813 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (ran (2nd
‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) ∩ (mVR‘𝑇)) = (ran (𝑓‘(2nd ‘𝑋)) ∩ (mVR‘𝑇))) |
51 | 31, 44, 50 | 3eqtrd 2660 |
. . . . . . . 8
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋)) = (ran (𝑓‘(2nd ‘𝑋)) ∩ (mVR‘𝑇))) |
52 | 20, 1, 42 | mvrsval 31402 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐸 → (𝑉‘𝑋) = (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) |
53 | 13, 52 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘𝑋) = (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) |
54 | 53 | iuneq1d 4545 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))) = ∪
𝑥 ∈ (ran
(2nd ‘𝑋)
∩ (mVR‘𝑇))(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)))) |
55 | | msubvrs.h |
. . . . . . . . . . . . . . . . 17
⊢ 𝐻 = (mVH‘𝑇) |
56 | 20, 1, 55 | mvhf 31455 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ mFS → 𝐻:(mVR‘𝑇)⟶𝐸) |
57 | 56 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝐻:(mVR‘𝑇)⟶𝐸) |
58 | | inss2 3834 |
. . . . . . . . . . . . . . . 16
⊢ (ran
(2nd ‘𝑋)
∩ (mVR‘𝑇))
⊆ (mVR‘𝑇) |
59 | 58 | sseli 3599 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (ran (2nd
‘𝑋) ∩
(mVR‘𝑇)) → 𝑥 ∈ (mVR‘𝑇)) |
60 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻:(mVR‘𝑇)⟶𝐸 ∧ 𝑥 ∈ (mVR‘𝑇)) → (𝐻‘𝑥) ∈ 𝐸) |
61 | 57, 59, 60 | syl2an 494 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝐻‘𝑥) ∈ 𝐸) |
62 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = (𝐻‘𝑥) → (1st ‘𝑒) = (1st
‘(𝐻‘𝑥))) |
63 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = (𝐻‘𝑥) → (2nd ‘𝑒) = (2nd
‘(𝐻‘𝑥))) |
64 | 63 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = (𝐻‘𝑥) → (𝑓‘(2nd ‘𝑒)) = (𝑓‘(2nd ‘(𝐻‘𝑥)))) |
65 | 62, 64 | opeq12d 4410 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = (𝐻‘𝑥) → 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉 = 〈(1st
‘(𝐻‘𝑥)), (𝑓‘(2nd ‘(𝐻‘𝑥)))〉) |
66 | 65, 27, 28 | fvmpt3i 6287 |
. . . . . . . . . . . . . 14
⊢ ((𝐻‘𝑥) ∈ 𝐸 → ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)) = 〈(1st ‘(𝐻‘𝑥)), (𝑓‘(2nd ‘(𝐻‘𝑥)))〉) |
67 | 61, 66 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)) = 〈(1st ‘(𝐻‘𝑥)), (𝑓‘(2nd ‘(𝐻‘𝑥)))〉) |
68 | 59 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑥 ∈ (mVR‘𝑇)) |
69 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(mType‘𝑇) =
(mType‘𝑇) |
70 | 20, 69, 55 | mvhval 31431 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (mVR‘𝑇) → (𝐻‘𝑥) = 〈((mType‘𝑇)‘𝑥), 〈“𝑥”〉〉) |
71 | 68, 70 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝐻‘𝑥) = 〈((mType‘𝑇)‘𝑥), 〈“𝑥”〉〉) |
72 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢
((mType‘𝑇)‘𝑥) ∈ V |
73 | | s1cli 13384 |
. . . . . . . . . . . . . . . . 17
⊢
〈“𝑥”〉 ∈ Word V |
74 | 73 | elexi 3213 |
. . . . . . . . . . . . . . . 16
⊢
〈“𝑥”〉 ∈ V |
75 | 72, 74 | op1std 7178 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻‘𝑥) = 〈((mType‘𝑇)‘𝑥), 〈“𝑥”〉〉 → (1st
‘(𝐻‘𝑥)) = ((mType‘𝑇)‘𝑥)) |
76 | 71, 75 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (1st
‘(𝐻‘𝑥)) = ((mType‘𝑇)‘𝑥)) |
77 | 72, 74 | op2ndd 7179 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐻‘𝑥) = 〈((mType‘𝑇)‘𝑥), 〈“𝑥”〉〉 → (2nd
‘(𝐻‘𝑥)) = 〈“𝑥”〉) |
78 | 71, 77 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (2nd
‘(𝐻‘𝑥)) = 〈“𝑥”〉) |
79 | 78 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑓‘(2nd ‘(𝐻‘𝑥))) = (𝑓‘〈“𝑥”〉)) |
80 | 76, 79 | opeq12d 4410 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 〈(1st
‘(𝐻‘𝑥)), (𝑓‘(2nd ‘(𝐻‘𝑥)))〉 = 〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) |
81 | 67, 80 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)) = 〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) |
82 | 81 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))) = (𝑉‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉)) |
83 | | simpl1 1064 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑇 ∈ mFS) |
84 | 20, 14, 69 | mtyf2 31448 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ mFS →
(mType‘𝑇):(mVR‘𝑇)⟶(mTC‘𝑇)) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (mType‘𝑇):(mVR‘𝑇)⟶(mTC‘𝑇)) |
86 | 85, 68 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → ((mType‘𝑇)‘𝑥) ∈ (mTC‘𝑇)) |
87 | 35 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇)) |
88 | | elun2 3781 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (mVR‘𝑇) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
89 | 68, 88 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
90 | 89 | s1cld 13383 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 〈“𝑥”〉 ∈ Word
((mCN‘𝑇) ∪
(mVR‘𝑇))) |
91 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(mCN‘𝑇) =
(mCN‘𝑇) |
92 | 91, 20, 15 | mrexval 31398 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇 ∈ mFS →
(mREx‘𝑇) = Word
((mCN‘𝑇) ∪
(mVR‘𝑇))) |
93 | 83, 92 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (mREx‘𝑇) = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
94 | 90, 93 | eleqtrrd 2704 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 〈“𝑥”〉 ∈
(mREx‘𝑇)) |
95 | 87, 94 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑓‘〈“𝑥”〉) ∈ (mREx‘𝑇)) |
96 | | opelxpi 5148 |
. . . . . . . . . . . . . 14
⊢
((((mType‘𝑇)‘𝑥) ∈ (mTC‘𝑇) ∧ (𝑓‘〈“𝑥”〉) ∈ (mREx‘𝑇)) →
〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉 ∈ ((mTC‘𝑇) × (mREx‘𝑇))) |
97 | 86, 95, 96 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) →
〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉 ∈ ((mTC‘𝑇) × (mREx‘𝑇))) |
98 | 97, 16 | syl6eleqr 2712 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) →
〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉 ∈ 𝐸) |
99 | 20, 1, 42 | mvrsval 31402 |
. . . . . . . . . . . 12
⊢
(〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉 ∈ 𝐸 → (𝑉‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) = (ran (2nd
‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) ∩ (mVR‘𝑇))) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) = (ran (2nd
‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) ∩ (mVR‘𝑇))) |
101 | | fvex 6201 |
. . . . . . . . . . . . . . 15
⊢ (𝑓‘〈“𝑥”〉) ∈
V |
102 | 72, 101 | op2nd 7177 |
. . . . . . . . . . . . . 14
⊢
(2nd ‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) = (𝑓‘〈“𝑥”〉) |
103 | 102 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (2nd
‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) = (𝑓‘〈“𝑥”〉)) |
104 | 103 | rneqd 5353 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → ran (2nd
‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) = ran (𝑓‘〈“𝑥”〉)) |
105 | 104 | ineq1d 3813 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (ran (2nd
‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) ∩ (mVR‘𝑇)) = (ran (𝑓‘〈“𝑥”〉) ∩ (mVR‘𝑇))) |
106 | 82, 100, 105 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))) = (ran (𝑓‘〈“𝑥”〉) ∩ (mVR‘𝑇))) |
107 | 106 | iuneq2dv 4542 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪
𝑥 ∈ (ran
(2nd ‘𝑋)
∩ (mVR‘𝑇))(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))) = ∪
𝑥 ∈ (ran
(2nd ‘𝑋)
∩ (mVR‘𝑇))(ran
(𝑓‘〈“𝑥”〉) ∩
(mVR‘𝑇))) |
108 | 54, 107 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))) = ∪
𝑥 ∈ (ran
(2nd ‘𝑋)
∩ (mVR‘𝑇))(ran
(𝑓‘〈“𝑥”〉) ∩
(mVR‘𝑇))) |
109 | 22, 51, 108 | 3eqtr4d 2666 |
. . . . . . 7
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)))) |
110 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝐹‘𝑋) = ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋)) |
111 | 110 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝑉‘(𝐹‘𝑋)) = (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋))) |
112 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝐹‘(𝐻‘𝑥)) = ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))) |
113 | 112 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝑉‘(𝐹‘(𝐻‘𝑥))) = (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)))) |
114 | 113 | iuneq2d 4547 |
. . . . . . . 8
⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)))) |
115 | 111, 114 | eqeq12d 2637 |
. . . . . . 7
⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → ((𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))) ↔ (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))))) |
116 | 109, 115 | syl5ibrcom 237 |
. . . . . 6
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))) |
117 | 116 | 3expia 1267 |
. . . . 5
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇)) → (𝑋 ∈ 𝐸 → (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥)))))) |
118 | 117 | com23 86 |
. . . 4
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇)) → (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥)))))) |
119 | 118 | rexlimdva 3031 |
. . 3
⊢ (𝑇 ∈ mFS → (∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥)))))) |
120 | 11, 119 | syl5bi 232 |
. 2
⊢ (𝑇 ∈ mFS → (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥)))))) |
121 | 120 | 3imp 1256 |
1
⊢ ((𝑇 ∈ mFS ∧ 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝐸) → (𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥)))) |