| 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 35533 |
. . . . 5
⊢ ran 𝑆 = ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) |
| 5 | 4 | eleq2i 2833 |
. . . 4
⊢ (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉))) |
| 6 | | eqid 2737 |
. . . . 5
⊢ (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) = (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) |
| 7 | 1 | fvexi 6920 |
. . . . . 6
⊢ 𝐸 ∈ V |
| 8 | 7 | mptex 7243 |
. . . . 5
⊢ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) ∈
V |
| 9 | 6, 8 | elrnmpti 5973 |
. . . 4
⊢ (𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) ↔ ∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) |
| 10 | 5, 9 | bitri 275 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 ↔ ∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) |
| 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 35507 |
. . . . . . . . . . 11
⊢ 𝐸 = ((mTC‘𝑇) × (mREx‘𝑇)) |
| 16 | 12, 15 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇))) |
| 17 | | xp2nd 8047 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (2nd
‘𝑋) ∈
(mREx‘𝑇)) |
| 18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2nd ‘𝑋) ∈ (mREx‘𝑇)) |
| 19 | | eqid 2737 |
. . . . . . . . . 10
⊢
(mVR‘𝑇) =
(mVR‘𝑇) |
| 20 | 2, 19, 14 | mrsubvrs 35527 |
. . . . . . . . 9
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ (2nd
‘𝑋) ∈
(mREx‘𝑇)) → (ran
(𝑓‘(2nd
‘𝑋)) ∩
(mVR‘𝑇)) = ∪ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘〈“𝑥”〉) ∩ (mVR‘𝑇))) |
| 21 | 11, 18, 20 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (ran (𝑓‘(2nd ‘𝑋)) ∩ (mVR‘𝑇)) = ∪ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))(ran (𝑓‘〈“𝑥”〉) ∩ (mVR‘𝑇))) |
| 22 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑒 = 𝑋 → (1st ‘𝑒) = (1st ‘𝑋)) |
| 23 | | 2fveq3 6911 |
. . . . . . . . . . . . 13
⊢ (𝑒 = 𝑋 → (𝑓‘(2nd ‘𝑒)) = (𝑓‘(2nd ‘𝑋))) |
| 24 | 22, 23 | opeq12d 4881 |
. . . . . . . . . . . 12
⊢ (𝑒 = 𝑋 → 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉 = 〈(1st
‘𝑋), (𝑓‘(2nd
‘𝑋))〉) |
| 25 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) |
| 26 | | opex 5469 |
. . . . . . . . . . . 12
⊢
〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉 ∈
V |
| 27 | 24, 25, 26 | fvmpt3i 7021 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐸 → ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋) = 〈(1st
‘𝑋), (𝑓‘(2nd
‘𝑋))〉) |
| 28 | 12, 27 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋) = 〈(1st
‘𝑋), (𝑓‘(2nd
‘𝑋))〉) |
| 29 | 28 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋)) = (𝑉‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉)) |
| 30 | | xp1st 8046 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (1st
‘𝑋) ∈
(mTC‘𝑇)) |
| 31 | 16, 30 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (1st ‘𝑋) ∈ (mTC‘𝑇)) |
| 32 | 2, 14 | mrsubf 35522 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ran (mRSubst‘𝑇) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇)) |
| 33 | 11, 32 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇)) |
| 34 | 17, 15 | eleq2s 2859 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ 𝐸 → (2nd ‘𝑋) ∈ (mREx‘𝑇)) |
| 35 | 12, 34 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2nd ‘𝑋) ∈ (mREx‘𝑇)) |
| 36 | 33, 35 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑓‘(2nd ‘𝑋)) ∈ (mREx‘𝑇)) |
| 37 | | opelxpi 5722 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑋) ∈ (mTC‘𝑇) ∧ (𝑓‘(2nd ‘𝑋)) ∈ (mREx‘𝑇)) → 〈(1st
‘𝑋), (𝑓‘(2nd
‘𝑋))〉 ∈
((mTC‘𝑇) ×
(mREx‘𝑇))) |
| 38 | 31, 36, 37 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉 ∈
((mTC‘𝑇) ×
(mREx‘𝑇))) |
| 39 | 38, 15 | eleqtrrdi 2852 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉 ∈ 𝐸) |
| 40 | | msubvrs.v |
. . . . . . . . . . 11
⊢ 𝑉 = (mVars‘𝑇) |
| 41 | 19, 1, 40 | mvrsval 35510 |
. . . . . . . . . 10
⊢
(〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉 ∈ 𝐸 → (𝑉‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) = (ran (2nd
‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) ∩ (mVR‘𝑇))) |
| 42 | 39, 41 | syl 17 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) = (ran (2nd
‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) ∩ (mVR‘𝑇))) |
| 43 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢
(1st ‘𝑋) ∈ V |
| 44 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (𝑓‘(2nd
‘𝑋)) ∈
V |
| 45 | 43, 44 | op2nd 8023 |
. . . . . . . . . . . 12
⊢
(2nd ‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) = (𝑓‘(2nd ‘𝑋)) |
| 46 | 45 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (2nd
‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) = (𝑓‘(2nd ‘𝑋))) |
| 47 | 46 | rneqd 5949 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ran (2nd
‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) = ran (𝑓‘(2nd
‘𝑋))) |
| 48 | 47 | ineq1d 4219 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (ran (2nd
‘〈(1st ‘𝑋), (𝑓‘(2nd ‘𝑋))〉) ∩ (mVR‘𝑇)) = (ran (𝑓‘(2nd ‘𝑋)) ∩ (mVR‘𝑇))) |
| 49 | 29, 42, 48 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋)) = (ran (𝑓‘(2nd ‘𝑋)) ∩ (mVR‘𝑇))) |
| 50 | 19, 1, 40 | mvrsval 35510 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐸 → (𝑉‘𝑋) = (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) |
| 51 | 12, 50 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘𝑋) = (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) |
| 52 | 51 | iuneq1d 5019 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))) = ∪
𝑥 ∈ (ran
(2nd ‘𝑋)
∩ (mVR‘𝑇))(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)))) |
| 53 | | msubvrs.h |
. . . . . . . . . . . . . . . . 17
⊢ 𝐻 = (mVH‘𝑇) |
| 54 | 19, 1, 53 | mvhf 35563 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ mFS → 𝐻:(mVR‘𝑇)⟶𝐸) |
| 55 | 54 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → 𝐻:(mVR‘𝑇)⟶𝐸) |
| 56 | | inss2 4238 |
. . . . . . . . . . . . . . . 16
⊢ (ran
(2nd ‘𝑋)
∩ (mVR‘𝑇))
⊆ (mVR‘𝑇) |
| 57 | 56 | sseli 3979 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (ran (2nd
‘𝑋) ∩
(mVR‘𝑇)) → 𝑥 ∈ (mVR‘𝑇)) |
| 58 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻:(mVR‘𝑇)⟶𝐸 ∧ 𝑥 ∈ (mVR‘𝑇)) → (𝐻‘𝑥) ∈ 𝐸) |
| 59 | 55, 57, 58 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝐻‘𝑥) ∈ 𝐸) |
| 60 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = (𝐻‘𝑥) → (1st ‘𝑒) = (1st
‘(𝐻‘𝑥))) |
| 61 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = (𝐻‘𝑥) → (𝑓‘(2nd ‘𝑒)) = (𝑓‘(2nd ‘(𝐻‘𝑥)))) |
| 62 | 60, 61 | opeq12d 4881 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = (𝐻‘𝑥) → 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉 = 〈(1st
‘(𝐻‘𝑥)), (𝑓‘(2nd ‘(𝐻‘𝑥)))〉) |
| 63 | 62, 25, 26 | fvmpt3i 7021 |
. . . . . . . . . . . . . 14
⊢ ((𝐻‘𝑥) ∈ 𝐸 → ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)) = 〈(1st ‘(𝐻‘𝑥)), (𝑓‘(2nd ‘(𝐻‘𝑥)))〉) |
| 64 | 59, 63 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)) = 〈(1st ‘(𝐻‘𝑥)), (𝑓‘(2nd ‘(𝐻‘𝑥)))〉) |
| 65 | 57 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑥 ∈ (mVR‘𝑇)) |
| 66 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(mType‘𝑇) =
(mType‘𝑇) |
| 67 | 19, 66, 53 | mvhval 35539 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (mVR‘𝑇) → (𝐻‘𝑥) = 〈((mType‘𝑇)‘𝑥), 〈“𝑥”〉〉) |
| 68 | 65, 67 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝐻‘𝑥) = 〈((mType‘𝑇)‘𝑥), 〈“𝑥”〉〉) |
| 69 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢
((mType‘𝑇)‘𝑥) ∈ V |
| 70 | | s1cli 14643 |
. . . . . . . . . . . . . . . . 17
⊢
〈“𝑥”〉 ∈ Word V |
| 71 | 70 | elexi 3503 |
. . . . . . . . . . . . . . . 16
⊢
〈“𝑥”〉 ∈ V |
| 72 | 69, 71 | op1std 8024 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻‘𝑥) = 〈((mType‘𝑇)‘𝑥), 〈“𝑥”〉〉 → (1st
‘(𝐻‘𝑥)) = ((mType‘𝑇)‘𝑥)) |
| 73 | 68, 72 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (1st
‘(𝐻‘𝑥)) = ((mType‘𝑇)‘𝑥)) |
| 74 | 69, 71 | op2ndd 8025 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐻‘𝑥) = 〈((mType‘𝑇)‘𝑥), 〈“𝑥”〉〉 → (2nd
‘(𝐻‘𝑥)) = 〈“𝑥”〉) |
| 75 | 68, 74 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (2nd
‘(𝐻‘𝑥)) = 〈“𝑥”〉) |
| 76 | 75 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑓‘(2nd ‘(𝐻‘𝑥))) = (𝑓‘〈“𝑥”〉)) |
| 77 | 73, 76 | opeq12d 4881 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 〈(1st
‘(𝐻‘𝑥)), (𝑓‘(2nd ‘(𝐻‘𝑥)))〉 = 〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) |
| 78 | 64, 77 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)) = 〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) |
| 79 | 78 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))) = (𝑉‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉)) |
| 80 | | simpl1 1192 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑇 ∈ mFS) |
| 81 | 19, 13, 66 | mtyf2 35556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ mFS →
(mType‘𝑇):(mVR‘𝑇)⟶(mTC‘𝑇)) |
| 82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (mType‘𝑇):(mVR‘𝑇)⟶(mTC‘𝑇)) |
| 83 | 82, 65 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → ((mType‘𝑇)‘𝑥) ∈ (mTC‘𝑇)) |
| 84 | 33 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑓:(mREx‘𝑇)⟶(mREx‘𝑇)) |
| 85 | | elun2 4183 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (mVR‘𝑇) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
| 86 | 65, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 𝑥 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
| 87 | 86 | s1cld 14641 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 〈“𝑥”〉 ∈ Word
((mCN‘𝑇) ∪
(mVR‘𝑇))) |
| 88 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(mCN‘𝑇) =
(mCN‘𝑇) |
| 89 | 88, 19, 14 | mrexval 35506 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇 ∈ mFS →
(mREx‘𝑇) = Word
((mCN‘𝑇) ∪
(mVR‘𝑇))) |
| 90 | 80, 89 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (mREx‘𝑇) = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
| 91 | 87, 90 | eleqtrrd 2844 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → 〈“𝑥”〉 ∈
(mREx‘𝑇)) |
| 92 | 84, 91 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑓‘〈“𝑥”〉) ∈ (mREx‘𝑇)) |
| 93 | | opelxpi 5722 |
. . . . . . . . . . . . . 14
⊢
((((mType‘𝑇)‘𝑥) ∈ (mTC‘𝑇) ∧ (𝑓‘〈“𝑥”〉) ∈ (mREx‘𝑇)) →
〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉 ∈ ((mTC‘𝑇) × (mREx‘𝑇))) |
| 94 | 83, 92, 93 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) →
〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉 ∈ ((mTC‘𝑇) × (mREx‘𝑇))) |
| 95 | 94, 15 | eleqtrrdi 2852 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) →
〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉 ∈ 𝐸) |
| 96 | 19, 1, 40 | mvrsval 35510 |
. . . . . . . . . . . 12
⊢
(〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉 ∈ 𝐸 → (𝑉‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) = (ran (2nd
‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) ∩ (mVR‘𝑇))) |
| 97 | 95, 96 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) = (ran (2nd
‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) ∩ (mVR‘𝑇))) |
| 98 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢ (𝑓‘〈“𝑥”〉) ∈
V |
| 99 | 69, 98 | op2nd 8023 |
. . . . . . . . . . . . . 14
⊢
(2nd ‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) = (𝑓‘〈“𝑥”〉) |
| 100 | 99 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (2nd
‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) = (𝑓‘〈“𝑥”〉)) |
| 101 | 100 | rneqd 5949 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → ran (2nd
‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) = ran (𝑓‘〈“𝑥”〉)) |
| 102 | 101 | ineq1d 4219 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (ran (2nd
‘〈((mType‘𝑇)‘𝑥), (𝑓‘〈“𝑥”〉)〉) ∩ (mVR‘𝑇)) = (ran (𝑓‘〈“𝑥”〉) ∩ (mVR‘𝑇))) |
| 103 | 79, 97, 102 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) ∧ 𝑥 ∈ (ran (2nd ‘𝑋) ∩ (mVR‘𝑇))) → (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))) = (ran (𝑓‘〈“𝑥”〉) ∩ (mVR‘𝑇))) |
| 104 | 103 | iuneq2dv 5016 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪
𝑥 ∈ (ran
(2nd ‘𝑋)
∩ (mVR‘𝑇))(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))) = ∪
𝑥 ∈ (ran
(2nd ‘𝑋)
∩ (mVR‘𝑇))(ran
(𝑓‘〈“𝑥”〉) ∩
(mVR‘𝑇))) |
| 105 | 52, 104 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))) = ∪
𝑥 ∈ (ran
(2nd ‘𝑋)
∩ (mVR‘𝑇))(ran
(𝑓‘〈“𝑥”〉) ∩
(mVR‘𝑇))) |
| 106 | 21, 49, 105 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)))) |
| 107 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝐹‘𝑋) = ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋)) |
| 108 | 107 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝑉‘(𝐹‘𝑋)) = (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋))) |
| 109 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝐹‘(𝐻‘𝑥)) = ((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))) |
| 110 | 109 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝑉‘(𝐹‘(𝐻‘𝑥))) = (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)))) |
| 111 | 110 | iuneq2d 5022 |
. . . . . . . 8
⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥)))) |
| 112 | 108, 111 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → ((𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))) ↔ (𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘((𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)‘(𝐻‘𝑥))))) |
| 113 | 106, 112 | syl5ibrcom 247 |
. . . . . 6
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑋 ∈ 𝐸) → (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))) |
| 114 | 113 | 3expia 1122 |
. . . . 5
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇)) → (𝑋 ∈ 𝐸 → (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥)))))) |
| 115 | 114 | com23 86 |
. . . 4
⊢ ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubst‘𝑇)) → (𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥)))))) |
| 116 | 115 | rexlimdva 3155 |
. . 3
⊢ (𝑇 ∈ mFS → (∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥)))))) |
| 117 | 10, 116 | biimtrid 242 |
. 2
⊢ (𝑇 ∈ mFS → (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝐸 → (𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥)))))) |
| 118 | 117 | 3imp 1111 |
1
⊢ ((𝑇 ∈ mFS ∧ 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝐸) → (𝑉‘(𝐹‘𝑋)) = ∪
𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥)))) |