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 |
|
mclsind.4 |
⊢ ( 𝜑 → 𝐵 ⊆ 𝑄 ) |
13 |
|
mclsind.5 |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑣 ) ∈ 𝑄 ) |
14 |
|
mclsind.6 |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑄 ) |
15 |
1 2 3 4 5 6 10 7 8 11
|
mclsval |
⊢ ( 𝜑 → ( 𝐾 𝐶 𝐵 ) = ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) |
16 |
6 12
|
ssind |
⊢ ( 𝜑 → 𝐵 ⊆ ( 𝐸 ∩ 𝑄 ) ) |
17 |
9 2 10
|
mvhf |
⊢ ( 𝑇 ∈ mFS → 𝐻 : 𝑉 ⟶ 𝐸 ) |
18 |
4 17
|
syl |
⊢ ( 𝜑 → 𝐻 : 𝑉 ⟶ 𝐸 ) |
19 |
18
|
ffnd |
⊢ ( 𝜑 → 𝐻 Fn 𝑉 ) |
20 |
18
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑣 ) ∈ 𝐸 ) |
21 |
20 13
|
elind |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑣 ) ∈ ( 𝐸 ∩ 𝑄 ) ) |
22 |
21
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝑉 ( 𝐻 ‘ 𝑣 ) ∈ ( 𝐸 ∩ 𝑄 ) ) |
23 |
|
ffnfv |
⊢ ( 𝐻 : 𝑉 ⟶ ( 𝐸 ∩ 𝑄 ) ↔ ( 𝐻 Fn 𝑉 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐻 ‘ 𝑣 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) |
24 |
19 22 23
|
sylanbrc |
⊢ ( 𝜑 → 𝐻 : 𝑉 ⟶ ( 𝐸 ∩ 𝑄 ) ) |
25 |
24
|
frnd |
⊢ ( 𝜑 → ran 𝐻 ⊆ ( 𝐸 ∩ 𝑄 ) ) |
26 |
16 25
|
unssd |
⊢ ( 𝜑 → ( 𝐵 ∪ ran 𝐻 ) ⊆ ( 𝐸 ∩ 𝑄 ) ) |
27 |
|
id |
⊢ ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) → ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ) |
28 |
|
inss2 |
⊢ ( 𝐸 ∩ 𝑄 ) ⊆ 𝑄 |
29 |
27 28
|
sstrdi |
⊢ ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) → ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) |
30 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝑇 ∈ mFS ) |
31 |
|
eqid |
⊢ ( mREx ‘ 𝑇 ) = ( mREx ‘ 𝑇 ) |
32 |
9 31 8 2
|
msubff |
⊢ ( 𝑇 ∈ mFS → 𝐿 : ( ( mREx ‘ 𝑇 ) ↑pm 𝑉 ) ⟶ ( 𝐸 ↑m 𝐸 ) ) |
33 |
|
frn |
⊢ ( 𝐿 : ( ( mREx ‘ 𝑇 ) ↑pm 𝑉 ) ⟶ ( 𝐸 ↑m 𝐸 ) → ran 𝐿 ⊆ ( 𝐸 ↑m 𝐸 ) ) |
34 |
30 32 33
|
3syl |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → ran 𝐿 ⊆ ( 𝐸 ↑m 𝐸 ) ) |
35 |
|
simpr2 |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝑠 ∈ ran 𝐿 ) |
36 |
34 35
|
sseldd |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝑠 ∈ ( 𝐸 ↑m 𝐸 ) ) |
37 |
|
elmapi |
⊢ ( 𝑠 ∈ ( 𝐸 ↑m 𝐸 ) → 𝑠 : 𝐸 ⟶ 𝐸 ) |
38 |
36 37
|
syl |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝑠 : 𝐸 ⟶ 𝐸 ) |
39 |
|
eqid |
⊢ ( mStat ‘ 𝑇 ) = ( mStat ‘ 𝑇 ) |
40 |
7 39
|
maxsta |
⊢ ( 𝑇 ∈ mFS → 𝐴 ⊆ ( mStat ‘ 𝑇 ) ) |
41 |
30 40
|
syl |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝐴 ⊆ ( mStat ‘ 𝑇 ) ) |
42 |
|
eqid |
⊢ ( mPreSt ‘ 𝑇 ) = ( mPreSt ‘ 𝑇 ) |
43 |
42 39
|
mstapst |
⊢ ( mStat ‘ 𝑇 ) ⊆ ( mPreSt ‘ 𝑇 ) |
44 |
41 43
|
sstrdi |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝐴 ⊆ ( mPreSt ‘ 𝑇 ) ) |
45 |
|
simpr1 |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ) |
46 |
44 45
|
sseldd |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ ( mPreSt ‘ 𝑇 ) ) |
47 |
1 2 42
|
elmpst |
⊢ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ ( mPreSt ‘ 𝑇 ) ↔ ( ( 𝑚 ⊆ 𝐷 ∧ ◡ 𝑚 = 𝑚 ) ∧ ( 𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin ) ∧ 𝑝 ∈ 𝐸 ) ) |
48 |
47
|
simp3bi |
⊢ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ ( mPreSt ‘ 𝑇 ) → 𝑝 ∈ 𝐸 ) |
49 |
46 48
|
syl |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝑝 ∈ 𝐸 ) |
50 |
38 49
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) |
51 |
50
|
3adant3 |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) |
52 |
51 14
|
elind |
⊢ ( ( 𝜑 ∧ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) |
53 |
52
|
3exp |
⊢ ( 𝜑 → ( ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) |
54 |
53
|
3expd |
⊢ ( 𝜑 → ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ( 𝑠 ∈ ran 𝐿 → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) ) ) |
55 |
54
|
imp31 |
⊢ ( ( ( 𝜑 ∧ 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ) ∧ 𝑠 ∈ ran 𝐿 ) → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) |
56 |
29 55
|
syl5 |
⊢ ( ( ( 𝜑 ∧ 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ) ∧ 𝑠 ∈ ran 𝐿 ) → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) |
57 |
56
|
impd |
⊢ ( ( ( 𝜑 ∧ 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ) ∧ 𝑠 ∈ ran 𝐿 ) → ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) |
58 |
57
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 ) → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) |
59 |
58
|
ex |
⊢ ( 𝜑 → ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) |
60 |
59
|
alrimiv |
⊢ ( 𝜑 → ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) |
61 |
60
|
alrimivv |
⊢ ( 𝜑 → ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) |
62 |
2
|
fvexi |
⊢ 𝐸 ∈ V |
63 |
62
|
inex1 |
⊢ ( 𝐸 ∩ 𝑄 ) ∈ V |
64 |
|
sseq2 |
⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ↔ ( 𝐵 ∪ ran 𝐻 ) ⊆ ( 𝐸 ∩ 𝑄 ) ) ) |
65 |
|
sseq2 |
⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ↔ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ) ) |
66 |
65
|
anbi1d |
⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ↔ ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ) ) |
67 |
|
eleq2 |
⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ↔ ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) |
68 |
66 67
|
imbi12d |
⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ↔ ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) |
69 |
68
|
ralbidv |
⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ↔ ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) |
70 |
69
|
imbi2d |
⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) ) |
71 |
70
|
albidv |
⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) ) |
72 |
71
|
2albidv |
⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) ) |
73 |
64 72
|
anbi12d |
⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ↔ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) ) ) |
74 |
63 73
|
elab |
⊢ ( ( 𝐸 ∩ 𝑄 ) ∈ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ↔ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) ) |
75 |
26 61 74
|
sylanbrc |
⊢ ( 𝜑 → ( 𝐸 ∩ 𝑄 ) ∈ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) |
76 |
|
intss1 |
⊢ ( ( 𝐸 ∩ 𝑄 ) ∈ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ ( 𝐸 ∩ 𝑄 ) ) |
77 |
75 76
|
syl |
⊢ ( 𝜑 → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ ( 𝐸 ∩ 𝑄 ) ) |
78 |
77 28
|
sstrdi |
⊢ ( 𝜑 → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( 〈 𝑚 , 𝑜 , 𝑝 〉 ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ 𝑄 ) |
79 |
15 78
|
eqsstrd |
⊢ ( 𝜑 → ( 𝐾 𝐶 𝐵 ) ⊆ 𝑄 ) |