Theorem dilsetN

Description: The set of dilations for a fiducial atom D . (Contributed by NM, 4-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dilset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dilset.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
	dilset.w	$$⊢W=\mathrm{WAtoms}\left(K\right)$$
	dilset.m	$$⊢M=\mathrm{PAut}\left(K\right)$$
	dilset.l	$$⊢L=\mathrm{Dil}\left(K\right)$$
Assertion	dilsetN	$$⊢\left(K\in B\wedge D\in A\right)\to L\left(D\right)=\left\{f\in M|\forall x\in S\left(x\subseteq W\left(D\right)\to f\left(x\right)=x\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dilset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		dilset.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
3		dilset.w	$$⊢W=\mathrm{WAtoms}\left(K\right)$$
4		dilset.m	$$⊢M=\mathrm{PAut}\left(K\right)$$
5		dilset.l	$$⊢L=\mathrm{Dil}\left(K\right)$$
6	1 2 3 4 5	dilfsetN	$$⊢K\in B\to L=\left(d\in A⟼\left\{f\in M|\forall x\in S\left(x\subseteq W\left(d\right)\to f\left(x\right)=x\right)\right\}\right)$$
7	6	fveq1d	$$⊢K\in B\to L\left(D\right)=\left(d\in A⟼\left\{f\in M|\forall x\in S\left(x\subseteq W\left(d\right)\to f\left(x\right)=x\right)\right\}\right)\left(D\right)$$
8		fveq2	$$⊢d=D\to W\left(d\right)=W\left(D\right)$$
9	8	sseq2d	$$⊢d=D\to \left(x\subseteq W\left(d\right)\leftrightarrow x\subseteq W\left(D\right)\right)$$
10	9	imbi1d	$$⊢d=D\to \left(\left(x\subseteq W\left(d\right)\to f\left(x\right)=x\right)\leftrightarrow \left(x\subseteq W\left(D\right)\to f\left(x\right)=x\right)\right)$$
11	10	ralbidv	$$⊢d=D\to \left(\forall x\in S\left(x\subseteq W\left(d\right)\to f\left(x\right)=x\right)\leftrightarrow \forall x\in S\left(x\subseteq W\left(D\right)\to f\left(x\right)=x\right)\right)$$
12	11	rabbidv	$$⊢d=D\to \left\{f\in M|\forall x\in S\left(x\subseteq W\left(d\right)\to f\left(x\right)=x\right)\right\}=\left\{f\in M|\forall x\in S\left(x\subseteq W\left(D\right)\to f\left(x\right)=x\right)\right\}$$
13		eqid	$$⊢\left(d\in A⟼\left\{f\in M|\forall x\in S\left(x\subseteq W\left(d\right)\to f\left(x\right)=x\right)\right\}\right)=\left(d\in A⟼\left\{f\in M|\forall x\in S\left(x\subseteq W\left(d\right)\to f\left(x\right)=x\right)\right\}\right)$$
14	4	fvexi	$$⊢M\in \mathrm{V}$$
15	14	rabex	$$⊢\left\{f\in M|\forall x\in S\left(x\subseteq W\left(D\right)\to f\left(x\right)=x\right)\right\}\in \mathrm{V}$$
16	12 13 15	fvmpt	$$⊢D\in A\to \left(d\in A⟼\left\{f\in M|\forall x\in S\left(x\subseteq W\left(d\right)\to f\left(x\right)=x\right)\right\}\right)\left(D\right)=\left\{f\in M|\forall x\in S\left(x\subseteq W\left(D\right)\to f\left(x\right)=x\right)\right\}$$
17	7 16	sylan9eq	$$⊢\left(K\in B\wedge D\in A\right)\to L\left(D\right)=\left\{f\in M|\forall x\in S\left(x\subseteq W\left(D\right)\to f\left(x\right)=x\right)\right\}$$