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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
leatom.l ⊢ ≤ = ( le ‘ 𝐾 )
leatom.z ⊢ 0 = ( 0. ‘ 𝐾 )
leatom.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion leatb ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ≤ 𝑃 ↔ ( 𝑋 = 𝑃 ∨ 𝑋 = 0 ) ) )

Proof

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