Metamath Proof Explorer

Theorem isat3

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

Ref Expression
Hypotheses isat3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
isat3.l ⊢ ≤ = ( le ‘ 𝐾 )
isat3.z ⊢ 0 = ( 0. ‘ 𝐾 )
isat3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion isat3 ( 𝐾 ∈ AtLat → ( 𝑃 ∈ 𝐴 ↔ ( 𝑃 ∈ 𝐵 ∧ 𝑃 ≠ 0 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑃 → ( 𝑥 = 𝑃 ∨ 𝑥 = 0 ) ) ) ) )

Proof

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