Step | Hyp | Ref
| Expression |
1 | | mclsval.d |
. . 3
⊢ 𝐷 = (mDV‘𝑇) |
2 | | mclsval.e |
. . 3
⊢ 𝐸 = (mEx‘𝑇) |
3 | | mclsval.c |
. . 3
⊢ 𝐶 = (mCls‘𝑇) |
4 | | mclsval.1 |
. . 3
⊢ (𝜑 → 𝑇 ∈ mFS) |
5 | | mclsval.2 |
. . 3
⊢ (𝜑 → 𝐾 ⊆ 𝐷) |
6 | | mclsval.3 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ 𝐸) |
7 | | mclsax.h |
. . 3
⊢ 𝐻 = (mVH‘𝑇) |
8 | | mclsax.a |
. . 3
⊢ 𝐴 = (mAx‘𝑇) |
9 | | mclsax.l |
. . 3
⊢ 𝐿 = (mSubst‘𝑇) |
10 | | mclsax.w |
. . 3
⊢ 𝑊 = (mVars‘𝑇) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | mclsval 30714 |
. 2
⊢ (𝜑 → (𝐾𝐶𝐵) = ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))}) |
12 | | mclsind.4 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ 𝑄) |
13 | 6, 12 | ssind 3799 |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ (𝐸 ∩ 𝑄)) |
14 | | mclsax.v |
. . . . . . . . . . 11
⊢ 𝑉 = (mVR‘𝑇) |
15 | 14, 2, 7 | mvhf 30709 |
. . . . . . . . . 10
⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸) |
16 | 4, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻:𝑉⟶𝐸) |
17 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐻:𝑉⟶𝐸 → 𝐻 Fn 𝑉) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 Fn 𝑉) |
19 | 16 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝐻‘𝑣) ∈ 𝐸) |
20 | | mclsind.5 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝐻‘𝑣) ∈ 𝑄) |
21 | 19, 20 | elind 3760 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝐻‘𝑣) ∈ (𝐸 ∩ 𝑄)) |
22 | 21 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ 𝑉 (𝐻‘𝑣) ∈ (𝐸 ∩ 𝑄)) |
23 | | ffnfv 6295 |
. . . . . . . 8
⊢ (𝐻:𝑉⟶(𝐸 ∩ 𝑄) ↔ (𝐻 Fn 𝑉 ∧ ∀𝑣 ∈ 𝑉 (𝐻‘𝑣) ∈ (𝐸 ∩ 𝑄))) |
24 | 18, 22, 23 | sylanbrc 695 |
. . . . . . 7
⊢ (𝜑 → 𝐻:𝑉⟶(𝐸 ∩ 𝑄)) |
25 | | frn 5966 |
. . . . . . 7
⊢ (𝐻:𝑉⟶(𝐸 ∩ 𝑄) → ran 𝐻 ⊆ (𝐸 ∩ 𝑄)) |
26 | 24, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝐻 ⊆ (𝐸 ∩ 𝑄)) |
27 | 13, 26 | unssd 3751 |
. . . . 5
⊢ (𝜑 → (𝐵 ∪ ran 𝐻) ⊆ (𝐸 ∩ 𝑄)) |
28 | | id 22 |
. . . . . . . . . . . 12
⊢ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄)) |
29 | | inss2 3796 |
. . . . . . . . . . . 12
⊢ (𝐸 ∩ 𝑄) ⊆ 𝑄 |
30 | 28, 29 | syl6ss 3580 |
. . . . . . . . . . 11
⊢ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄) |
31 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝑇 ∈ mFS) |
32 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(mREx‘𝑇) =
(mREx‘𝑇) |
33 | 14, 32, 9, 2 | msubff 30681 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ mFS → 𝐿:((mREx‘𝑇) ↑pm 𝑉)⟶(𝐸 ↑𝑚 𝐸)) |
34 | | frn 5966 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿:((mREx‘𝑇) ↑pm 𝑉)⟶(𝐸 ↑𝑚 𝐸) → ran 𝐿 ⊆ (𝐸 ↑𝑚 𝐸)) |
35 | 31, 33, 34 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → ran 𝐿 ⊆ (𝐸 ↑𝑚 𝐸)) |
36 | | simpr2 1061 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝑠 ∈ ran 𝐿) |
37 | 35, 36 | sseldd 3569 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝑠 ∈ (𝐸 ↑𝑚 𝐸)) |
38 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ (𝐸 ↑𝑚 𝐸) → 𝑠:𝐸⟶𝐸) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝑠:𝐸⟶𝐸) |
40 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(mStat‘𝑇) =
(mStat‘𝑇) |
41 | 8, 40 | maxsta 30705 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ mFS → 𝐴 ⊆ (mStat‘𝑇)) |
42 | 31, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝐴 ⊆ (mStat‘𝑇)) |
43 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(mPreSt‘𝑇) =
(mPreSt‘𝑇) |
44 | 43, 40 | mstapst 30698 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(mStat‘𝑇)
⊆ (mPreSt‘𝑇) |
45 | 42, 44 | syl6ss 3580 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝐴 ⊆ (mPreSt‘𝑇)) |
46 | | simpr1 1060 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴) |
47 | 45, 46 | sseldd 3569 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 〈𝑚, 𝑜, 𝑝〉 ∈ (mPreSt‘𝑇)) |
48 | 1, 2, 43 | elmpst 30687 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑚, 𝑜, 𝑝〉 ∈ (mPreSt‘𝑇) ↔ ((𝑚 ⊆ 𝐷 ∧ ◡𝑚 = 𝑚) ∧ (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin) ∧ 𝑝 ∈ 𝐸)) |
49 | 48 | simp3bi 1071 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑚, 𝑜, 𝑝〉 ∈ (mPreSt‘𝑇) → 𝑝 ∈ 𝐸) |
50 | 47, 49 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝑝 ∈ 𝐸) |
51 | 39, 50 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → (𝑠‘𝑝) ∈ 𝐸) |
52 | 51 | 3adant3 1074 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝐸) |
53 | | mclsind.6 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑄) |
54 | 52, 53 | elind 3760 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)) |
55 | 54 | 3exp 1256 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄) → (∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
56 | 55 | 3expd 1276 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → (𝑠 ∈ ran 𝐿 → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄 → (∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))))) |
57 | 56 | imp31 447 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴) ∧ 𝑠 ∈ ran 𝐿) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄 → (∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
58 | 30, 57 | syl5 33 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴) ∧ 𝑠 ∈ ran 𝐿) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) → (∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
59 | 58 | impd 446 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴) ∧ 𝑠 ∈ ran 𝐿) → (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))) |
60 | 59 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ 〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴) → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))) |
61 | 60 | ex 449 |
. . . . . . 7
⊢ (𝜑 → (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
62 | 61 | alrimiv 1842 |
. . . . . 6
⊢ (𝜑 → ∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
63 | 62 | alrimivv 1843 |
. . . . 5
⊢ (𝜑 → ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
64 | | fvex 6113 |
. . . . . . . 8
⊢
(mEx‘𝑇) ∈
V |
65 | 2, 64 | eqeltri 2684 |
. . . . . . 7
⊢ 𝐸 ∈ V |
66 | 65 | inex1 4727 |
. . . . . 6
⊢ (𝐸 ∩ 𝑄) ∈ V |
67 | | sseq2 3590 |
. . . . . . 7
⊢ (𝑐 = (𝐸 ∩ 𝑄) → ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ↔ (𝐵 ∪ ran 𝐻) ⊆ (𝐸 ∩ 𝑄))) |
68 | | sseq2 3590 |
. . . . . . . . . . . . 13
⊢ (𝑐 = (𝐸 ∩ 𝑄) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ↔ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄))) |
69 | 68 | anbi1d 737 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝐸 ∩ 𝑄) → (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) ↔ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)))) |
70 | | eleq2 2677 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝐸 ∩ 𝑄) → ((𝑠‘𝑝) ∈ 𝑐 ↔ (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))) |
71 | 69, 70 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑐 = (𝐸 ∩ 𝑄) → ((((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐) ↔ (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
72 | 71 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑐 = (𝐸 ∩ 𝑄) → (∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐) ↔ ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
73 | 72 | imbi2d 329 |
. . . . . . . . 9
⊢ (𝑐 = (𝐸 ∩ 𝑄) → ((〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))))) |
74 | 73 | albidv 1836 |
. . . . . . . 8
⊢ (𝑐 = (𝐸 ∩ 𝑄) → (∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ ∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))))) |
75 | 74 | 2albidv 1838 |
. . . . . . 7
⊢ (𝑐 = (𝐸 ∩ 𝑄) → (∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))))) |
76 | 67, 75 | anbi12d 743 |
. . . . . 6
⊢ (𝑐 = (𝐸 ∩ 𝑄) → (((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) ↔ ((𝐵 ∪ ran 𝐻) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))))) |
77 | 66, 76 | elab 3319 |
. . . . 5
⊢ ((𝐸 ∩ 𝑄) ∈ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ↔ ((𝐵 ∪ ran 𝐻) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))))) |
78 | 27, 63, 77 | sylanbrc 695 |
. . . 4
⊢ (𝜑 → (𝐸 ∩ 𝑄) ∈ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))}) |
79 | | intss1 4427 |
. . . 4
⊢ ((𝐸 ∩ 𝑄) ∈ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} → ∩
{𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ (𝐸 ∩ 𝑄)) |
80 | 78, 79 | syl 17 |
. . 3
⊢ (𝜑 → ∩ {𝑐
∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ (𝐸 ∩ 𝑄)) |
81 | 80, 29 | syl6ss 3580 |
. 2
⊢ (𝜑 → ∩ {𝑐
∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝑄) |
82 | 11, 81 | eqsstrd 3602 |
1
⊢ (𝜑 → (𝐾𝐶𝐵) ⊆ 𝑄) |