Theorem pats

Description: The set of atoms in a poset. (Contributed by NM, 18-Sep-2011)

	Ref	Expression
Hypotheses	patoms.b	$$⊢B={\mathrm{Base}}_K$$
	patoms.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	patoms.c	$$⊢C={⋖}_K$$
	patoms.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	pats	$$⊢K\in D\to A=\left\{x\in B|\underset{\dot{}}{0}Cx\right\}$$

Proof

Step	Hyp	Ref	Expression
1		patoms.b	$$⊢B={\mathrm{Base}}_K$$
2		patoms.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
3		patoms.c	$$⊢C={⋖}_K$$
4		patoms.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		elex	$$⊢K\in D\to K\in \mathrm{V}$$
6		fveq2	$$⊢p=K\to {\mathrm{Base}}_p={\mathrm{Base}}_K$$
7	6 1	eqtr4di	$$⊢p=K\to {\mathrm{Base}}_p=B$$
8		fveq2	$$⊢p=K\to {⋖}_p={⋖}_K$$
9	8 3	eqtr4di	$$⊢p=K\to {⋖}_p=C$$
10	9	breqd	$$⊢p=K\to \left(\mathrm{0.}\left(p\right){⋖}_{p}x\leftrightarrow \mathrm{0.}\left(p\right)Cx\right)$$
11		fveq2	$$⊢p=K\to \mathrm{0.}\left(p\right)=\mathrm{0.}\left(K\right)$$
12	11 2	eqtr4di	$$⊢p=K\to \mathrm{0.}\left(p\right)=\underset{\dot{}}{0}$$
13	12	breq1d	$$⊢p=K\to \left(\mathrm{0.}\left(p\right)Cx\leftrightarrow \underset{\dot{}}{0}Cx\right)$$
14	10 13	bitrd	$$⊢p=K\to \left(\mathrm{0.}\left(p\right){⋖}_{p}x\leftrightarrow \underset{\dot{}}{0}Cx\right)$$
15	7 14	rabeqbidv	$$⊢p=K\to \left\{x\in {\mathrm{Base}}_p|\mathrm{0.}\left(p\right){⋖}_{p}x\right\}=\left\{x\in B|\underset{\dot{}}{0}Cx\right\}$$
16		df-ats	$$⊢\mathrm{Atoms}=\left(p\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_p|\mathrm{0.}\left(p\right){⋖}_{p}x\right\}\right)$$
17	1	fvexi	$$⊢B\in \mathrm{V}$$
18	17	rabex	$$⊢\left\{x\in B|\underset{\dot{}}{0}Cx\right\}\in \mathrm{V}$$
19	15 16 18	fvmpt	$$⊢K\in \mathrm{V}\to \mathrm{Atoms}\left(K\right)=\left\{x\in B|\underset{\dot{}}{0}Cx\right\}$$
20	4 19	syl5eq	$$⊢K\in \mathrm{V}\to A=\left\{x\in B|\underset{\dot{}}{0}Cx\right\}$$
21	5 20	syl	$$⊢K\in D\to A=\left\{x\in B|\underset{\dot{}}{0}Cx\right\}$$