Metamath Proof Explorer

Theorem mclsssvlem

Description: Lemma for mclsssv . (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mclsval.d ⊢ 𝐷 = ( mDV ‘ 𝑇 )
mclsval.e ⊢ 𝐸 = ( mEx ‘ 𝑇 )
mclsval.c ⊢ 𝐶 = ( mCls ‘ 𝑇 )
mclsval.1 ⊢ ( 𝜑 → 𝑇 ∈ mFS )
mclsval.2 ⊢ ( 𝜑 → 𝐾 ⊆ 𝐷 )
mclsval.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐸 )
mclsval.h ⊢ 𝐻 = ( mVH ‘ 𝑇 )
mclsval.a ⊢ 𝐴 = ( mAx ‘ 𝑇 )
mclsval.s ⊢ 𝑆 = ( mSubst ‘ 𝑇 )
mclsval.v ⊢ 𝑉 = ( mVars ‘ 𝑇 )
Assertion mclsssvlem ( 𝜑 → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ 𝐸 )

Proof

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 mclsval.h ⊢ 𝐻 = ( mVH ‘ 𝑇 )
8 mclsval.a ⊢ 𝐴 = ( mAx ‘ 𝑇 )
9 mclsval.s ⊢ 𝑆 = ( mSubst ‘ 𝑇 )
10 mclsval.v ⊢ 𝑉 = ( mVars ‘ 𝑇 )
11 eqid ⊢ ( mVR ‘ 𝑇 ) = ( mVR ‘ 𝑇 )
12 11 2 7 mvhf ⊢ ( 𝑇 ∈ mFS → 𝐻 : ( mVR ‘ 𝑇 ) ⟶ 𝐸 )
13 4 12 syl ⊢ ( 𝜑 → 𝐻 : ( mVR ‘ 𝑇 ) ⟶ 𝐸 )
14 13 frnd ⊢ ( 𝜑 → ran 𝐻 ⊆ 𝐸 )
15 6 14 unssd ⊢ ( 𝜑 → ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝐸 )
16 9 2 msubf ⊢ ( 𝑠 ∈ ran 𝑆 → 𝑠 : 𝐸 ⟶ 𝐸 )
17 eqid ⊢ ( mStat ‘ 𝑇 ) = ( mStat ‘ 𝑇 )
18 8 17 maxsta ⊢ ( 𝑇 ∈ mFS → 𝐴 ⊆ ( mStat ‘ 𝑇 ) )
19 4 18 syl ⊢ ( 𝜑 → 𝐴 ⊆ ( mStat ‘ 𝑇 ) )
20 eqid ⊢ ( mPreSt ‘ 𝑇 ) = ( mPreSt ‘ 𝑇 )
21 20 17 mstapst ⊢ ( mStat ‘ 𝑇 ) ⊆ ( mPreSt ‘ 𝑇 )
22 19 21 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ( mPreSt ‘ 𝑇 ) )
23 22 sselda ⊢ ( ( 𝜑 ∧ ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ) → ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mPreSt ‘ 𝑇 ) )
24 1 2 20 elmpst ⊢ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mPreSt ‘ 𝑇 ) ↔ ( ( 𝑚 ⊆ 𝐷 ∧ ◡ 𝑚 = 𝑚 ) ∧ ( 𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin ) ∧ 𝑝 ∈ 𝐸 ) )
25 24 simp3bi ⊢ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mPreSt ‘ 𝑇 ) → 𝑝 ∈ 𝐸 )
26 23 25 syl ⊢ ( ( 𝜑 ∧ ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ) → 𝑝 ∈ 𝐸 )
27 ffvelrn ⊢ ( ( 𝑠 : 𝐸 ⟶ 𝐸 ∧ 𝑝 ∈ 𝐸 ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 )
28 16 26 27 syl2anr ⊢ ( ( ( 𝜑 ∧ ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ) ∧ 𝑠 ∈ ran 𝑆 ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 )
29 28 a1d ⊢ ( ( ( 𝜑 ∧ ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ) ∧ 𝑠 ∈ ran 𝑆 ) → ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) )
30 29 ralrimiva ⊢ ( ( 𝜑 ∧ ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ) → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) )
31 30 ex ⊢ ( 𝜑 → ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) ) )
32 31 alrimiv ⊢ ( 𝜑 → ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) ) )
33 32 alrimivv ⊢ ( 𝜑 → ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) ) )
34 2 fvexi ⊢ 𝐸 ∈ V
35 sseq2 ⊢ ( 𝑐 = 𝐸 → ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ↔ ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝐸 ) )
36 sseq2 ⊢ ( 𝑐 = 𝐸 → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ↔ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ) )
37 36 anbi1d ⊢ ( 𝑐 = 𝐸 → ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ↔ ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ) )
38 eleq2 ⊢ ( 𝑐 = 𝐸 → ( ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ↔ ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) )
39 37 38 imbi12d ⊢ ( 𝑐 = 𝐸 → ( ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ↔ ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) ) )
40 39 ralbidv ⊢ ( 𝑐 = 𝐸 → ( ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ↔ ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) ) )
41 40 imbi2d ⊢ ( 𝑐 = 𝐸 → ( ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) ) ) )
42 41 albidv ⊢ ( 𝑐 = 𝐸 → ( ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) ) ) )
43 42 2albidv ⊢ ( 𝑐 = 𝐸 → ( ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) ) ) )
44 35 43 anbi12d ⊢ ( 𝑐 = 𝐸 → ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ↔ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝐸 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) ) ) ) )
45 34 44 elab ⊢ ( 𝐸 ∈ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ↔ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝐸 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝐸 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ) ) ) )
46 15 33 45 sylanbrc ⊢ ( 𝜑 → 𝐸 ∈ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
47 intss1 ⊢ ( 𝐸 ∈ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ 𝐸 )
48 46 47 syl ⊢ ( 𝜑 → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ 𝐸 )