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 33096 |
. 2
⊢ (𝜑 → (𝐾𝐶𝐵) = ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))}) |
12 | | mclsind.4 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ 𝑄) |
13 | 6, 12 | ssind 4123 |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ (𝐸 ∩ 𝑄)) |
14 | | mclsax.v |
. . . . . . . . . . 11
⊢ 𝑉 = (mVR‘𝑇) |
15 | 14, 2, 7 | mvhf 33091 |
. . . . . . . . . 10
⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸) |
16 | 4, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻:𝑉⟶𝐸) |
17 | 16 | ffnd 6505 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 Fn 𝑉) |
18 | 16 | ffvelrnda 6861 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝐻‘𝑣) ∈ 𝐸) |
19 | | mclsind.5 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝐻‘𝑣) ∈ 𝑄) |
20 | 18, 19 | elind 4084 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝐻‘𝑣) ∈ (𝐸 ∩ 𝑄)) |
21 | 20 | ralrimiva 3096 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ 𝑉 (𝐻‘𝑣) ∈ (𝐸 ∩ 𝑄)) |
22 | | ffnfv 6892 |
. . . . . . . 8
⊢ (𝐻:𝑉⟶(𝐸 ∩ 𝑄) ↔ (𝐻 Fn 𝑉 ∧ ∀𝑣 ∈ 𝑉 (𝐻‘𝑣) ∈ (𝐸 ∩ 𝑄))) |
23 | 17, 21, 22 | sylanbrc 586 |
. . . . . . 7
⊢ (𝜑 → 𝐻:𝑉⟶(𝐸 ∩ 𝑄)) |
24 | 23 | frnd 6512 |
. . . . . 6
⊢ (𝜑 → ran 𝐻 ⊆ (𝐸 ∩ 𝑄)) |
25 | 13, 24 | unssd 4076 |
. . . . 5
⊢ (𝜑 → (𝐵 ∪ ran 𝐻) ⊆ (𝐸 ∩ 𝑄)) |
26 | | id 22 |
. . . . . . . . . . . 12
⊢ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄)) |
27 | | inss2 4120 |
. . . . . . . . . . . 12
⊢ (𝐸 ∩ 𝑄) ⊆ 𝑄 |
28 | 26, 27 | sstrdi 3889 |
. . . . . . . . . . 11
⊢ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄) |
29 | 4 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝑇 ∈ mFS) |
30 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(mREx‘𝑇) =
(mREx‘𝑇) |
31 | 14, 30, 9, 2 | msubff 33063 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ mFS → 𝐿:((mREx‘𝑇) ↑pm 𝑉)⟶(𝐸 ↑m 𝐸)) |
32 | | frn 6511 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿:((mREx‘𝑇) ↑pm 𝑉)⟶(𝐸 ↑m 𝐸) → ran 𝐿 ⊆ (𝐸 ↑m 𝐸)) |
33 | 29, 31, 32 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → ran 𝐿 ⊆ (𝐸 ↑m 𝐸)) |
34 | | simpr2 1196 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝑠 ∈ ran 𝐿) |
35 | 33, 34 | sseldd 3878 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝑠 ∈ (𝐸 ↑m 𝐸)) |
36 | | elmapi 8459 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ (𝐸 ↑m 𝐸) → 𝑠:𝐸⟶𝐸) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝑠:𝐸⟶𝐸) |
38 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(mStat‘𝑇) =
(mStat‘𝑇) |
39 | 8, 38 | maxsta 33087 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ mFS → 𝐴 ⊆ (mStat‘𝑇)) |
40 | 29, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝐴 ⊆ (mStat‘𝑇)) |
41 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(mPreSt‘𝑇) =
(mPreSt‘𝑇) |
42 | 41, 38 | mstapst 33080 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(mStat‘𝑇)
⊆ (mPreSt‘𝑇) |
43 | 40, 42 | sstrdi 3889 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝐴 ⊆ (mPreSt‘𝑇)) |
44 | | simpr1 1195 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴) |
45 | 43, 44 | sseldd 3878 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 〈𝑚, 𝑜, 𝑝〉 ∈ (mPreSt‘𝑇)) |
46 | 1, 2, 41 | elmpst 33069 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑚, 𝑜, 𝑝〉 ∈ (mPreSt‘𝑇) ↔ ((𝑚 ⊆ 𝐷 ∧ ◡𝑚 = 𝑚) ∧ (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin) ∧ 𝑝 ∈ 𝐸)) |
47 | 46 | simp3bi 1148 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑚, 𝑜, 𝑝〉 ∈ (mPreSt‘𝑇) → 𝑝 ∈ 𝐸) |
48 | 45, 47 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → 𝑝 ∈ 𝐸) |
49 | 37, 48 | ffvelrnd 6862 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄)) → (𝑠‘𝑝) ∈ 𝐸) |
50 | 49 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝐸) |
51 | | mclsind.6 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑄) |
52 | 50, 51 | elind 4084 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)) |
53 | 52 | 3exp 1120 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄) → (∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
54 | 53 | 3expd 1354 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → (𝑠 ∈ ran 𝐿 → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄 → (∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))))) |
55 | 54 | imp31 421 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴) ∧ 𝑠 ∈ ran 𝐿) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑄 → (∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
56 | 28, 55 | syl5 34 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴) ∧ 𝑠 ∈ ran 𝐿) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) → (∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
57 | 56 | impd 414 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴) ∧ 𝑠 ∈ ran 𝐿) → (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))) |
58 | 57 | ralrimiva 3096 |
. . . . . . . 8
⊢ ((𝜑 ∧ 〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴) → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))) |
59 | 58 | ex 416 |
. . . . . . 7
⊢ (𝜑 → (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
60 | 59 | alrimiv 1934 |
. . . . . 6
⊢ (𝜑 → ∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
61 | 60 | alrimivv 1935 |
. . . . 5
⊢ (𝜑 → ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
62 | 2 | fvexi 6688 |
. . . . . . 7
⊢ 𝐸 ∈ V |
63 | 62 | inex1 5185 |
. . . . . 6
⊢ (𝐸 ∩ 𝑄) ∈ V |
64 | | sseq2 3903 |
. . . . . . 7
⊢ (𝑐 = (𝐸 ∩ 𝑄) → ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ↔ (𝐵 ∪ ran 𝐻) ⊆ (𝐸 ∩ 𝑄))) |
65 | | sseq2 3903 |
. . . . . . . . . . . . 13
⊢ (𝑐 = (𝐸 ∩ 𝑄) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ↔ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄))) |
66 | 65 | anbi1d 633 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝐸 ∩ 𝑄) → (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) ↔ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)))) |
67 | | eleq2 2821 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝐸 ∩ 𝑄) → ((𝑠‘𝑝) ∈ 𝑐 ↔ (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))) |
68 | 66, 67 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑐 = (𝐸 ∩ 𝑄) → ((((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐) ↔ (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
69 | 68 | ralbidv 3109 |
. . . . . . . . . 10
⊢ (𝑐 = (𝐸 ∩ 𝑄) → (∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐) ↔ ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))) |
70 | 69 | imbi2d 344 |
. . . . . . . . 9
⊢ (𝑐 = (𝐸 ∩ 𝑄) → ((〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))))) |
71 | 70 | albidv 1927 |
. . . . . . . 8
⊢ (𝑐 = (𝐸 ∩ 𝑄) → (∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ ∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))))) |
72 | 71 | 2albidv 1930 |
. . . . . . 7
⊢ (𝑐 = (𝐸 ∩ 𝑄) → (∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))))) |
73 | 64, 72 | anbi12d 634 |
. . . . . 6
⊢ (𝑐 = (𝐸 ∩ 𝑄) → (((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) ↔ ((𝐵 ∪ ran 𝐻) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄)))))) |
74 | 63, 73 | elab 3573 |
. . . . 5
⊢ ((𝐸 ∩ 𝑄) ∈ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ↔ ((𝐵 ∪ ran 𝐻) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐸 ∩ 𝑄) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ (𝐸 ∩ 𝑄))))) |
75 | 25, 61, 74 | sylanbrc 586 |
. . . 4
⊢ (𝜑 → (𝐸 ∩ 𝑄) ∈ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))}) |
76 | | intss1 4851 |
. . . 4
⊢ ((𝐸 ∩ 𝑄) ∈ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} → ∩
{𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ (𝐸 ∩ 𝑄)) |
77 | 75, 76 | syl 17 |
. . 3
⊢ (𝜑 → ∩ {𝑐
∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ (𝐸 ∩ 𝑄)) |
78 | 77, 27 | sstrdi 3889 |
. 2
⊢ (𝜑 → ∩ {𝑐
∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝑄) |
79 | 11, 78 | eqsstrd 3915 |
1
⊢ (𝜑 → (𝐾𝐶𝐵) ⊆ 𝑄) |