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 ⊢ D = mDV ⁡ T
mclsval.e ⊢ E = mEx ⁡ T
mclsval.c ⊢ C = mCls ⁡ T
mclsval.1 ⊢ φ → T ∈ mFS
mclsval.2 ⊢ φ → K ⊆ D
mclsval.3 ⊢ φ → B ⊆ E
mclsval.h ⊢ H = mVH ⁡ T
mclsval.a ⊢ A = mAx ⁡ T
mclsval.s ⊢ S = mSubst ⁡ T
mclsval.v ⊢ V = mVars ⁡ T
Assertion mclsval ⊢ φ → K C B = ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c

Proof

Step Hyp Ref Expression
1 mclsval.d ⊢ D = mDV ⁡ T
2 mclsval.e ⊢ E = mEx ⁡ T
3 mclsval.c ⊢ C = mCls ⁡ T
4 mclsval.1 ⊢ φ → T ∈ mFS
5 mclsval.2 ⊢ φ → K ⊆ D
6 mclsval.3 ⊢ φ → B ⊆ E
7 mclsval.h ⊢ H = mVH ⁡ T
8 mclsval.a ⊢ A = mAx ⁡ T
9 mclsval.s ⊢ S = mSubst ⁡ T
10 mclsval.v ⊢ V = mVars ⁡ T
11 elex ⊢ T ∈ mFS → T ∈ V
12 fveq2 ⊢ t = T → mDV ⁡ t = mDV ⁡ T
13 12 1 eqtr4di ⊢ t = T → mDV ⁡ t = D
14 13 pweqd ⊢ t = T → 𝒫 mDV ⁡ t = 𝒫 D
15 fveq2 ⊢ t = T → mEx ⁡ t = mEx ⁡ T
16 15 2 eqtr4di ⊢ t = T → mEx ⁡ t = E
17 16 pweqd ⊢ t = T → 𝒫 mEx ⁡ t = 𝒫 E
18 fveq2 ⊢ t = T → mVH ⁡ t = mVH ⁡ T
19 18 7 eqtr4di ⊢ t = T → mVH ⁡ t = H
20 19 rneqd ⊢ t = T → ran ⁡ mVH ⁡ t = ran ⁡ H
21 20 uneq2d ⊢ t = T → h ∪ ran ⁡ mVH ⁡ t = h ∪ ran ⁡ H
22 21 sseq1d ⊢ t = T → h ∪ ran ⁡ mVH ⁡ t ⊆ c ↔ h ∪ ran ⁡ H ⊆ c
23 fveq2 ⊢ t = T → mAx ⁡ t = mAx ⁡ T
24 23 8 eqtr4di ⊢ t = T → mAx ⁡ t = A
25 24 eleq2d ⊢ t = T → m o p ∈ mAx ⁡ t ↔ m o p ∈ A
26 fveq2 ⊢ t = T → mSubst ⁡ t = mSubst ⁡ T
27 26 9 eqtr4di ⊢ t = T → mSubst ⁡ t = S
28 27 rneqd ⊢ t = T → ran ⁡ mSubst ⁡ t = ran ⁡ S
29 20 uneq2d ⊢ t = T → o ∪ ran ⁡ mVH ⁡ t = o ∪ ran ⁡ H
30 29 imaeq2d ⊢ t = T → s o ∪ ran ⁡ mVH ⁡ t = s o ∪ ran ⁡ H
31 30 sseq1d ⊢ t = T → s o ∪ ran ⁡ mVH ⁡ t ⊆ c ↔ s o ∪ ran ⁡ H ⊆ c
32 fveq2 ⊢ t = T → mVars ⁡ t = mVars ⁡ T
33 32 10 eqtr4di ⊢ t = T → mVars ⁡ t = V
34 19 fveq1d ⊢ t = T → mVH ⁡ t ⁡ x = H ⁡ x
35 34 fveq2d ⊢ t = T → s ⁡ mVH ⁡ t ⁡ x = s ⁡ H ⁡ x
36 33 35 fveq12d ⊢ t = T → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x = V ⁡ s ⁡ H ⁡ x
37 19 fveq1d ⊢ t = T → mVH ⁡ t ⁡ y = H ⁡ y
38 37 fveq2d ⊢ t = T → s ⁡ mVH ⁡ t ⁡ y = s ⁡ H ⁡ y
39 33 38 fveq12d ⊢ t = T → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y = V ⁡ s ⁡ H ⁡ y
40 36 39 xpeq12d ⊢ t = T → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y = V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y
41 40 sseq1d ⊢ t = T → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d ↔ V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d
42 41 imbi2d ⊢ t = T → x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d ↔ x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d
43 42 2albidv ⊢ t = T → ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d ↔ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d
44 31 43 anbi12d ⊢ t = T → s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d ↔ s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d
45 44 imbi1d ⊢ t = T → s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c ↔ s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c
46 28 45 raleqbidv ⊢ t = T → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c ↔ ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c
47 25 46 imbi12d ⊢ t = T → m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c ↔ m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c
48 47 albidv ⊢ t = T → ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c ↔ ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c
49 48 2albidv ⊢ t = T → ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c ↔ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c
50 22 49 anbi12d ⊢ t = T → h ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c ↔ h ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c
51 50 abbidv ⊢ t = T → c | h ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c = c | h ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c
52 51 inteqd ⊢ t = T → ⋂ c | h ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c = ⋂ c | h ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c
53 14 17 52 mpoeq123dv ⊢ t = T → d ∈ 𝒫 mDV ⁡ t , h ∈ 𝒫 mEx ⁡ t ⟼ ⋂ c | h ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c = d ∈ 𝒫 D , h ∈ 𝒫 E ⟼ ⋂ c | h ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c
54 df-mcls ⊢ mCls = t ∈ V ⟼ d ∈ 𝒫 mDV ⁡ t , h ∈ 𝒫 mEx ⁡ t ⟼ ⋂ c | h ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c
55 1 fvexi ⊢ D ∈ V
56 55 pwex ⊢ 𝒫 D ∈ V
57 2 fvexi ⊢ E ∈ V
58 57 pwex ⊢ 𝒫 E ∈ V
59 56 58 mpoex ⊢ d ∈ 𝒫 D , h ∈ 𝒫 E ⟼ ⋂ c | h ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c ∈ V
60 53 54 59 fvmpt ⊢ T ∈ V → mCls ⁡ T = d ∈ 𝒫 D , h ∈ 𝒫 E ⟼ ⋂ c | h ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c
61 4 11 60 3syl ⊢ φ → mCls ⁡ T = d ∈ 𝒫 D , h ∈ 𝒫 E ⟼ ⋂ c | h ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c
62 3 61 syl5eq ⊢ φ → C = d ∈ 𝒫 D , h ∈ 𝒫 E ⟼ ⋂ c | h ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c
63 simprr ⊢ φ ∧ d = K ∧ h = B → h = B
64 63 uneq1d ⊢ φ ∧ d = K ∧ h = B → h ∪ ran ⁡ H = B ∪ ran ⁡ H
65 64 sseq1d ⊢ φ ∧ d = K ∧ h = B → h ∪ ran ⁡ H ⊆ c ↔ B ∪ ran ⁡ H ⊆ c
66 simprl ⊢ φ ∧ d = K ∧ h = B → d = K
67 66 sseq2d ⊢ φ ∧ d = K ∧ h = B → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d ↔ V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K
68 67 imbi2d ⊢ φ ∧ d = K ∧ h = B → x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d ↔ x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K
69 68 2albidv ⊢ φ ∧ d = K ∧ h = B → ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d ↔ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K
70 69 anbi2d ⊢ φ ∧ d = K ∧ h = B → s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d ↔ s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K
71 70 imbi1d ⊢ φ ∧ d = K ∧ h = B → s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c ↔ s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
72 71 ralbidv ⊢ φ ∧ d = K ∧ h = B → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c ↔ ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
73 72 imbi2d ⊢ φ ∧ d = K ∧ h = B → m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c ↔ m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
74 73 albidv ⊢ φ ∧ d = K ∧ h = B → ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c ↔ ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
75 74 2albidv ⊢ φ ∧ d = K ∧ h = B → ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c ↔ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
76 65 75 anbi12d ⊢ φ ∧ d = K ∧ h = B → h ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c ↔ B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
77 76 abbidv ⊢ φ ∧ d = K ∧ h = B → c | h ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c = c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
78 77 inteqd ⊢ φ ∧ d = K ∧ h = B → ⋂ c | h ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ d → s ⁡ p ∈ c = ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
79 55 elpw2 ⊢ K ∈ 𝒫 D ↔ K ⊆ D
80 5 79 sylibr ⊢ φ → K ∈ 𝒫 D
81 57 elpw2 ⊢ B ∈ 𝒫 E ↔ B ⊆ E
82 6 81 sylibr ⊢ φ → B ∈ 𝒫 E
83 1 2 3 4 5 6 7 8 9 10 mclsssvlem ⊢ φ → ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ⊆ E
84 57 ssex ⊢ ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ⊆ E → ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ∈ V
85 83 84 syl ⊢ φ → ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ∈ V
86 62 78 80 82 85 ovmpod ⊢ φ → K C B = ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c