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 ⊢φ→KCB=⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→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→mop∈mAx⁡t↔mop∈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→so∪ran⁡mVH⁡t=so∪ran⁡H
31 30 sseq1d ⊢t=T→so∪ran⁡mVH⁡t⊆c↔so∪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→xmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d↔xmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d
43 42 2albidv ⊢t=T→∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d↔∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d
44 31 43 anbi12d ⊢t=T→so∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d↔so∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d
45 44 imbi1d ⊢t=T→so∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c↔so∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d→s⁡p∈c
46 28 45 raleqbidv ⊢t=T→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c↔∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d→s⁡p∈c
47 25 46 imbi12d ⊢t=T→mop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c↔mop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d→s⁡p∈c
48 47 albidv ⊢t=T→∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c↔∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d→s⁡p∈c
49 48 2albidv ⊢t=T→∀m∀o∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c↔∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→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∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c↔h∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→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∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c=c|h∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→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∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c=⋂c|h∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→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∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→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∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→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∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→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∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→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∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→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∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d→s⁡p∈c
62 3 61 eqtrid ⊢φ→C=d∈𝒫D,h∈𝒫E⟼⋂c|h∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→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→xmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d↔xmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K
69 68 2albidv ⊢φ∧d=K∧h=B→∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d↔∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K
70 69 anbi2d ⊢φ∧d=K∧h=B→so∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d↔so∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K
71 70 imbi1d ⊢φ∧d=K∧h=B→so∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d→s⁡p∈c↔so∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c
72 71 ralbidv ⊢φ∧d=K∧h=B→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d→s⁡p∈c↔∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c
73 72 imbi2d ⊢φ∧d=K∧h=B→mop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d→s⁡p∈c↔mop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c
74 73 albidv ⊢φ∧d=K∧h=B→∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d→s⁡p∈c↔∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c
75 74 2albidv ⊢φ∧d=K∧h=B→∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d→s⁡p∈c↔∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→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∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d→s⁡p∈c↔B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→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∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d→s⁡p∈c=c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→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∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆d→s⁡p∈c=⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→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∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c⊆E
84 57 ssex ⊢⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c⊆E→⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c∈V
85 83 84 syl ⊢φ→⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c∈V
86 62 78 80 82 85 ovmpod ⊢φ→KCB=⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c