Metamath Proof Explorer

Theorem mclsax

Description: The closure is closed under axiom application. (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 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐸 )
mclsax.a ⊢ 𝐴 = ( mAx ‘ 𝑇 )
mclsax.l ⊢ 𝐿 = ( mSubst ‘ 𝑇 )
mclsax.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
mclsax.h ⊢ 𝐻 = ( mVH ‘ 𝑇 )
mclsax.w ⊢ 𝑊 = ( mVars ‘ 𝑇 )
mclsax.4 ⊢ ( 𝜑 → ⟨ 𝑀 , 𝑂 , 𝑃 ⟩ ∈ 𝐴 )
mclsax.5 ⊢ ( 𝜑 → 𝑆 ∈ ran 𝐿 )
mclsax.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) )
mclsax.7 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐾 𝐶 𝐵 ) )
mclsax.8 ⊢ ( ( 𝜑 ∧ ( 𝑥 𝑀 𝑦 ∧ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ) → 𝑎 𝐾 𝑏 )
Assertion mclsax ( 𝜑 → ( 𝑆 ‘ 𝑃 ) ∈ ( 𝐾 𝐶 𝐵 ) )

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 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 imbitrrid ⊢ ( 𝜑 → ( ( ( 𝐵 ∪ 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 sselid ⊢ ( 𝜑 → ⟨ 𝑀 , 𝑂 , 𝑃 ⟩ ∈ ( 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 ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑃 ) ∈ ( 𝐾 𝐶 𝐵 ) )