Metamath Proof Explorer

Theorem isat3

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

Ref Expression
Hypotheses isat3.b ⊢ B = Base K
isat3.l ⊢ ≤ ˙ = ≤ K
isat3.z ⊢ 0 ˙ = 0. ⁡ K
isat3.a ⊢ A = Atoms ⁡ K
Assertion isat3 ⊢ K ∈ AtLat → P ∈ A ↔ P ∈ B ∧ P ≠ 0 ˙ ∧ ∀ x ∈ B x ≤ ˙ P → x = P ∨ x = 0 ˙

Proof

Step Hyp Ref Expression
1 isat3.b ⊢ B = Base K
2 isat3.l ⊢ ≤ ˙ = ≤ K
3 isat3.z ⊢ 0 ˙ = 0. ⁡ K
4 isat3.a ⊢ A = Atoms ⁡ K
5 eqid ⊢ ⋖ K = ⋖ K
6 1 3 5 4 isat ⊢ K ∈ AtLat → P ∈ A ↔ P ∈ B ∧ 0 ˙ ⋖ K P
7 simpl ⊢ K ∈ AtLat ∧ P ∈ B → K ∈ AtLat
8 1 3 atl0cl ⊢ K ∈ AtLat → 0 ˙ ∈ B
9 8 adantr ⊢ K ∈ AtLat ∧ P ∈ B → 0 ˙ ∈ B
10 simpr ⊢ K ∈ AtLat ∧ P ∈ B → P ∈ B
11 eqid ⊢ < K = < K
12 1 2 11 5 cvrval2 ⊢ K ∈ AtLat ∧ 0 ˙ ∈ B ∧ P ∈ B → 0 ˙ ⋖ K P ↔ 0 ˙ < K P ∧ ∀ x ∈ B 0 ˙ < K x ∧ x ≤ ˙ P → x = P
13 7 9 10 12 syl3anc ⊢ K ∈ AtLat ∧ P ∈ B → 0 ˙ ⋖ K P ↔ 0 ˙ < K P ∧ ∀ x ∈ B 0 ˙ < K x ∧ x ≤ ˙ P → x = P
14 1 11 3 atlltn0 ⊢ K ∈ AtLat ∧ P ∈ B → 0 ˙ < K P ↔ P ≠ 0 ˙
15 1 11 3 atlltn0 ⊢ K ∈ AtLat ∧ x ∈ B → 0 ˙ < K x ↔ x ≠ 0 ˙
16 15 adantlr ⊢ K ∈ AtLat ∧ P ∈ B ∧ x ∈ B → 0 ˙ < K x ↔ x ≠ 0 ˙
17 16 imbi1d ⊢ K ∈ AtLat ∧ P ∈ B ∧ x ∈ B → 0 ˙ < K x → x = P ↔ x ≠ 0 ˙ → x = P
18 17 imbi2d ⊢ K ∈ AtLat ∧ P ∈ B ∧ x ∈ B → x ≤ ˙ P → 0 ˙ < K x → x = P ↔ x ≤ ˙ P → x ≠ 0 ˙ → x = P
19 impexp ⊢ 0 ˙ < K x ∧ x ≤ ˙ P → x = P ↔ 0 ˙ < K x → x ≤ ˙ P → x = P
20 bi2.04 ⊢ 0 ˙ < K x → x ≤ ˙ P → x = P ↔ x ≤ ˙ P → 0 ˙ < K x → x = P
21 19 20 bitri ⊢ 0 ˙ < K x ∧ x ≤ ˙ P → x = P ↔ x ≤ ˙ P → 0 ˙ < K x → x = P
22 orcom ⊢ x = P ∨ x = 0 ˙ ↔ x = 0 ˙ ∨ x = P
23 neor ⊢ x = 0 ˙ ∨ x = P ↔ x ≠ 0 ˙ → x = P
24 22 23 bitri ⊢ x = P ∨ x = 0 ˙ ↔ x ≠ 0 ˙ → x = P
25 24 imbi2i ⊢ x ≤ ˙ P → x = P ∨ x = 0 ˙ ↔ x ≤ ˙ P → x ≠ 0 ˙ → x = P
26 18 21 25 3bitr4g ⊢ K ∈ AtLat ∧ P ∈ B ∧ x ∈ B → 0 ˙ < K x ∧ x ≤ ˙ P → x = P ↔ x ≤ ˙ P → x = P ∨ x = 0 ˙
27 26 ralbidva ⊢ K ∈ AtLat ∧ P ∈ B → ∀ x ∈ B 0 ˙ < K x ∧ x ≤ ˙ P → x = P ↔ ∀ x ∈ B x ≤ ˙ P → x = P ∨ x = 0 ˙
28 14 27 anbi12d ⊢ K ∈ AtLat ∧ P ∈ B → 0 ˙ < K P ∧ ∀ x ∈ B 0 ˙ < K x ∧ x ≤ ˙ P → x = P ↔ P ≠ 0 ˙ ∧ ∀ x ∈ B x ≤ ˙ P → x = P ∨ x = 0 ˙
29 13 28 bitr2d ⊢ K ∈ AtLat ∧ P ∈ B → P ≠ 0 ˙ ∧ ∀ x ∈ B x ≤ ˙ P → x = P ∨ x = 0 ˙ ↔ 0 ˙ ⋖ K P
30 29 pm5.32da ⊢ K ∈ AtLat → P ∈ B ∧ P ≠ 0 ˙ ∧ ∀ x ∈ B x ≤ ˙ P → x = P ∨ x = 0 ˙ ↔ P ∈ B ∧ 0 ˙ ⋖ K P
31 6 30 bitr4d ⊢ K ∈ AtLat → P ∈ A ↔ P ∈ B ∧ P ≠ 0 ˙ ∧ ∀ x ∈ B x ≤ ˙ P → x = P ∨ x = 0 ˙
32 3anass ⊢ P ∈ B ∧ P ≠ 0 ˙ ∧ ∀ x ∈ B x ≤ ˙ P → x = P ∨ x = 0 ˙ ↔ P ∈ B ∧ P ≠ 0 ˙ ∧ ∀ x ∈ B x ≤ ˙ P → x = P ∨ x = 0 ˙
33 31 32 bitr4di ⊢ K ∈ AtLat → P ∈ A ↔ P ∈ B ∧ P ≠ 0 ˙ ∧ ∀ x ∈ B x ≤ ˙ P → x = P ∨ x = 0 ˙