Metamath Proof Explorer

Theorem mclsval

Description: The function mapping variables to variable expressions is one-to-one. (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 mclsval ( 𝜑 → ( 𝐾 𝐶 𝐵 ) = ∩ { 𝑐 ∣ ( ( 𝐵 ∪ 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 elex ⊢ ( 𝑇 ∈ mFS → 𝑇 ∈ V )
12 fveq2 ⊢ ( 𝑡 = 𝑇 → ( mDV ‘ 𝑡 ) = ( mDV ‘ 𝑇 ) )
13 12 1 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( mDV ‘ 𝑡 ) = 𝐷 )
14 13 pweqd ⊢ ( 𝑡 = 𝑇 → 𝒫 ( mDV ‘ 𝑡 ) = 𝒫 𝐷 )
15 fveq2 ⊢ ( 𝑡 = 𝑇 → ( mEx ‘ 𝑡 ) = ( mEx ‘ 𝑇 ) )
16 15 2 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( mEx ‘ 𝑡 ) = 𝐸 )
17 16 pweqd ⊢ ( 𝑡 = 𝑇 → 𝒫 ( mEx ‘ 𝑡 ) = 𝒫 𝐸 )
18 fveq2 ⊢ ( 𝑡 = 𝑇 → ( mVH ‘ 𝑡 ) = ( mVH ‘ 𝑇 ) )
19 18 7 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( mVH ‘ 𝑡 ) = 𝐻 )
20 19 rneqd ⊢ ( 𝑡 = 𝑇 → ran ( mVH ‘ 𝑡 ) = ran 𝐻 )
21 20 uneq2d ⊢ ( 𝑡 = 𝑇 → ( ℎ ∪ ran ( mVH ‘ 𝑡 ) ) = ( ℎ ∪ ran 𝐻 ) )
22 21 sseq1d ⊢ ( 𝑡 = 𝑇 → ( ( ℎ ∪ ran ( mVH ‘ 𝑡 ) ) ⊆ 𝑐 ↔ ( ℎ ∪ ran 𝐻 ) ⊆ 𝑐 ) )
23 fveq2 ⊢ ( 𝑡 = 𝑇 → ( mAx ‘ 𝑡 ) = ( mAx ‘ 𝑇 ) )
24 23 8 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( mAx ‘ 𝑡 ) = 𝐴 )
25 24 eleq2d ⊢ ( 𝑡 = 𝑇 → ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) ↔ ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ) )
26 fveq2 ⊢ ( 𝑡 = 𝑇 → ( mSubst ‘ 𝑡 ) = ( mSubst ‘ 𝑇 ) )
27 26 9 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( mSubst ‘ 𝑡 ) = 𝑆 )
28 27 rneqd ⊢ ( 𝑡 = 𝑇 → ran ( mSubst ‘ 𝑡 ) = ran 𝑆 )
29 20 uneq2d ⊢ ( 𝑡 = 𝑇 → ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) = ( 𝑜 ∪ ran 𝐻 ) )
30 29 imaeq2d ⊢ ( 𝑡 = 𝑇 → ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) = ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) )
31 30 sseq1d ⊢ ( 𝑡 = 𝑇 → ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ↔ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ) )
32 fveq2 ⊢ ( 𝑡 = 𝑇 → ( mVars ‘ 𝑡 ) = ( mVars ‘ 𝑇 ) )
33 32 10 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( mVars ‘ 𝑡 ) = 𝑉 )
34 19 fveq1d ⊢ ( 𝑡 = 𝑇 → ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
35 34 fveq2d ⊢ ( 𝑡 = 𝑇 → ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) = ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) )
36 33 35 fveq12d ⊢ ( 𝑡 = 𝑇 → ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) = ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
37 19 fveq1d ⊢ ( 𝑡 = 𝑇 → ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) )
38 37 fveq2d ⊢ ( 𝑡 = 𝑇 → ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) = ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) )
39 33 38 fveq12d ⊢ ( 𝑡 = 𝑇 → ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) = ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) )
40 36 39 xpeq12d ⊢ ( 𝑡 = 𝑇 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) = ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) )
41 40 sseq1d ⊢ ( 𝑡 = 𝑇 → ( ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ↔ ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) )
42 41 imbi2d ⊢ ( 𝑡 = 𝑇 → ( ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ↔ ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) )
43 42 2albidv ⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) )
44 31 43 anbi12d ⊢ ( 𝑡 = 𝑇 → ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) ↔ ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) ) )
45 44 imbi1d ⊢ ( 𝑡 = 𝑇 → ( ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ↔ ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) )
46 28 45 raleqbidv ⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ↔ ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) )
47 25 46 imbi12d ⊢ ( 𝑡 = 𝑇 → ( ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) )
48 47 albidv ⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) )
49 48 2albidv ⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) )
50 22 49 anbi12d ⊢ ( 𝑡 = 𝑇 → ( ( ( ℎ ∪ ran ( mVH ‘ 𝑡 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ↔ ( ( ℎ ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ) )
51 50 abbidv ⊢ ( 𝑡 = 𝑇 → { 𝑐 ∣ ( ( ℎ ∪ ran ( mVH ‘ 𝑡 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } = { 𝑐 ∣ ( ( ℎ ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
52 51 inteqd ⊢ ( 𝑡 = 𝑇 → ∩ { 𝑐 ∣ ( ( ℎ ∪ ran ( mVH ‘ 𝑡 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } = ∩ { 𝑐 ∣ ( ( ℎ ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
53 14 17 52 mpoeq123dv ⊢ ( 𝑡 = 𝑇 → ( 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) , ℎ ∈ 𝒫 ( mEx ‘ 𝑡 ) ↦ ∩ { 𝑐 ∣ ( ( ℎ ∪ ran ( mVH ‘ 𝑡 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) = ( 𝑑 ∈ 𝒫 𝐷 , ℎ ∈ 𝒫 𝐸 ↦ ∩ { 𝑐 ∣ ( ( ℎ ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) )
54 df-mcls ⊢ mCls = ( 𝑡 ∈ V ↦ ( 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) , ℎ ∈ 𝒫 ( mEx ‘ 𝑡 ) ↦ ∩ { 𝑐 ∣ ( ( ℎ ∪ ran ( mVH ‘ 𝑡 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) )
55 1 fvexi ⊢ 𝐷 ∈ V
56 55 pwex ⊢ 𝒫 𝐷 ∈ V
57 2 fvexi ⊢ 𝐸 ∈ V
58 57 pwex ⊢ 𝒫 𝐸 ∈ V
59 56 58 mpoex ⊢ ( 𝑑 ∈ 𝒫 𝐷 , ℎ ∈ 𝒫 𝐸 ↦ ∩ { 𝑐 ∣ ( ( ℎ ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) ∈ V
60 53 54 59 fvmpt ⊢ ( 𝑇 ∈ V → ( mCls ‘ 𝑇 ) = ( 𝑑 ∈ 𝒫 𝐷 , ℎ ∈ 𝒫 𝐸 ↦ ∩ { 𝑐 ∣ ( ( ℎ ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) )
61 4 11 60 3syl ⊢ ( 𝜑 → ( mCls ‘ 𝑇 ) = ( 𝑑 ∈ 𝒫 𝐷 , ℎ ∈ 𝒫 𝐸 ↦ ∩ { 𝑐 ∣ ( ( ℎ ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) )
62 3 61 eqtrid ⊢ ( 𝜑 → 𝐶 = ( 𝑑 ∈ 𝒫 𝐷 , ℎ ∈ 𝒫 𝐸 ↦ ∩ { 𝑐 ∣ ( ( ℎ ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) )
63 simprr ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ℎ = 𝐵 )
64 63 uneq1d ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ( ℎ ∪ ran 𝐻 ) = ( 𝐵 ∪ ran 𝐻 ) )
65 64 sseq1d ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ( ( ℎ ∪ ran 𝐻 ) ⊆ 𝑐 ↔ ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ) )
66 simprl ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → 𝑑 = 𝐾 )
67 66 sseq2d ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ( ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ↔ ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) )
68 67 imbi2d ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ( ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ↔ ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) )
69 68 2albidv ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) )
70 69 anbi2d ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) ↔ ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ) )
71 70 imbi1d ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ( ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ↔ ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) )
72 71 ralbidv ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ( ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ↔ ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) )
73 72 imbi2d ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ( ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) )
74 73 albidv ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ( ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) )
75 74 2albidv ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ( ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) )
76 65 75 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ( ( ( ℎ ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ↔ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ) )
77 76 abbidv ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → { 𝑐 ∣ ( ( ℎ ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } = { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
78 77 inteqd ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐾 ∧ ℎ = 𝐵 ) ) → ∩ { 𝑐 ∣ ( ( ℎ ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } = ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
79 55 elpw2 ⊢ ( 𝐾 ∈ 𝒫 𝐷 ↔ 𝐾 ⊆ 𝐷 )
80 5 79 sylibr ⊢ ( 𝜑 → 𝐾 ∈ 𝒫 𝐷 )
81 57 elpw2 ⊢ ( 𝐵 ∈ 𝒫 𝐸 ↔ 𝐵 ⊆ 𝐸 )
82 6 81 sylibr ⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝐸 )
83 1 2 3 4 5 6 7 8 9 10 mclsssvlem ⊢ ( 𝜑 → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ 𝐸 )
84 57 ssex ⊢ ( ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ 𝐸 → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ∈ V )
85 83 84 syl ⊢ ( 𝜑 → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ∈ V )
86 62 78 80 82 85 ovmpod ⊢ ( 𝜑 → ( 𝐾 𝐶 𝐵 ) = ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝑆 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑉 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )