Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mclsval Structured version   Visualization version   GIF version

Theorem mclsval 33969
Description: The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
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
Ref Expression
mclsval (πœ‘ β†’ (𝐾𝐢𝐡) = ∩ {𝑐 ∣ ((𝐡 βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))})
Distinct variable groups:   π‘š,𝑐,π‘œ,𝑝,𝑠,𝐸   π‘₯,𝑐,𝐻,π‘š,π‘œ,𝑝,𝑠   𝑦,𝑐,𝐡,π‘š,π‘œ,𝑝,𝑠,π‘₯   𝐢,π‘š,π‘œ,𝑝,𝑠,π‘₯   𝐴,𝑐,π‘š,π‘œ,𝑝,𝑠   𝑆,𝑐,𝑠,π‘₯,𝑦   𝑇,𝑐,π‘š,π‘œ,𝑝,𝑠,π‘₯,𝑦   πœ‘,𝑐,π‘š,π‘œ,𝑝,𝑠,π‘₯,𝑦   𝑉,𝑐,π‘₯   𝐾,𝑐,π‘š,π‘œ,𝑝,𝑠,π‘₯,𝑦
Allowed substitution hints:   𝐴(π‘₯,𝑦)   𝐢(𝑦,𝑐)   𝐷(π‘₯,𝑦,π‘š,π‘œ,𝑠,𝑝,𝑐)   𝑆(π‘š,π‘œ,𝑝)   𝐸(π‘₯,𝑦)   𝐻(𝑦)   𝑉(𝑦,π‘š,π‘œ,𝑠,𝑝)

Proof of Theorem mclsval
Dummy variables β„Ž 𝑑 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mclsval.c . . 3 𝐢 = (mClsβ€˜π‘‡)
2 mclsval.1 . . . 4 (πœ‘ β†’ 𝑇 ∈ mFS)
3 elex 3461 . . . 4 (𝑇 ∈ mFS β†’ 𝑇 ∈ V)
4 fveq2 6839 . . . . . . . 8 (𝑑 = 𝑇 β†’ (mDVβ€˜π‘‘) = (mDVβ€˜π‘‡))
5 mclsval.d . . . . . . . 8 𝐷 = (mDVβ€˜π‘‡)
64, 5eqtr4di 2795 . . . . . . 7 (𝑑 = 𝑇 β†’ (mDVβ€˜π‘‘) = 𝐷)
76pweqd 4575 . . . . . 6 (𝑑 = 𝑇 β†’ 𝒫 (mDVβ€˜π‘‘) = 𝒫 𝐷)
8 fveq2 6839 . . . . . . . 8 (𝑑 = 𝑇 β†’ (mExβ€˜π‘‘) = (mExβ€˜π‘‡))
9 mclsval.e . . . . . . . 8 𝐸 = (mExβ€˜π‘‡)
108, 9eqtr4di 2795 . . . . . . 7 (𝑑 = 𝑇 β†’ (mExβ€˜π‘‘) = 𝐸)
1110pweqd 4575 . . . . . 6 (𝑑 = 𝑇 β†’ 𝒫 (mExβ€˜π‘‘) = 𝒫 𝐸)
12 fveq2 6839 . . . . . . . . . . . . 13 (𝑑 = 𝑇 β†’ (mVHβ€˜π‘‘) = (mVHβ€˜π‘‡))
13 mclsval.h . . . . . . . . . . . . 13 𝐻 = (mVHβ€˜π‘‡)
1412, 13eqtr4di 2795 . . . . . . . . . . . 12 (𝑑 = 𝑇 β†’ (mVHβ€˜π‘‘) = 𝐻)
1514rneqd 5891 . . . . . . . . . . 11 (𝑑 = 𝑇 β†’ ran (mVHβ€˜π‘‘) = ran 𝐻)
1615uneq2d 4121 . . . . . . . . . 10 (𝑑 = 𝑇 β†’ (β„Ž βˆͺ ran (mVHβ€˜π‘‘)) = (β„Ž βˆͺ ran 𝐻))
1716sseq1d 3973 . . . . . . . . 9 (𝑑 = 𝑇 β†’ ((β„Ž βˆͺ ran (mVHβ€˜π‘‘)) βŠ† 𝑐 ↔ (β„Ž βˆͺ ran 𝐻) βŠ† 𝑐))
18 fveq2 6839 . . . . . . . . . . . . . 14 (𝑑 = 𝑇 β†’ (mAxβ€˜π‘‘) = (mAxβ€˜π‘‡))
19 mclsval.a . . . . . . . . . . . . . 14 𝐴 = (mAxβ€˜π‘‡)
2018, 19eqtr4di 2795 . . . . . . . . . . . . 13 (𝑑 = 𝑇 β†’ (mAxβ€˜π‘‘) = 𝐴)
2120eleq2d 2823 . . . . . . . . . . . 12 (𝑑 = 𝑇 β†’ (βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) ↔ βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴))
22 fveq2 6839 . . . . . . . . . . . . . . 15 (𝑑 = 𝑇 β†’ (mSubstβ€˜π‘‘) = (mSubstβ€˜π‘‡))
23 mclsval.s . . . . . . . . . . . . . . 15 𝑆 = (mSubstβ€˜π‘‡)
2422, 23eqtr4di 2795 . . . . . . . . . . . . . 14 (𝑑 = 𝑇 β†’ (mSubstβ€˜π‘‘) = 𝑆)
2524rneqd 5891 . . . . . . . . . . . . 13 (𝑑 = 𝑇 β†’ ran (mSubstβ€˜π‘‘) = ran 𝑆)
2615uneq2d 4121 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑇 β†’ (π‘œ βˆͺ ran (mVHβ€˜π‘‘)) = (π‘œ βˆͺ ran 𝐻))
2726imaeq2d 6011 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑇 β†’ (𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) = (𝑠 β€œ (π‘œ βˆͺ ran 𝐻)))
2827sseq1d 3973 . . . . . . . . . . . . . . 15 (𝑑 = 𝑇 β†’ ((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ↔ (𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐))
29 fveq2 6839 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑇 β†’ (mVarsβ€˜π‘‘) = (mVarsβ€˜π‘‡))
30 mclsval.v . . . . . . . . . . . . . . . . . . . . 21 𝑉 = (mVarsβ€˜π‘‡)
3129, 30eqtr4di 2795 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑇 β†’ (mVarsβ€˜π‘‘) = 𝑉)
3214fveq1d 6841 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑇 β†’ ((mVHβ€˜π‘‘)β€˜π‘₯) = (π»β€˜π‘₯))
3332fveq2d 6843 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑇 β†’ (π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯)) = (π‘ β€˜(π»β€˜π‘₯)))
3431, 33fveq12d 6846 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑇 β†’ ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) = (π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))))
3514fveq1d 6841 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑇 β†’ ((mVHβ€˜π‘‘)β€˜π‘¦) = (π»β€˜π‘¦))
3635fveq2d 6843 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑇 β†’ (π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)) = (π‘ β€˜(π»β€˜π‘¦)))
3731, 36fveq12d 6846 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑇 β†’ ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦))) = (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦))))
3834, 37xpeq12d 5662 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑇 β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) = ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))))
3938sseq1d 3973 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑇 β†’ ((((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑 ↔ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑))
4039imbi2d 340 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑇 β†’ ((π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑) ↔ (π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)))
41402albidv 1926 . . . . . . . . . . . . . . 15 (𝑑 = 𝑇 β†’ (βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑) ↔ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)))
4228, 41anbi12d 631 . . . . . . . . . . . . . 14 (𝑑 = 𝑇 β†’ (((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) ↔ ((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑))))
4342imbi1d 341 . . . . . . . . . . . . 13 (𝑑 = 𝑇 β†’ ((((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐) ↔ (((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))
4425, 43raleqbidv 3317 . . . . . . . . . . . 12 (𝑑 = 𝑇 β†’ (βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐) ↔ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))
4521, 44imbi12d 344 . . . . . . . . . . 11 (𝑑 = 𝑇 β†’ ((βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)) ↔ (βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐))))
4645albidv 1923 . . . . . . . . . 10 (𝑑 = 𝑇 β†’ (βˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)) ↔ βˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐))))
47462albidv 1926 . . . . . . . . 9 (𝑑 = 𝑇 β†’ (βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)) ↔ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐))))
4817, 47anbi12d 631 . . . . . . . 8 (𝑑 = 𝑇 β†’ (((β„Ž βˆͺ ran (mVHβ€˜π‘‘)) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐))) ↔ ((β„Ž βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))))
4948abbidv 2806 . . . . . . 7 (𝑑 = 𝑇 β†’ {𝑐 ∣ ((β„Ž βˆͺ ran (mVHβ€˜π‘‘)) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))} = {𝑐 ∣ ((β„Ž βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))})
5049inteqd 4910 . . . . . 6 (𝑑 = 𝑇 β†’ ∩ {𝑐 ∣ ((β„Ž βˆͺ ran (mVHβ€˜π‘‘)) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))} = ∩ {𝑐 ∣ ((β„Ž βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))})
517, 11, 50mpoeq123dv 7426 . . . . 5 (𝑑 = 𝑇 β†’ (𝑑 ∈ 𝒫 (mDVβ€˜π‘‘), β„Ž ∈ 𝒫 (mExβ€˜π‘‘) ↦ ∩ {𝑐 ∣ ((β„Ž βˆͺ ran (mVHβ€˜π‘‘)) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))}) = (𝑑 ∈ 𝒫 𝐷, β„Ž ∈ 𝒫 𝐸 ↦ ∩ {𝑐 ∣ ((β„Ž βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))}))
52 df-mcls 33903 . . . . 5 mCls = (𝑑 ∈ V ↦ (𝑑 ∈ 𝒫 (mDVβ€˜π‘‘), β„Ž ∈ 𝒫 (mExβ€˜π‘‘) ↦ ∩ {𝑐 ∣ ((β„Ž βˆͺ ran (mVHβ€˜π‘‘)) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))}))
535fvexi 6853 . . . . . . 7 𝐷 ∈ V
5453pwex 5333 . . . . . 6 𝒫 𝐷 ∈ V
559fvexi 6853 . . . . . . 7 𝐸 ∈ V
5655pwex 5333 . . . . . 6 𝒫 𝐸 ∈ V
5754, 56mpoex 8004 . . . . 5 (𝑑 ∈ 𝒫 𝐷, β„Ž ∈ 𝒫 𝐸 ↦ ∩ {𝑐 ∣ ((β„Ž βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))}) ∈ V
5851, 52, 57fvmpt 6945 . . . 4 (𝑇 ∈ V β†’ (mClsβ€˜π‘‡) = (𝑑 ∈ 𝒫 𝐷, β„Ž ∈ 𝒫 𝐸 ↦ ∩ {𝑐 ∣ ((β„Ž βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))}))
592, 3, 583syl 18 . . 3 (πœ‘ β†’ (mClsβ€˜π‘‡) = (𝑑 ∈ 𝒫 𝐷, β„Ž ∈ 𝒫 𝐸 ↦ ∩ {𝑐 ∣ ((β„Ž βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))}))
601, 59eqtrid 2789 . 2 (πœ‘ β†’ 𝐢 = (𝑑 ∈ 𝒫 𝐷, β„Ž ∈ 𝒫 𝐸 ↦ ∩ {𝑐 ∣ ((β„Ž βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))}))
61 simprr 771 . . . . . . 7 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ β„Ž = 𝐡)
6261uneq1d 4120 . . . . . 6 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ (β„Ž βˆͺ ran 𝐻) = (𝐡 βˆͺ ran 𝐻))
6362sseq1d 3973 . . . . 5 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ ((β„Ž βˆͺ ran 𝐻) βŠ† 𝑐 ↔ (𝐡 βˆͺ ran 𝐻) βŠ† 𝑐))
64 simprl 769 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ 𝑑 = 𝐾)
6564sseq2d 3974 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ (((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑 ↔ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾))
6665imbi2d 340 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ ((π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑) ↔ (π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)))
67662albidv 1926 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ (βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑) ↔ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)))
6867anbi2d 629 . . . . . . . . . 10 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ (((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) ↔ ((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾))))
6968imbi1d 341 . . . . . . . . 9 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ ((((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐) ↔ (((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))
7069ralbidv 3172 . . . . . . . 8 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ (βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐) ↔ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))
7170imbi2d 340 . . . . . . 7 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ ((βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)) ↔ (βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐))))
7271albidv 1923 . . . . . 6 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ (βˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)) ↔ βˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐))))
73722albidv 1926 . . . . 5 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ (βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)) ↔ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐))))
7463, 73anbi12d 631 . . . 4 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ (((β„Ž βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐))) ↔ ((𝐡 βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))))
7574abbidv 2806 . . 3 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ {𝑐 ∣ ((β„Ž βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))} = {𝑐 ∣ ((𝐡 βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))})
7675inteqd 4910 . 2 ((πœ‘ ∧ (𝑑 = 𝐾 ∧ β„Ž = 𝐡)) β†’ ∩ {𝑐 ∣ ((β„Ž βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))} = ∩ {𝑐 ∣ ((𝐡 βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))})
77 mclsval.2 . . 3 (πœ‘ β†’ 𝐾 βŠ† 𝐷)
7853elpw2 5300 . . 3 (𝐾 ∈ 𝒫 𝐷 ↔ 𝐾 βŠ† 𝐷)
7977, 78sylibr 233 . 2 (πœ‘ β†’ 𝐾 ∈ 𝒫 𝐷)
80 mclsval.3 . . 3 (πœ‘ β†’ 𝐡 βŠ† 𝐸)
8155elpw2 5300 . . 3 (𝐡 ∈ 𝒫 𝐸 ↔ 𝐡 βŠ† 𝐸)
8280, 81sylibr 233 . 2 (πœ‘ β†’ 𝐡 ∈ 𝒫 𝐸)
835, 9, 1, 2, 77, 80, 13, 19, 23, 30mclsssvlem 33968 . . 3 (πœ‘ β†’ ∩ {𝑐 ∣ ((𝐡 βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))} βŠ† 𝐸)
8455ssex 5276 . . 3 (∩ {𝑐 ∣ ((𝐡 βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))} βŠ† 𝐸 β†’ ∩ {𝑐 ∣ ((𝐡 βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))} ∈ V)
8583, 84syl 17 . 2 (πœ‘ β†’ ∩ {𝑐 ∣ ((𝐡 βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))} ∈ V)
8660, 76, 79, 82, 85ovmpod 7501 1 (πœ‘ β†’ (𝐾𝐢𝐡) = ∩ {𝑐 ∣ ((𝐡 βˆͺ ran 𝐻) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ 𝐴 β†’ βˆ€π‘  ∈ ran 𝑆(((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ ((π‘‰β€˜(π‘ β€˜(π»β€˜π‘₯))) Γ— (π‘‰β€˜(π‘ β€˜(π»β€˜π‘¦)))) βŠ† 𝐾)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396  βˆ€wal 1539   = wceq 1541   ∈ wcel 2106  {cab 2714  βˆ€wral 3062  Vcvv 3443   βˆͺ cun 3906   βŠ† wss 3908  π’« cpw 4558  βŸ¨cotp 4592  βˆ© cint 4905   class class class wbr 5103   Γ— cxp 5629  ran crn 5632   β€œ cima 5634  β€˜cfv 6493  (class class class)co 7351   ∈ cmpo 7353  mAxcmax 33871  mExcmex 33873  mDVcmdv 33874  mVarscmvrs 33875  mSubstcmsub 33877  mVHcmvh 33878  mFScmfs 33882  mClscmcls 33883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-ot 4593  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7307  df-ov 7354  df-oprab 7355  df-mpo 7356  df-om 7795  df-1st 7913  df-2nd 7914  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-rdg 8348  df-1o 8404  df-er 8606  df-map 8725  df-pm 8726  df-en 8842  df-dom 8843  df-sdom 8844  df-fin 8845  df-card 9833  df-pnf 11149  df-mnf 11150  df-xr 11151  df-ltxr 11152  df-le 11153  df-sub 11345  df-neg 11346  df-nn 12112  df-2 12174  df-n0 12372  df-z 12458  df-uz 12722  df-fz 13379  df-fzo 13522  df-seq 13861  df-hash 14185  df-word 14357  df-concat 14413  df-s1 14438  df-struct 16979  df-sets 16996  df-slot 17014  df-ndx 17026  df-base 17044  df-ress 17073  df-plusg 17106  df-0g 17283  df-gsum 17284  df-mgm 18457  df-sgrp 18506  df-mnd 18517  df-submnd 18562  df-frmd 18619  df-mrex 33892  df-mex 33893  df-mrsub 33896  df-msub 33897  df-mvh 33898  df-mpst 33899  df-msr 33900  df-msta 33901  df-mfs 33902  df-mcls 33903
This theorem is referenced by:  mclsssv  33970  ssmclslem  33971  ss2mcls  33974  mclsax  33975  mclsind  33976
  Copyright terms: Public domain W3C validator