Theorem isat3

Description: The predicate "is an atom". ( elat2 analog.) (Contributed by NM, 27-Apr-2014)

	Ref	Expression
Hypotheses	isat3.b	$$⊢B={\mathrm{Base}}_K$$
	isat3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	isat3.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	isat3.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	isat3	$$⊢K\in \mathrm{AtLat}\to \left(P\in A\leftrightarrow \left(P\in B\wedge P\ne \underset{\dot{}}{0}\wedge \forall x\in B\left(x\underset{\dot{}}{\le }P\to \left(x=P\vee x=\underset{\dot{}}{0}\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isat3.b	$$⊢B={\mathrm{Base}}_K$$
2		isat3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		isat3.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
4		isat3.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		eqid	$$⊢{⋖}_K={⋖}_K$$
6	1 3 5 4	isat	$$⊢K\in \mathrm{AtLat}\to \left(P\in A\leftrightarrow \left(P\in B\wedge \underset{\dot{}}{0}{⋖}_{K}P\right)\right)$$
7		simpl	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in B\right)\to K\in \mathrm{AtLat}$$
8	1 3	atl0cl	$$⊢K\in \mathrm{AtLat}\to \underset{\dot{}}{0}\in B$$
9	8	adantr	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in B\right)\to \underset{\dot{}}{0}\in B$$
10		simpr	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in B\right)\to P\in B$$
11		eqid	$$⊢{<}_K={<}_K$$
12	1 2 11 5	cvrval2	$$⊢\left(K\in \mathrm{AtLat}\wedge \underset{\dot{}}{0}\in B\wedge P\in B\right)\to \left(\underset{\dot{}}{0}{⋖}_{K}P\leftrightarrow \left(\underset{\dot{}}{0}{<}_{K}P\wedge \forall x\in B\left(\left(\underset{\dot{}}{0}{<}_{K}x\wedge x\underset{\dot{}}{\le }P\right)\to x=P\right)\right)\right)$$
13	7 9 10 12	syl3anc	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in B\right)\to \left(\underset{\dot{}}{0}{⋖}_{K}P\leftrightarrow \left(\underset{\dot{}}{0}{<}_{K}P\wedge \forall x\in B\left(\left(\underset{\dot{}}{0}{<}_{K}x\wedge x\underset{\dot{}}{\le }P\right)\to x=P\right)\right)\right)$$
14	1 11 3	atlltn0	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in B\right)\to \left(\underset{\dot{}}{0}{<}_{K}P\leftrightarrow P\ne \underset{\dot{}}{0}\right)$$
15	1 11 3	atlltn0	$$⊢\left(K\in \mathrm{AtLat}\wedge x\in B\right)\to \left(\underset{\dot{}}{0}{<}_{K}x\leftrightarrow x\ne \underset{\dot{}}{0}\right)$$
16	15	adantlr	$$⊢\left(\left(K\in \mathrm{AtLat}\wedge P\in B\right)\wedge x\in B\right)\to \left(\underset{\dot{}}{0}{<}_{K}x\leftrightarrow x\ne \underset{\dot{}}{0}\right)$$
17	16	imbi1d	$$⊢\left(\left(K\in \mathrm{AtLat}\wedge P\in B\right)\wedge x\in B\right)\to \left(\left(\underset{\dot{}}{0}{<}_{K}x\to x=P\right)\leftrightarrow \left(x\ne \underset{\dot{}}{0}\to x=P\right)\right)$$
18	17	imbi2d	$$⊢\left(\left(K\in \mathrm{AtLat}\wedge P\in B\right)\wedge x\in B\right)\to \left(\left(x\underset{\dot{}}{\le }P\to \left(\underset{\dot{}}{0}{<}_{K}x\to x=P\right)\right)\leftrightarrow \left(x\underset{\dot{}}{\le }P\to \left(x\ne \underset{\dot{}}{0}\to x=P\right)\right)\right)$$
19		impexp	$$⊢\left(\left(\underset{\dot{}}{0}{<}_{K}x\wedge x\underset{\dot{}}{\le }P\right)\to x=P\right)\leftrightarrow \left(\underset{\dot{}}{0}{<}_{K}x\to \left(x\underset{\dot{}}{\le }P\to x=P\right)\right)$$
20		bi2.04	$$⊢\left(\underset{\dot{}}{0}{<}_{K}x\to \left(x\underset{\dot{}}{\le }P\to x=P\right)\right)\leftrightarrow \left(x\underset{\dot{}}{\le }P\to \left(\underset{\dot{}}{0}{<}_{K}x\to x=P\right)\right)$$
21	19 20	bitri	$$⊢\left(\left(\underset{\dot{}}{0}{<}_{K}x\wedge x\underset{\dot{}}{\le }P\right)\to x=P\right)\leftrightarrow \left(x\underset{\dot{}}{\le }P\to \left(\underset{\dot{}}{0}{<}_{K}x\to x=P\right)\right)$$
22		orcom	$$⊢\left(x=P\vee x=\underset{\dot{}}{0}\right)\leftrightarrow \left(x=\underset{\dot{}}{0}\vee x=P\right)$$
23		neor	$$⊢\left(x=\underset{\dot{}}{0}\vee x=P\right)\leftrightarrow \left(x\ne \underset{\dot{}}{0}\to x=P\right)$$
24	22 23	bitri	$$⊢\left(x=P\vee x=\underset{\dot{}}{0}\right)\leftrightarrow \left(x\ne \underset{\dot{}}{0}\to x=P\right)$$
25	24	imbi2i	$$⊢\left(x\underset{\dot{}}{\le }P\to \left(x=P\vee x=\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(x\underset{\dot{}}{\le }P\to \left(x\ne \underset{\dot{}}{0}\to x=P\right)\right)$$
26	18 21 25	3bitr4g	$$⊢\left(\left(K\in \mathrm{AtLat}\wedge P\in B\right)\wedge x\in B\right)\to \left(\left(\left(\underset{\dot{}}{0}{<}_{K}x\wedge x\underset{\dot{}}{\le }P\right)\to x=P\right)\leftrightarrow \left(x\underset{\dot{}}{\le }P\to \left(x=P\vee x=\underset{\dot{}}{0}\right)\right)\right)$$
27	26	ralbidva	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in B\right)\to \left(\forall x\in B\left(\left(\underset{\dot{}}{0}{<}_{K}x\wedge x\underset{\dot{}}{\le }P\right)\to x=P\right)\leftrightarrow \forall x\in B\left(x\underset{\dot{}}{\le }P\to \left(x=P\vee x=\underset{\dot{}}{0}\right)\right)\right)$$
28	14 27	anbi12d	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in B\right)\to \left(\left(\underset{\dot{}}{0}{<}_{K}P\wedge \forall x\in B\left(\left(\underset{\dot{}}{0}{<}_{K}x\wedge x\underset{\dot{}}{\le }P\right)\to x=P\right)\right)\leftrightarrow \left(P\ne \underset{\dot{}}{0}\wedge \forall x\in B\left(x\underset{\dot{}}{\le }P\to \left(x=P\vee x=\underset{\dot{}}{0}\right)\right)\right)\right)$$
29	13 28	bitr2d	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in B\right)\to \left(\left(P\ne \underset{\dot{}}{0}\wedge \forall x\in B\left(x\underset{\dot{}}{\le }P\to \left(x=P\vee x=\underset{\dot{}}{0}\right)\right)\right)\leftrightarrow \underset{\dot{}}{0}{⋖}_{K}P\right)$$
30	29	pm5.32da	$$⊢K\in \mathrm{AtLat}\to \left(\left(P\in B\wedge \left(P\ne \underset{\dot{}}{0}\wedge \forall x\in B\left(x\underset{\dot{}}{\le }P\to \left(x=P\vee x=\underset{\dot{}}{0}\right)\right)\right)\right)\leftrightarrow \left(P\in B\wedge \underset{\dot{}}{0}{⋖}_{K}P\right)\right)$$
31	6 30	bitr4d	$$⊢K\in \mathrm{AtLat}\to \left(P\in A\leftrightarrow \left(P\in B\wedge \left(P\ne \underset{\dot{}}{0}\wedge \forall x\in B\left(x\underset{\dot{}}{\le }P\to \left(x=P\vee x=\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
32		3anass	$$⊢\left(P\in B\wedge P\ne \underset{\dot{}}{0}\wedge \forall x\in B\left(x\underset{\dot{}}{\le }P\to \left(x=P\vee x=\underset{\dot{}}{0}\right)\right)\right)\leftrightarrow \left(P\in B\wedge \left(P\ne \underset{\dot{}}{0}\wedge \forall x\in B\left(x\underset{\dot{}}{\le }P\to \left(x=P\vee x=\underset{\dot{}}{0}\right)\right)\right)\right)$$
33	31 32	bitr4di	$$⊢K\in \mathrm{AtLat}\to \left(P\in A\leftrightarrow \left(P\in B\wedge P\ne \underset{\dot{}}{0}\wedge \forall x\in B\left(x\underset{\dot{}}{\le }P\to \left(x=P\vee x=\underset{\dot{}}{0}\right)\right)\right)\right)$$