Metamath Proof Explorer

Theorem leatb

Description: A poset element less than or equal to an atom equals either zero or the atom. ( atss analog.) (Contributed by NM, 17-Nov-2011)

Ref Expression
Hypotheses leatom.b ⊢ B = Base K
leatom.l ⊢ ≤ ˙ = ≤ K
leatom.z ⊢ 0 ˙ = 0. ⁡ K
leatom.a ⊢ A = Atoms ⁡ K
Assertion leatb ⊢ K ∈ OP ∧ X ∈ B ∧ P ∈ A → X ≤ ˙ P ↔ X = P ∨ X = 0 ˙

Proof

Step Hyp Ref Expression
1 leatom.b ⊢ B = Base K
2 leatom.l ⊢ ≤ ˙ = ≤ K
3 leatom.z ⊢ 0 ˙ = 0. ⁡ K
4 leatom.a ⊢ A = Atoms ⁡ K
5 1 2 3 op0le ⊢ K ∈ OP ∧ X ∈ B → 0 ˙ ≤ ˙ X
6 5 3adant3 ⊢ K ∈ OP ∧ X ∈ B ∧ P ∈ A → 0 ˙ ≤ ˙ X
7 6 biantrurd ⊢ K ∈ OP ∧ X ∈ B ∧ P ∈ A → X ≤ ˙ P ↔ 0 ˙ ≤ ˙ X ∧ X ≤ ˙ P
8 opposet ⊢ K ∈ OP → K ∈ Poset
9 8 3ad2ant1 ⊢ K ∈ OP ∧ X ∈ B ∧ P ∈ A → K ∈ Poset
10 1 3 op0cl ⊢ K ∈ OP → 0 ˙ ∈ B
11 1 4 atbase ⊢ P ∈ A → P ∈ B
12 id ⊢ X ∈ B → X ∈ B
13 10 11 12 3anim123i ⊢ K ∈ OP ∧ P ∈ A ∧ X ∈ B → 0 ˙ ∈ B ∧ P ∈ B ∧ X ∈ B
14 13 3com23 ⊢ K ∈ OP ∧ X ∈ B ∧ P ∈ A → 0 ˙ ∈ B ∧ P ∈ B ∧ X ∈ B
15 eqid ⊢ ⋖ K = ⋖ K
16 3 15 4 atcvr0 ⊢ K ∈ OP ∧ P ∈ A → 0 ˙ ⋖ K P
17 16 3adant2 ⊢ K ∈ OP ∧ X ∈ B ∧ P ∈ A → 0 ˙ ⋖ K P
18 1 2 15 cvrnbtwn4 ⊢ K ∈ Poset ∧ 0 ˙ ∈ B ∧ P ∈ B ∧ X ∈ B ∧ 0 ˙ ⋖ K P → 0 ˙ ≤ ˙ X ∧ X ≤ ˙ P ↔ 0 ˙ = X ∨ X = P
19 9 14 17 18 syl3anc ⊢ K ∈ OP ∧ X ∈ B ∧ P ∈ A → 0 ˙ ≤ ˙ X ∧ X ≤ ˙ P ↔ 0 ˙ = X ∨ X = P
20 eqcom ⊢ 0 ˙ = X ↔ X = 0 ˙
21 20 orbi1i ⊢ 0 ˙ = X ∨ X = P ↔ X = 0 ˙ ∨ X = P
22 19 21 bitrdi ⊢ K ∈ OP ∧ X ∈ B ∧ P ∈ A → 0 ˙ ≤ ˙ X ∧ X ≤ ˙ P ↔ X = 0 ˙ ∨ X = P
23 7 22 bitrd ⊢ K ∈ OP ∧ X ∈ B ∧ P ∈ A → X ≤ ˙ P ↔ X = 0 ˙ ∨ X = P
24 orcom ⊢ X = 0 ˙ ∨ X = P ↔ X = P ∨ X = 0 ˙
25 23 24 bitrdi ⊢ K ∈ OP ∧ X ∈ B ∧ P ∈ A → X ≤ ˙ P ↔ X = P ∨ X = 0 ˙