Step | Hyp | Ref
| Expression |
1 | | otex 5124 |
. . . . 5
⊢
⟨((1^{st} ‘(1^{st} ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑇) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩ ∈ V |
2 | 1 | csbex 4988 |
. . . 4
⊢
⦋(2^{nd} ‘𝑠) / 𝑎⦌⟨((1^{st}
‘(1^{st} ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑇) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩ ∈ V |
3 | 2 | csbex 4988 |
. . 3
⊢
⦋(2^{nd} ‘(1^{st} ‘𝑠)) / ℎ⦌⦋(2^{nd}
‘𝑠) / 𝑎⦌⟨((1^{st}
‘(1^{st} ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑇) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩ ∈ V |
4 | | eqid 2799 |
. . . 4
⊢
(mVars‘𝑇) =
(mVars‘𝑇) |
5 | | mpstssv.p |
. . . 4
⊢ 𝑃 = (mPreSt‘𝑇) |
6 | | msrf.r |
. . . 4
⊢ 𝑅 = (mStRed‘𝑇) |
7 | 4, 5, 6 | msrfval 31951 |
. . 3
⊢ 𝑅 = (𝑠 ∈ 𝑃 ↦ ⦋(2^{nd}
‘(1^{st} ‘𝑠)) / ℎ⦌⦋(2^{nd}
‘𝑠) / 𝑎⦌⟨((1^{st}
‘(1^{st} ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑇) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩) |
8 | 3, 7 | fnmpti 6233 |
. 2
⊢ 𝑅 Fn 𝑃 |
9 | 5 | mpst123 31954 |
. . . . . 6
⊢ (𝑠 ∈ 𝑃 → 𝑠 = ⟨(1^{st}
‘(1^{st} ‘𝑠)), (2^{nd} ‘(1^{st}
‘𝑠)), (2^{nd}
‘𝑠)⟩) |
10 | 9 | fveq2d 6415 |
. . . . 5
⊢ (𝑠 ∈ 𝑃 → (𝑅‘𝑠) = (𝑅‘⟨(1^{st}
‘(1^{st} ‘𝑠)), (2^{nd} ‘(1^{st}
‘𝑠)), (2^{nd}
‘𝑠)⟩)) |
11 | | id 22 |
. . . . . . 7
⊢ (𝑠 ∈ 𝑃 → 𝑠 ∈ 𝑃) |
12 | 9, 11 | eqeltrrd 2879 |
. . . . . 6
⊢ (𝑠 ∈ 𝑃 → ⟨(1^{st}
‘(1^{st} ‘𝑠)), (2^{nd} ‘(1^{st}
‘𝑠)), (2^{nd}
‘𝑠)⟩ ∈
𝑃) |
13 | | eqid 2799 |
. . . . . . 7
⊢ ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) = ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) |
14 | 4, 5, 6, 13 | msrval 31952 |
. . . . . 6
⊢
(⟨(1^{st} ‘(1^{st} ‘𝑠)), (2^{nd} ‘(1^{st}
‘𝑠)), (2^{nd}
‘𝑠)⟩ ∈
𝑃 → (𝑅‘⟨(1^{st}
‘(1^{st} ‘𝑠)), (2^{nd} ‘(1^{st}
‘𝑠)), (2^{nd}
‘𝑠)⟩) =
⟨((1^{st} ‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))), (2^{nd}
‘(1^{st} ‘𝑠)), (2^{nd} ‘𝑠)⟩) |
15 | 12, 14 | syl 17 |
. . . . 5
⊢ (𝑠 ∈ 𝑃 → (𝑅‘⟨(1^{st}
‘(1^{st} ‘𝑠)), (2^{nd} ‘(1^{st}
‘𝑠)), (2^{nd}
‘𝑠)⟩) =
⟨((1^{st} ‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))), (2^{nd}
‘(1^{st} ‘𝑠)), (2^{nd} ‘𝑠)⟩) |
16 | 10, 15 | eqtrd 2833 |
. . . 4
⊢ (𝑠 ∈ 𝑃 → (𝑅‘𝑠) = ⟨((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))), (2^{nd}
‘(1^{st} ‘𝑠)), (2^{nd} ‘𝑠)⟩) |
17 | | inss1 4028 |
. . . . . . 7
⊢
((1^{st} ‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))) ⊆ (1^{st}
‘(1^{st} ‘𝑠)) |
18 | | eqid 2799 |
. . . . . . . . . . 11
⊢
(mDV‘𝑇) =
(mDV‘𝑇) |
19 | | eqid 2799 |
. . . . . . . . . . 11
⊢
(mEx‘𝑇) =
(mEx‘𝑇) |
20 | 18, 19, 5 | elmpst 31950 |
. . . . . . . . . 10
⊢
(⟨(1^{st} ‘(1^{st} ‘𝑠)), (2^{nd} ‘(1^{st}
‘𝑠)), (2^{nd}
‘𝑠)⟩ ∈
𝑃 ↔ (((1^{st}
‘(1^{st} ‘𝑠)) ⊆ (mDV‘𝑇) ∧ ^{◡}(1^{st} ‘(1^{st}
‘𝑠)) =
(1^{st} ‘(1^{st} ‘𝑠))) ∧ ((2^{nd}
‘(1^{st} ‘𝑠)) ⊆ (mEx‘𝑇) ∧ (2^{nd}
‘(1^{st} ‘𝑠)) ∈ Fin) ∧ (2^{nd}
‘𝑠) ∈
(mEx‘𝑇))) |
21 | 12, 20 | sylib 210 |
. . . . . . . . 9
⊢ (𝑠 ∈ 𝑃 → (((1^{st}
‘(1^{st} ‘𝑠)) ⊆ (mDV‘𝑇) ∧ ^{◡}(1^{st} ‘(1^{st}
‘𝑠)) =
(1^{st} ‘(1^{st} ‘𝑠))) ∧ ((2^{nd}
‘(1^{st} ‘𝑠)) ⊆ (mEx‘𝑇) ∧ (2^{nd}
‘(1^{st} ‘𝑠)) ∈ Fin) ∧ (2^{nd}
‘𝑠) ∈
(mEx‘𝑇))) |
22 | 21 | simp1d 1173 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝑃 → ((1^{st}
‘(1^{st} ‘𝑠)) ⊆ (mDV‘𝑇) ∧ ^{◡}(1^{st} ‘(1^{st}
‘𝑠)) =
(1^{st} ‘(1^{st} ‘𝑠)))) |
23 | 22 | simpld 489 |
. . . . . . 7
⊢ (𝑠 ∈ 𝑃 → (1^{st}
‘(1^{st} ‘𝑠)) ⊆ (mDV‘𝑇)) |
24 | 17, 23 | syl5ss 3809 |
. . . . . 6
⊢ (𝑠 ∈ 𝑃 → ((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))) ⊆ (mDV‘𝑇)) |
25 | | cnvin 5757 |
. . . . . . 7
⊢ ^{◡}((1^{st} ‘(1^{st}
‘𝑠)) ∩ (∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))) = (^{◡}(1^{st} ‘(1^{st}
‘𝑠)) ∩ ^{◡}(∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))) |
26 | 22 | simprd 490 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝑃 → ^{◡}(1^{st} ‘(1^{st}
‘𝑠)) =
(1^{st} ‘(1^{st} ‘𝑠))) |
27 | | cnvxp 5768 |
. . . . . . . . 9
⊢ ^{◡}(∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)}))) = (∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)}))) |
28 | 27 | a1i 11 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝑃 → ^{◡}(∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)}))) = (∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))) |
29 | 26, 28 | ineq12d 4013 |
. . . . . . 7
⊢ (𝑠 ∈ 𝑃 → (^{◡}(1^{st} ‘(1^{st}
‘𝑠)) ∩ ^{◡}(∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))) = ((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)}))))) |
30 | 25, 29 | syl5eq 2845 |
. . . . . 6
⊢ (𝑠 ∈ 𝑃 → ^{◡}((1^{st} ‘(1^{st}
‘𝑠)) ∩ (∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))) = ((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)}))))) |
31 | 24, 30 | jca 508 |
. . . . 5
⊢ (𝑠 ∈ 𝑃 → (((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))) ⊆ (mDV‘𝑇) ∧ ^{◡}((1^{st} ‘(1^{st}
‘𝑠)) ∩ (∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))) = ((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))))) |
32 | 21 | simp2d 1174 |
. . . . 5
⊢ (𝑠 ∈ 𝑃 → ((2^{nd}
‘(1^{st} ‘𝑠)) ⊆ (mEx‘𝑇) ∧ (2^{nd}
‘(1^{st} ‘𝑠)) ∈ Fin)) |
33 | 21 | simp3d 1175 |
. . . . 5
⊢ (𝑠 ∈ 𝑃 → (2^{nd} ‘𝑠) ∈ (mEx‘𝑇)) |
34 | 18, 19, 5 | elmpst 31950 |
. . . . 5
⊢
(⟨((1^{st} ‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))), (2^{nd}
‘(1^{st} ‘𝑠)), (2^{nd} ‘𝑠)⟩ ∈ 𝑃 ↔ ((((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))) ⊆ (mDV‘𝑇) ∧ ^{◡}((1^{st} ‘(1^{st}
‘𝑠)) ∩ (∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))) = ((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)}))))) ∧ ((2^{nd}
‘(1^{st} ‘𝑠)) ⊆ (mEx‘𝑇) ∧ (2^{nd}
‘(1^{st} ‘𝑠)) ∈ Fin) ∧ (2^{nd}
‘𝑠) ∈
(mEx‘𝑇))) |
35 | 31, 32, 33, 34 | syl3anbrc 1444 |
. . . 4
⊢ (𝑠 ∈ 𝑃 → ⟨((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))), (2^{nd}
‘(1^{st} ‘𝑠)), (2^{nd} ‘𝑠)⟩ ∈ 𝑃) |
36 | 16, 35 | eqeltrd 2878 |
. . 3
⊢ (𝑠 ∈ 𝑃 → (𝑅‘𝑠) ∈ 𝑃) |
37 | 36 | rgen 3103 |
. 2
⊢
∀𝑠 ∈
𝑃 (𝑅‘𝑠) ∈ 𝑃 |
38 | | ffnfv 6614 |
. 2
⊢ (𝑅:𝑃⟶𝑃 ↔ (𝑅 Fn 𝑃 ∧ ∀𝑠 ∈ 𝑃 (𝑅‘𝑠) ∈ 𝑃)) |
39 | 8, 37, 38 | mpbir2an 703 |
1
⊢ 𝑅:𝑃⟶𝑃 |