Proof of Theorem elmsta
Step | Hyp | Ref
| Expression |
1 | | mstapst.p |
. . . . 5
⊢ 𝑃 = (mPreSt‘𝑇) |
2 | | mstapst.s |
. . . . 5
⊢ 𝑆 = (mStat‘𝑇) |
3 | 1, 2 | mstapst 33222 |
. . . 4
⊢ 𝑆 ⊆ 𝑃 |
4 | 3 | sseli 3896 |
. . 3
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → 〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃) |
5 | | elmsta.v |
. . . . . . . . . 10
⊢ 𝑉 = (mVars‘𝑇) |
6 | | eqid 2737 |
. . . . . . . . . 10
⊢
(mStRed‘𝑇) =
(mStRed‘𝑇) |
7 | | elmsta.z |
. . . . . . . . . 10
⊢ 𝑍 = ∪
(𝑉 “ (𝐻 ∪ {𝐴})) |
8 | 5, 1, 6, 7 | msrval 33213 |
. . . . . . . . 9
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → ((mStRed‘𝑇)‘〈𝐷, 𝐻, 𝐴〉) = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
9 | 4, 8 | syl 17 |
. . . . . . . 8
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → ((mStRed‘𝑇)‘〈𝐷, 𝐻, 𝐴〉) = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
10 | 6, 2 | msrid 33220 |
. . . . . . . 8
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → ((mStRed‘𝑇)‘〈𝐷, 𝐻, 𝐴〉) = 〈𝐷, 𝐻, 𝐴〉) |
11 | 9, 10 | eqtr3d 2779 |
. . . . . . 7
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉 = 〈𝐷, 𝐻, 𝐴〉) |
12 | 11 | fveq2d 6721 |
. . . . . 6
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → (1st ‘〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) = (1st ‘〈𝐷, 𝐻, 𝐴〉)) |
13 | 12 | fveq2d 6721 |
. . . . 5
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → (1st
‘(1st ‘〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉)) = (1st
‘(1st ‘〈𝐷, 𝐻, 𝐴〉))) |
14 | | inss1 4143 |
. . . . . . 7
⊢ (𝐷 ∩ (𝑍 × 𝑍)) ⊆ 𝐷 |
15 | 1 | mpstrcl 33216 |
. . . . . . . . 9
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V)) |
16 | 4, 15 | syl 17 |
. . . . . . . 8
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → (𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V)) |
17 | 16 | simp1d 1144 |
. . . . . . 7
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → 𝐷 ∈ V) |
18 | | ssexg 5216 |
. . . . . . 7
⊢ (((𝐷 ∩ (𝑍 × 𝑍)) ⊆ 𝐷 ∧ 𝐷 ∈ V) → (𝐷 ∩ (𝑍 × 𝑍)) ∈ V) |
19 | 14, 17, 18 | sylancr 590 |
. . . . . 6
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → (𝐷 ∩ (𝑍 × 𝑍)) ∈ V) |
20 | 16 | simp2d 1145 |
. . . . . 6
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → 𝐻 ∈ V) |
21 | 16 | simp3d 1146 |
. . . . . 6
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → 𝐴 ∈ V) |
22 | | ot1stg 7775 |
. . . . . 6
⊢ (((𝐷 ∩ (𝑍 × 𝑍)) ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V) → (1st
‘(1st ‘〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉)) = (𝐷 ∩ (𝑍 × 𝑍))) |
23 | 19, 20, 21, 22 | syl3anc 1373 |
. . . . 5
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → (1st
‘(1st ‘〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉)) = (𝐷 ∩ (𝑍 × 𝑍))) |
24 | | ot1stg 7775 |
. . . . . 6
⊢ ((𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V) →
(1st ‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐷) |
25 | 16, 24 | syl 17 |
. . . . 5
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → (1st
‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐷) |
26 | 13, 23, 25 | 3eqtr3d 2785 |
. . . 4
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → (𝐷 ∩ (𝑍 × 𝑍)) = 𝐷) |
27 | | inss2 4144 |
. . . 4
⊢ (𝐷 ∩ (𝑍 × 𝑍)) ⊆ (𝑍 × 𝑍) |
28 | 26, 27 | eqsstrrdi 3956 |
. . 3
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → 𝐷 ⊆ (𝑍 × 𝑍)) |
29 | 4, 28 | jca 515 |
. 2
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 → (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍))) |
30 | 8 | adantr 484 |
. . . . 5
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍)) → ((mStRed‘𝑇)‘〈𝐷, 𝐻, 𝐴〉) = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
31 | | simpr 488 |
. . . . . . 7
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍)) → 𝐷 ⊆ (𝑍 × 𝑍)) |
32 | | df-ss 3883 |
. . . . . . 7
⊢ (𝐷 ⊆ (𝑍 × 𝑍) ↔ (𝐷 ∩ (𝑍 × 𝑍)) = 𝐷) |
33 | 31, 32 | sylib 221 |
. . . . . 6
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍)) → (𝐷 ∩ (𝑍 × 𝑍)) = 𝐷) |
34 | 33 | oteq1d 4796 |
. . . . 5
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍)) → 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉 = 〈𝐷, 𝐻, 𝐴〉) |
35 | 30, 34 | eqtrd 2777 |
. . . 4
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍)) → ((mStRed‘𝑇)‘〈𝐷, 𝐻, 𝐴〉) = 〈𝐷, 𝐻, 𝐴〉) |
36 | 1, 6 | msrf 33217 |
. . . . . 6
⊢
(mStRed‘𝑇):𝑃⟶𝑃 |
37 | | ffn 6545 |
. . . . . 6
⊢
((mStRed‘𝑇):𝑃⟶𝑃 → (mStRed‘𝑇) Fn 𝑃) |
38 | 36, 37 | ax-mp 5 |
. . . . 5
⊢
(mStRed‘𝑇) Fn
𝑃 |
39 | | simpl 486 |
. . . . 5
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍)) → 〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃) |
40 | | fnfvelrn 6901 |
. . . . 5
⊢
(((mStRed‘𝑇)
Fn 𝑃 ∧ 〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃) → ((mStRed‘𝑇)‘〈𝐷, 𝐻, 𝐴〉) ∈ ran (mStRed‘𝑇)) |
41 | 38, 39, 40 | sylancr 590 |
. . . 4
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍)) → ((mStRed‘𝑇)‘〈𝐷, 𝐻, 𝐴〉) ∈ ran (mStRed‘𝑇)) |
42 | 35, 41 | eqeltrrd 2839 |
. . 3
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍)) → 〈𝐷, 𝐻, 𝐴〉 ∈ ran (mStRed‘𝑇)) |
43 | 6, 2 | mstaval 33219 |
. . 3
⊢ 𝑆 = ran (mStRed‘𝑇) |
44 | 42, 43 | eleqtrrdi 2849 |
. 2
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍)) → 〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆) |
45 | 29, 44 | impbii 212 |
1
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 ↔ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍))) |