Step |
Hyp |
Ref |
Expression |
1 |
|
mclsval.d |
⊢ 𝐷 = ( mDV ‘ 𝑇 ) |
2 |
|
mclsval.e |
⊢ 𝐸 = ( mEx ‘ 𝑇 ) |
3 |
|
mclsval.c |
⊢ 𝐶 = ( mCls ‘ 𝑇 ) |
4 |
|
mclsval.1 |
⊢ ( 𝜑 → 𝑇 ∈ mFS ) |
5 |
|
mclsval.2 |
⊢ ( 𝜑 → 𝐾 ⊆ 𝐷 ) |
6 |
|
mclsval.3 |
⊢ ( 𝜑 → 𝐵 ⊆ 𝐸 ) |
7 |
|
mclsax.a |
⊢ 𝐴 = ( mAx ‘ 𝑇 ) |
8 |
|
mclsax.l |
⊢ 𝐿 = ( mSubst ‘ 𝑇 ) |
9 |
|
mclsax.v |
⊢ 𝑉 = ( mVR ‘ 𝑇 ) |
10 |
|
mclsax.h |
⊢ 𝐻 = ( mVH ‘ 𝑇 ) |
11 |
|
mclsax.w |
⊢ 𝑊 = ( mVars ‘ 𝑇 ) |
12 |
|
mclsax.4 |
⊢ ( 𝜑 → 〈 𝑀 , 𝑂 , 𝑃 〉 ∈ 𝐴 ) |
13 |
|
mclsax.5 |
⊢ ( 𝜑 → 𝑆 ∈ ran 𝐿 ) |
14 |
|
mclsax.6 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) ) |
15 |
|
mclsax.7 |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐾 𝐶 𝐵 ) ) |
16 |
|
mclsax.8 |
⊢ ( ( 𝜑 ∧ ( 𝑥 𝑀 𝑦 ∧ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ) → 𝑎 𝐾 𝑏 ) |
17 |
|
abid |
⊢ ( 𝑐 ∈ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ↔ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ) |
18 |
|
intss1 |
⊢ ( 𝑐 ∈ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ 𝑐 ) |
19 |
17 18
|
sylbir |
⊢ ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ 𝑐 ) |
20 |
1 2 3 4 5 6 10 7 8 11
|
mclsval |
⊢ ( 𝜑 → ( 𝐾 𝐶 𝐵 ) = ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) |
21 |
20
|
sseq1d |
⊢ ( 𝜑 → ( ( 𝐾 𝐶 𝐵 ) ⊆ 𝑐 ↔ ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ 𝑐 ) ) |
22 |
19 21
|
syl5ibr |
⊢ ( 𝜑 → ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) → ( 𝐾 𝐶 𝐵 ) ⊆ 𝑐 ) ) |
23 |
|
sstr2 |
⊢ ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) → ( ( 𝐾 𝐶 𝐵 ) ⊆ 𝑐 → ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ) ) |
24 |
23
|
com12 |
⊢ ( ( 𝐾 𝐶 𝐵 ) ⊆ 𝑐 → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) → ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ) ) |
25 |
24
|
anim1d |
⊢ ( ( 𝐾 𝐶 𝐵 ) ⊆ 𝑐 → ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ) ) |
26 |
25
|
imim1d |
⊢ ( ( 𝐾 𝐶 𝐵 ) ⊆ 𝑐 → ( ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) → ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) |
27 |
26
|
ralimdv |
⊢ ( ( 𝐾 𝐶 𝐵 ) ⊆ 𝑐 → ( ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) |
28 |
27
|
imim2d |
⊢ ( ( 𝐾 𝐶 𝐵 ) ⊆ 𝑐 → ( ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) → ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ) |
29 |
28
|
alimdv |
⊢ ( ( 𝐾 𝐶 𝐵 ) ⊆ 𝑐 → ( ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) → ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ) |
30 |
29
|
2alimdv |
⊢ ( ( 𝐾 𝐶 𝐵 ) ⊆ 𝑐 → ( ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) → ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ) |
31 |
30
|
com12 |
⊢ ( ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) → ( ( 𝐾 𝐶 𝐵 ) ⊆ 𝑐 → ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ) |
32 |
31
|
adantl |
⊢ ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) → ( ( 𝐾 𝐶 𝐵 ) ⊆ 𝑐 → ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ) |
33 |
22 32
|
sylcom |
⊢ ( 𝜑 → ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) → ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ) |
34 |
|
eqid |
⊢ ( mPreSt ‘ 𝑇 ) = ( mPreSt ‘ 𝑇 ) |
35 |
|
eqid |
⊢ ( mStat ‘ 𝑇 ) = ( mStat ‘ 𝑇 ) |
36 |
34 35
|
mstapst |
⊢ ( mStat ‘ 𝑇 ) ⊆ ( mPreSt ‘ 𝑇 ) |
37 |
7 35
|
maxsta |
⊢ ( 𝑇 ∈ mFS → 𝐴 ⊆ ( mStat ‘ 𝑇 ) ) |
38 |
4 37
|
syl |
⊢ ( 𝜑 → 𝐴 ⊆ ( mStat ‘ 𝑇 ) ) |
39 |
38 12
|
sseldd |
⊢ ( 𝜑 → 〈 𝑀 , 𝑂 , 𝑃 〉 ∈ ( mStat ‘ 𝑇 ) ) |
40 |
36 39
|
sseldi |
⊢ ( 𝜑 → 〈 𝑀 , 𝑂 , 𝑃 〉 ∈ ( mPreSt ‘ 𝑇 ) ) |
41 |
34
|
mpstrcl |
⊢ ( 〈 𝑀 , 𝑂 , 𝑃 〉 ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑀 ∈ V ∧ 𝑂 ∈ V ∧ 𝑃 ∈ V ) ) |
42 |
|
simp1 |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → 𝑚 = 𝑀 ) |
43 |
|
simp2 |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → 𝑜 = 𝑂 ) |
44 |
|
simp3 |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → 𝑝 = 𝑃 ) |
45 |
42 43 44
|
oteq123d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → 〈 𝑚 , 𝑜 , 𝑝 〉 = 〈 𝑀 , 𝑂 , 𝑃 〉 ) |
46 |
45
|
eleq1d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ↔ 〈 𝑀 , 𝑂 , 𝑃 〉 ∈ 𝐴 ) ) |
47 |
43
|
uneq1d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → ( 𝑜 ∪ ran 𝐻 ) = ( 𝑂 ∪ ran 𝐻 ) ) |
48 |
47
|
imaeq2d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) = ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ) |
49 |
48
|
sseq1d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ↔ ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ) ) |
50 |
42
|
breqd |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → ( 𝑥 𝑚 𝑦 ↔ 𝑥 𝑀 𝑦 ) ) |
51 |
50
|
imbi1d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → ( ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ↔ ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ) |
52 |
51
|
2albidv |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ) |
53 |
49 52
|
anbi12d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ↔ ( ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ) ) |
54 |
44
|
fveq2d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → ( 𝑠 ‘ 𝑝 ) = ( 𝑠 ‘ 𝑃 ) ) |
55 |
54
|
eleq1d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → ( ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ↔ ( 𝑠 ‘ 𝑃 ) ∈ 𝑐 ) ) |
56 |
53 55
|
imbi12d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → ( ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ↔ ( ( ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑃 ) ∈ 𝑐 ) ) ) |
57 |
56
|
ralbidv |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → ( ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ↔ ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑃 ) ∈ 𝑐 ) ) ) |
58 |
46 57
|
imbi12d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃 ) → ( ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ( 〈 𝑀 , 𝑂 , 𝑃 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑃 ) ∈ 𝑐 ) ) ) ) |
59 |
58
|
spc3gv |
⊢ ( ( 𝑀 ∈ V ∧ 𝑂 ∈ V ∧ 𝑃 ∈ V ) → ( ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) → ( 〈 𝑀 , 𝑂 , 𝑃 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑃 ) ∈ 𝑐 ) ) ) ) |
60 |
40 41 59
|
3syl |
⊢ ( 𝜑 → ( ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) → ( 〈 𝑀 , 𝑂 , 𝑃 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑃 ) ∈ 𝑐 ) ) ) ) |
61 |
|
elun |
⊢ ( 𝑥 ∈ ( 𝑂 ∪ ran 𝐻 ) ↔ ( 𝑥 ∈ 𝑂 ∨ 𝑥 ∈ ran 𝐻 ) ) |
62 |
15
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝑉 ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐾 𝐶 𝐵 ) ) |
63 |
9 2 10
|
mvhf |
⊢ ( 𝑇 ∈ mFS → 𝐻 : 𝑉 ⟶ 𝐸 ) |
64 |
4 63
|
syl |
⊢ ( 𝜑 → 𝐻 : 𝑉 ⟶ 𝐸 ) |
65 |
|
ffn |
⊢ ( 𝐻 : 𝑉 ⟶ 𝐸 → 𝐻 Fn 𝑉 ) |
66 |
|
fveq2 |
⊢ ( 𝑥 = ( 𝐻 ‘ 𝑣 ) → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) |
67 |
66
|
eleq1d |
⊢ ( 𝑥 = ( 𝐻 ‘ 𝑣 ) → ( ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) ↔ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐾 𝐶 𝐵 ) ) ) |
68 |
67
|
ralrn |
⊢ ( 𝐻 Fn 𝑉 → ( ∀ 𝑥 ∈ ran 𝐻 ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐾 𝐶 𝐵 ) ) ) |
69 |
64 65 68
|
3syl |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝐻 ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐾 𝐶 𝐵 ) ) ) |
70 |
62 69
|
mpbird |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐻 ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) ) |
71 |
70
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐻 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) ) |
72 |
14 71
|
jaodan |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑂 ∨ 𝑥 ∈ ran 𝐻 ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) ) |
73 |
61 72
|
sylan2b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∪ ran 𝐻 ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) ) |
74 |
73
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑂 ∪ ran 𝐻 ) ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) ) |
75 |
8 2
|
msubf |
⊢ ( 𝑆 ∈ ran 𝐿 → 𝑆 : 𝐸 ⟶ 𝐸 ) |
76 |
13 75
|
syl |
⊢ ( 𝜑 → 𝑆 : 𝐸 ⟶ 𝐸 ) |
77 |
76
|
ffund |
⊢ ( 𝜑 → Fun 𝑆 ) |
78 |
1 2 34
|
elmpst |
⊢ ( 〈 𝑀 , 𝑂 , 𝑃 〉 ∈ ( mPreSt ‘ 𝑇 ) ↔ ( ( 𝑀 ⊆ 𝐷 ∧ ◡ 𝑀 = 𝑀 ) ∧ ( 𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin ) ∧ 𝑃 ∈ 𝐸 ) ) |
79 |
40 78
|
sylib |
⊢ ( 𝜑 → ( ( 𝑀 ⊆ 𝐷 ∧ ◡ 𝑀 = 𝑀 ) ∧ ( 𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin ) ∧ 𝑃 ∈ 𝐸 ) ) |
80 |
79
|
simp2d |
⊢ ( 𝜑 → ( 𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin ) ) |
81 |
80
|
simpld |
⊢ ( 𝜑 → 𝑂 ⊆ 𝐸 ) |
82 |
76
|
fdmd |
⊢ ( 𝜑 → dom 𝑆 = 𝐸 ) |
83 |
81 82
|
sseqtrrd |
⊢ ( 𝜑 → 𝑂 ⊆ dom 𝑆 ) |
84 |
64
|
frnd |
⊢ ( 𝜑 → ran 𝐻 ⊆ 𝐸 ) |
85 |
84 82
|
sseqtrrd |
⊢ ( 𝜑 → ran 𝐻 ⊆ dom 𝑆 ) |
86 |
83 85
|
unssd |
⊢ ( 𝜑 → ( 𝑂 ∪ ran 𝐻 ) ⊆ dom 𝑆 ) |
87 |
|
funimass4 |
⊢ ( ( Fun 𝑆 ∧ ( 𝑂 ∪ ran 𝐻 ) ⊆ dom 𝑆 ) → ( ( 𝑆 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ↔ ∀ 𝑥 ∈ ( 𝑂 ∪ ran 𝐻 ) ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) ) ) |
88 |
77 86 87
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑆 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ↔ ∀ 𝑥 ∈ ( 𝑂 ∪ ran 𝐻 ) ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) ) ) |
89 |
74 88
|
mpbird |
⊢ ( 𝜑 → ( 𝑆 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ) |
90 |
16
|
3exp2 |
⊢ ( 𝜑 → ( 𝑥 𝑀 𝑦 → ( 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) → 𝑎 𝐾 𝑏 ) ) ) ) |
91 |
90
|
imp4b |
⊢ ( ( 𝜑 ∧ 𝑥 𝑀 𝑦 ) → ( ( 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) → 𝑎 𝐾 𝑏 ) ) |
92 |
91
|
ralrimivv |
⊢ ( ( 𝜑 ∧ 𝑥 𝑀 𝑦 ) → ∀ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ∀ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) 𝑎 𝐾 𝑏 ) |
93 |
|
dfss3 |
⊢ ( ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ↔ ∀ 𝑧 ∈ ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) 𝑧 ∈ 𝐾 ) |
94 |
|
eleq1 |
⊢ ( 𝑧 = 〈 𝑎 , 𝑏 〉 → ( 𝑧 ∈ 𝐾 ↔ 〈 𝑎 , 𝑏 〉 ∈ 𝐾 ) ) |
95 |
|
df-br |
⊢ ( 𝑎 𝐾 𝑏 ↔ 〈 𝑎 , 𝑏 〉 ∈ 𝐾 ) |
96 |
94 95
|
bitr4di |
⊢ ( 𝑧 = 〈 𝑎 , 𝑏 〉 → ( 𝑧 ∈ 𝐾 ↔ 𝑎 𝐾 𝑏 ) ) |
97 |
96
|
ralxp |
⊢ ( ∀ 𝑧 ∈ ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) 𝑧 ∈ 𝐾 ↔ ∀ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ∀ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) 𝑎 𝐾 𝑏 ) |
98 |
93 97
|
bitri |
⊢ ( ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ↔ ∀ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ∀ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) 𝑎 𝐾 𝑏 ) |
99 |
92 98
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑥 𝑀 𝑦 ) → ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) |
100 |
99
|
ex |
⊢ ( 𝜑 → ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) |
101 |
100
|
alrimivv |
⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) |
102 |
89 101
|
jca |
⊢ ( 𝜑 → ( ( 𝑆 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ) |
103 |
|
imaeq1 |
⊢ ( 𝑠 = 𝑆 → ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) = ( 𝑆 “ ( 𝑂 ∪ ran 𝐻 ) ) ) |
104 |
103
|
sseq1d |
⊢ ( 𝑠 = 𝑆 → ( ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ↔ ( 𝑆 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ) ) |
105 |
|
fveq1 |
⊢ ( 𝑠 = 𝑆 → ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) = ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) |
106 |
105
|
fveq2d |
⊢ ( 𝑠 = 𝑆 → ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) = ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) |
107 |
|
fveq1 |
⊢ ( 𝑠 = 𝑆 → ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) |
108 |
107
|
fveq2d |
⊢ ( 𝑠 = 𝑆 → ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) = ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) |
109 |
106 108
|
xpeq12d |
⊢ ( 𝑠 = 𝑆 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) = ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ) |
110 |
109
|
sseq1d |
⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ↔ ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) |
111 |
110
|
imbi2d |
⊢ ( 𝑠 = 𝑆 → ( ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ↔ ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ) |
112 |
111
|
2albidv |
⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ) |
113 |
104 112
|
anbi12d |
⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ↔ ( ( 𝑆 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ) ) |
114 |
|
fveq1 |
⊢ ( 𝑠 = 𝑆 → ( 𝑠 ‘ 𝑃 ) = ( 𝑆 ‘ 𝑃 ) ) |
115 |
114
|
eleq1d |
⊢ ( 𝑠 = 𝑆 → ( ( 𝑠 ‘ 𝑃 ) ∈ 𝑐 ↔ ( 𝑆 ‘ 𝑃 ) ∈ 𝑐 ) ) |
116 |
113 115
|
imbi12d |
⊢ ( 𝑠 = 𝑆 → ( ( ( ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑃 ) ∈ 𝑐 ) ↔ ( ( ( 𝑆 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑆 ‘ 𝑃 ) ∈ 𝑐 ) ) ) |
117 |
116
|
rspcv |
⊢ ( 𝑆 ∈ ran 𝐿 → ( ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑃 ) ∈ 𝑐 ) → ( ( ( 𝑆 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑆 ‘ 𝑃 ) ∈ 𝑐 ) ) ) |
118 |
13 117
|
syl |
⊢ ( 𝜑 → ( ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑃 ) ∈ 𝑐 ) → ( ( ( 𝑆 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑆 ‘ 𝑃 ) ∈ 𝑐 ) ) ) |
119 |
102 118
|
mpid |
⊢ ( 𝜑 → ( ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑃 ) ∈ 𝑐 ) → ( 𝑆 ‘ 𝑃 ) ∈ 𝑐 ) ) |
120 |
12 119
|
embantd |
⊢ ( 𝜑 → ( ( 〈 𝑀 , 𝑂 , 𝑃 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑂 ∪ ran 𝐻 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑀 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑃 ) ∈ 𝑐 ) ) → ( 𝑆 ‘ 𝑃 ) ∈ 𝑐 ) ) |
121 |
33 60 120
|
3syld |
⊢ ( 𝜑 → ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) → ( 𝑆 ‘ 𝑃 ) ∈ 𝑐 ) ) |
122 |
121
|
alrimiv |
⊢ ( 𝜑 → ∀ 𝑐 ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) → ( 𝑆 ‘ 𝑃 ) ∈ 𝑐 ) ) |
123 |
|
fvex |
⊢ ( 𝑆 ‘ 𝑃 ) ∈ V |
124 |
123
|
elintab |
⊢ ( ( 𝑆 ‘ 𝑃 ) ∈ ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ↔ ∀ 𝑐 ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) → ( 𝑆 ‘ 𝑃 ) ∈ 𝑐 ) ) |
125 |
122 124
|
sylibr |
⊢ ( 𝜑 → ( 𝑆 ‘ 𝑃 ) ∈ ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) |
126 |
125 20
|
eleqtrrd |
⊢ ( 𝜑 → ( 𝑆 ‘ 𝑃 ) ∈ ( 𝐾 𝐶 𝐵 ) ) |