Step | Hyp | Ref
| Expression |
1 | | mclspps.5 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ ran 𝐿) |
2 | | mclspps.l |
. . . . 5
⊢ 𝐿 = (mSubst‘𝑇) |
3 | | mclspps.e |
. . . . 5
⊢ 𝐸 = (mEx‘𝑇) |
4 | 2, 3 | msubf 31429 |
. . . 4
⊢ (𝑆 ∈ ran 𝐿 → 𝑆:𝐸⟶𝐸) |
5 | 1, 4 | syl 17 |
. . 3
⊢ (𝜑 → 𝑆:𝐸⟶𝐸) |
6 | | ffn 6045 |
. . 3
⊢ (𝑆:𝐸⟶𝐸 → 𝑆 Fn 𝐸) |
7 | 5, 6 | syl 17 |
. 2
⊢ (𝜑 → 𝑆 Fn 𝐸) |
8 | | mclspps.d |
. . . 4
⊢ 𝐷 = (mDV‘𝑇) |
9 | | mclspps.c |
. . . 4
⊢ 𝐶 = (mCls‘𝑇) |
10 | | mclspps.1 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ mFS) |
11 | | eqid 2622 |
. . . . . . . . 9
⊢
(mPreSt‘𝑇) =
(mPreSt‘𝑇) |
12 | | mclspps.j |
. . . . . . . . 9
⊢ 𝐽 = (mPPSt‘𝑇) |
13 | 11, 12 | mppspst 31471 |
. . . . . . . 8
⊢ 𝐽 ⊆ (mPreSt‘𝑇) |
14 | | mclspps.4 |
. . . . . . . 8
⊢ (𝜑 → 〈𝑀, 𝑂, 𝑃〉 ∈ 𝐽) |
15 | 13, 14 | sseldi 3601 |
. . . . . . 7
⊢ (𝜑 → 〈𝑀, 𝑂, 𝑃〉 ∈ (mPreSt‘𝑇)) |
16 | 8, 3, 11 | elmpst 31433 |
. . . . . . 7
⊢
(〈𝑀, 𝑂, 𝑃〉 ∈ (mPreSt‘𝑇) ↔ ((𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀) ∧ (𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin) ∧ 𝑃 ∈ 𝐸)) |
17 | 15, 16 | sylib 208 |
. . . . . 6
⊢ (𝜑 → ((𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀) ∧ (𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin) ∧ 𝑃 ∈ 𝐸)) |
18 | 17 | simp1d 1073 |
. . . . 5
⊢ (𝜑 → (𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀)) |
19 | 18 | simpld 475 |
. . . 4
⊢ (𝜑 → 𝑀 ⊆ 𝐷) |
20 | 17 | simp2d 1074 |
. . . . 5
⊢ (𝜑 → (𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin)) |
21 | 20 | simpld 475 |
. . . 4
⊢ (𝜑 → 𝑂 ⊆ 𝐸) |
22 | | eqid 2622 |
. . . 4
⊢
(mAx‘𝑇) =
(mAx‘𝑇) |
23 | | mclspps.v |
. . . 4
⊢ 𝑉 = (mVR‘𝑇) |
24 | | mclspps.h |
. . . 4
⊢ 𝐻 = (mVH‘𝑇) |
25 | | mclspps.w |
. . . 4
⊢ 𝑊 = (mVars‘𝑇) |
26 | | mclspps.6 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → (𝑆‘𝑥) ∈ (𝐾𝐶𝐵)) |
27 | 26 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑂 (𝑆‘𝑥) ∈ (𝐾𝐶𝐵)) |
28 | | ffun 6048 |
. . . . . . 7
⊢ (𝑆:𝐸⟶𝐸 → Fun 𝑆) |
29 | 5, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → Fun 𝑆) |
30 | | fdm 6051 |
. . . . . . . 8
⊢ (𝑆:𝐸⟶𝐸 → dom 𝑆 = 𝐸) |
31 | 5, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 → dom 𝑆 = 𝐸) |
32 | 21, 31 | sseqtr4d 3642 |
. . . . . 6
⊢ (𝜑 → 𝑂 ⊆ dom 𝑆) |
33 | | funimass5 6334 |
. . . . . 6
⊢ ((Fun
𝑆 ∧ 𝑂 ⊆ dom 𝑆) → (𝑂 ⊆ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ ∀𝑥 ∈ 𝑂 (𝑆‘𝑥) ∈ (𝐾𝐶𝐵))) |
34 | 29, 32, 33 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝑂 ⊆ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ ∀𝑥 ∈ 𝑂 (𝑆‘𝑥) ∈ (𝐾𝐶𝐵))) |
35 | 27, 34 | mpbird 247 |
. . . 4
⊢ (𝜑 → 𝑂 ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) |
36 | 23, 3, 24 | mvhf 31455 |
. . . . . . 7
⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸) |
37 | 10, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐻:𝑉⟶𝐸) |
38 | 37 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝐻‘𝑣) ∈ 𝐸) |
39 | | mclspps.7 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵)) |
40 | | elpreima 6337 |
. . . . . . 7
⊢ (𝑆 Fn 𝐸 → ((𝐻‘𝑣) ∈ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝐻‘𝑣) ∈ 𝐸 ∧ (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵)))) |
41 | 7, 40 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐻‘𝑣) ∈ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝐻‘𝑣) ∈ 𝐸 ∧ (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵)))) |
42 | 41 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ((𝐻‘𝑣) ∈ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝐻‘𝑣) ∈ 𝐸 ∧ (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵)))) |
43 | 38, 39, 42 | mpbir2and 957 |
. . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝐻‘𝑣) ∈ (◡𝑆 “ (𝐾𝐶𝐵))) |
44 | 10 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇) ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) ∧ ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) → 𝑇 ∈ mFS) |
45 | | mclspps.2 |
. . . . . 6
⊢ (𝜑 → 𝐾 ⊆ 𝐷) |
46 | 45 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇) ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) ∧ ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) → 𝐾 ⊆ 𝐷) |
47 | | mclspps.3 |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ 𝐸) |
48 | 47 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇) ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) ∧ ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) → 𝐵 ⊆ 𝐸) |
49 | 14 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇) ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) ∧ ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) → 〈𝑀, 𝑂, 𝑃〉 ∈ 𝐽) |
50 | 1 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇) ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) ∧ ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) → 𝑆 ∈ ran 𝐿) |
51 | 26 | 3ad2antl1 1223 |
. . . . 5
⊢ (((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇) ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) ∧ ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) ∧ 𝑥 ∈ 𝑂) → (𝑆‘𝑥) ∈ (𝐾𝐶𝐵)) |
52 | 39 | 3ad2antl1 1223 |
. . . . 5
⊢ (((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇) ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) ∧ ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) ∧ 𝑣 ∈ 𝑉) → (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵)) |
53 | | mclspps.8 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) → 𝑎𝐾𝑏) |
54 | 53 | 3ad2antl1 1223 |
. . . . 5
⊢ (((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇) ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) ∧ ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) → 𝑎𝐾𝑏) |
55 | | simp21 1094 |
. . . . 5
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇) ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) ∧ ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) → 〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇)) |
56 | | simp22 1095 |
. . . . 5
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇) ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) ∧ ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) → 𝑠 ∈ ran 𝐿) |
57 | | simp23 1096 |
. . . . 5
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇) ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) ∧ ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) |
58 | | simp3 1063 |
. . . . 5
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇) ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) ∧ ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) → ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) |
59 | 8, 3, 9, 44, 46, 48, 12, 2, 23, 24, 25, 49, 50, 51, 52, 54, 55, 56, 57, 58 | mclsppslem 31480 |
. . . 4
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑇) ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) ∧ ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀)) → (𝑠‘𝑝) ∈ (◡𝑆 “ (𝐾𝐶𝐵))) |
60 | 8, 3, 9, 10, 19, 21, 22, 2, 23, 24, 25, 35, 43, 59 | mclsind 31467 |
. . 3
⊢ (𝜑 → (𝑀𝐶𝑂) ⊆ (◡𝑆 “ (𝐾𝐶𝐵))) |
61 | 11, 12, 9 | elmpps 31470 |
. . . . 5
⊢
(〈𝑀, 𝑂, 𝑃〉 ∈ 𝐽 ↔ (〈𝑀, 𝑂, 𝑃〉 ∈ (mPreSt‘𝑇) ∧ 𝑃 ∈ (𝑀𝐶𝑂))) |
62 | 61 | simprbi 480 |
. . . 4
⊢
(〈𝑀, 𝑂, 𝑃〉 ∈ 𝐽 → 𝑃 ∈ (𝑀𝐶𝑂)) |
63 | 14, 62 | syl 17 |
. . 3
⊢ (𝜑 → 𝑃 ∈ (𝑀𝐶𝑂)) |
64 | 60, 63 | sseldd 3604 |
. 2
⊢ (𝜑 → 𝑃 ∈ (◡𝑆 “ (𝐾𝐶𝐵))) |
65 | | elpreima 6337 |
. . 3
⊢ (𝑆 Fn 𝐸 → (𝑃 ∈ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑃 ∈ 𝐸 ∧ (𝑆‘𝑃) ∈ (𝐾𝐶𝐵)))) |
66 | 65 | simplbda 654 |
. 2
⊢ ((𝑆 Fn 𝐸 ∧ 𝑃 ∈ (◡𝑆 “ (𝐾𝐶𝐵))) → (𝑆‘𝑃) ∈ (𝐾𝐶𝐵)) |
67 | 7, 64, 66 | syl2anc 693 |
1
⊢ (𝜑 → (𝑆‘𝑃) ∈ (𝐾𝐶𝐵)) |