Step | Hyp | Ref
| Expression |
1 | | eqid 2825 |
. . . . 5
⊢
(mPreSt‘𝑇) =
(mPreSt‘𝑇) |
2 | | mstaval.r |
. . . . 5
⊢ 𝑅 = (mStRed‘𝑇) |
3 | 1, 2 | msrf 31985 |
. . . 4
⊢ 𝑅:(mPreSt‘𝑇)⟶(mPreSt‘𝑇) |
4 | | ffn 6278 |
. . . 4
⊢ (𝑅:(mPreSt‘𝑇)⟶(mPreSt‘𝑇) → 𝑅 Fn (mPreSt‘𝑇)) |
5 | | fvelrnb 6490 |
. . . 4
⊢ (𝑅 Fn (mPreSt‘𝑇) → (𝑋 ∈ ran 𝑅 ↔ ∃𝑠 ∈ (mPreSt‘𝑇)(𝑅‘𝑠) = 𝑋)) |
6 | 3, 4, 5 | mp2b 10 |
. . 3
⊢ (𝑋 ∈ ran 𝑅 ↔ ∃𝑠 ∈ (mPreSt‘𝑇)(𝑅‘𝑠) = 𝑋) |
7 | 1 | mpst123 31983 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (mPreSt‘𝑇) → 𝑠 = ⟨(1^{st}
‘(1^{st} ‘𝑠)), (2^{nd} ‘(1^{st}
‘𝑠)), (2^{nd}
‘𝑠)⟩) |
8 | 7 | fveq2d 6437 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (mPreSt‘𝑇) → (𝑅‘𝑠) = (𝑅‘⟨(1^{st}
‘(1^{st} ‘𝑠)), (2^{nd} ‘(1^{st}
‘𝑠)), (2^{nd}
‘𝑠)⟩)) |
9 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (mPreSt‘𝑇) → 𝑠 ∈ (mPreSt‘𝑇)) |
10 | 7, 9 | eqeltrrd 2907 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (mPreSt‘𝑇) → ⟨(1^{st}
‘(1^{st} ‘𝑠)), (2^{nd} ‘(1^{st}
‘𝑠)), (2^{nd}
‘𝑠)⟩ ∈
(mPreSt‘𝑇)) |
11 | | eqid 2825 |
. . . . . . . . . . . 12
⊢
(mVars‘𝑇) =
(mVars‘𝑇) |
12 | | eqid 2825 |
. . . . . . . . . . . 12
⊢ ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) = ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) |
13 | 11, 1, 2, 12 | msrval 31981 |
. . . . . . . . . . 11
⊢
(⟨(1^{st} ‘(1^{st} ‘𝑠)), (2^{nd} ‘(1^{st}
‘𝑠)), (2^{nd}
‘𝑠)⟩ ∈
(mPreSt‘𝑇) →
(𝑅‘⟨(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} ‘𝑠)⟩) |
14 | 10, 13 | syl 17 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (mPreSt‘𝑇) → (𝑅‘⟨(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 | 8, 14 | eqtrd 2861 |
. . . . . . . . 9
⊢ (𝑠 ∈ (mPreSt‘𝑇) → (𝑅‘𝑠) = ⟨((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 | 3 | ffvelrni 6607 |
. . . . . . . . 9
⊢ (𝑠 ∈ (mPreSt‘𝑇) → (𝑅‘𝑠) ∈ (mPreSt‘𝑇)) |
17 | 15, 16 | eqeltrrd 2907 |
. . . . . . . 8
⊢ (𝑠 ∈ (mPreSt‘𝑇) → ⟨((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))), (2^{nd}
‘(1^{st} ‘𝑠)), (2^{nd} ‘𝑠)⟩ ∈ (mPreSt‘𝑇)) |
18 | 11, 1, 2, 12 | msrval 31981 |
. . . . . . . 8
⊢
(⟨((1^{st} ‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))), (2^{nd}
‘(1^{st} ‘𝑠)), (2^{nd} ‘𝑠)⟩ ∈ (mPreSt‘𝑇) → (𝑅‘⟨((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} ‘𝑠)})))) ∩ (∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))), (2^{nd}
‘(1^{st} ‘𝑠)), (2^{nd} ‘𝑠)⟩) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ (𝑠 ∈ (mPreSt‘𝑇) → (𝑅‘⟨((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} ‘𝑠)})))) ∩ (∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))), (2^{nd}
‘(1^{st} ‘𝑠)), (2^{nd} ‘𝑠)⟩) |
20 | | inass 4048 |
. . . . . . . . . 10
⊢
(((1^{st} ‘(1^{st} ‘𝑠)) ∩ (∪
((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} ‘𝑠)})))) = ((1^{st}
‘(1^{st} ‘𝑠)) ∩ ((∪
((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} ‘𝑠)}))))) |
21 | | inidm 4047 |
. . . . . . . . . . 11
⊢ ((∪ ((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} ‘𝑠)})))) = (∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)}))) |
22 | 21 | ineq2i 4038 |
. . . . . . . . . 10
⊢
((1^{st} ‘(1^{st} ‘𝑠)) ∩ ((∪
((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} ‘𝑠)}))))) = ((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))) |
23 | 20, 22 | eqtri 2849 |
. . . . . . . . 9
⊢
(((1^{st} ‘(1^{st} ‘𝑠)) ∩ (∪
((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} ‘𝑠)})))) = ((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))) |
24 | 23 | a1i 11 |
. . . . . . . 8
⊢ (𝑠 ∈ (mPreSt‘𝑇) → (((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((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} ‘𝑠)})))) = ((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)}))))) |
25 | 24 | oteq1d 4635 |
. . . . . . 7
⊢ (𝑠 ∈ (mPreSt‘𝑇) → ⟨(((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((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} ‘𝑠)})))), (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} ‘𝑠)⟩) |
26 | 19, 25 | eqtrd 2861 |
. . . . . 6
⊢ (𝑠 ∈ (mPreSt‘𝑇) → (𝑅‘⟨((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} ‘𝑠)})))), (2^{nd}
‘(1^{st} ‘𝑠)), (2^{nd} ‘𝑠)⟩) |
27 | 15 | fveq2d 6437 |
. . . . . 6
⊢ (𝑠 ∈ (mPreSt‘𝑇) → (𝑅‘(𝑅‘𝑠)) = (𝑅‘⟨((1^{st}
‘(1^{st} ‘𝑠)) ∩ (∪
((mVars‘𝑇) “
((2^{nd} ‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})) × ∪ ((mVars‘𝑇) “ ((2^{nd}
‘(1^{st} ‘𝑠)) ∪ {(2^{nd} ‘𝑠)})))), (2^{nd}
‘(1^{st} ‘𝑠)), (2^{nd} ‘𝑠)⟩)) |
28 | 26, 27, 15 | 3eqtr4d 2871 |
. . . . 5
⊢ (𝑠 ∈ (mPreSt‘𝑇) → (𝑅‘(𝑅‘𝑠)) = (𝑅‘𝑠)) |
29 | | fveq2 6433 |
. . . . . 6
⊢ ((𝑅‘𝑠) = 𝑋 → (𝑅‘(𝑅‘𝑠)) = (𝑅‘𝑋)) |
30 | | id 22 |
. . . . . 6
⊢ ((𝑅‘𝑠) = 𝑋 → (𝑅‘𝑠) = 𝑋) |
31 | 29, 30 | eqeq12d 2840 |
. . . . 5
⊢ ((𝑅‘𝑠) = 𝑋 → ((𝑅‘(𝑅‘𝑠)) = (𝑅‘𝑠) ↔ (𝑅‘𝑋) = 𝑋)) |
32 | 28, 31 | syl5ibcom 237 |
. . . 4
⊢ (𝑠 ∈ (mPreSt‘𝑇) → ((𝑅‘𝑠) = 𝑋 → (𝑅‘𝑋) = 𝑋)) |
33 | 32 | rexlimiv 3236 |
. . 3
⊢
(∃𝑠 ∈
(mPreSt‘𝑇)(𝑅‘𝑠) = 𝑋 → (𝑅‘𝑋) = 𝑋) |
34 | 6, 33 | sylbi 209 |
. 2
⊢ (𝑋 ∈ ran 𝑅 → (𝑅‘𝑋) = 𝑋) |
35 | | mstaval.s |
. . 3
⊢ 𝑆 = (mStat‘𝑇) |
36 | 2, 35 | mstaval 31987 |
. 2
⊢ 𝑆 = ran 𝑅 |
37 | 34, 36 | eleq2s 2924 |
1
⊢ (𝑋 ∈ 𝑆 → (𝑅‘𝑋) = 𝑋) |