Metamath Proof Explorer

Theorem hlrelat2

Description: A consequence of relative atomicity. ( chrelat2i analog.) (Contributed by NM, 5-Feb-2012)

Ref Expression
Hypotheses hlrelat2.b ⊢ B = Base K
hlrelat2.l ⊢ ≤ ˙ = ≤ K
hlrelat2.a ⊢ A = Atoms ⁡ K
Assertion hlrelat2 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → ¬ X ≤ ˙ Y ↔ ∃ p ∈ A p ≤ ˙ X ∧ ¬ p ≤ ˙ Y

Proof

Step Hyp Ref Expression
1 hlrelat2.b ⊢ B = Base K
2 hlrelat2.l ⊢ ≤ ˙ = ≤ K
3 hlrelat2.a ⊢ A = Atoms ⁡ K
4 hllat ⊢ K ∈ HL → K ∈ Lat
5 eqid ⊢ < K = < K
6 eqid ⊢ meet ⁡ K = meet ⁡ K
7 1 2 5 6 latnlemlt ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → ¬ X ≤ ˙ Y ↔ X meet ⁡ K Y < K X
8 4 7 syl3an1 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → ¬ X ≤ ˙ Y ↔ X meet ⁡ K Y < K X
9 simp1 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → K ∈ HL
10 1 6 latmcl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y ∈ B
11 4 10 syl3an1 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y ∈ B
12 simp2 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ∈ B
13 eqid ⊢ join ⁡ K = join ⁡ K
14 1 2 5 13 3 hlrelat ⊢ K ∈ HL ∧ X meet ⁡ K Y ∈ B ∧ X ∈ B ∧ X meet ⁡ K Y < K X → ∃ p ∈ A X meet ⁡ K Y < K X meet ⁡ K Y join ⁡ K p ∧ X meet ⁡ K Y join ⁡ K p ≤ ˙ X
15 14 ex ⊢ K ∈ HL ∧ X meet ⁡ K Y ∈ B ∧ X ∈ B → X meet ⁡ K Y < K X → ∃ p ∈ A X meet ⁡ K Y < K X meet ⁡ K Y join ⁡ K p ∧ X meet ⁡ K Y join ⁡ K p ≤ ˙ X
16 9 11 12 15 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y < K X → ∃ p ∈ A X meet ⁡ K Y < K X meet ⁡ K Y join ⁡ K p ∧ X meet ⁡ K Y join ⁡ K p ≤ ˙ X
17 simpl1 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → K ∈ HL
18 17 hllatd ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → K ∈ Lat
19 11 adantr ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → X meet ⁡ K Y ∈ B
20 1 3 atbase ⊢ p ∈ A → p ∈ B
21 20 adantl ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → p ∈ B
22 simpl2 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → X ∈ B
23 1 2 13 latjle12 ⊢ K ∈ Lat ∧ X meet ⁡ K Y ∈ B ∧ p ∈ B ∧ X ∈ B → X meet ⁡ K Y ≤ ˙ X ∧ p ≤ ˙ X ↔ X meet ⁡ K Y join ⁡ K p ≤ ˙ X
24 18 19 21 22 23 syl13anc ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → X meet ⁡ K Y ≤ ˙ X ∧ p ≤ ˙ X ↔ X meet ⁡ K Y join ⁡ K p ≤ ˙ X
25 simpr ⊢ X meet ⁡ K Y ≤ ˙ X ∧ p ≤ ˙ X → p ≤ ˙ X
26 24 25 syl6bir ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → X meet ⁡ K Y join ⁡ K p ≤ ˙ X → p ≤ ˙ X
27 26 adantld ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → X meet ⁡ K Y < K X meet ⁡ K Y join ⁡ K p ∧ X meet ⁡ K Y join ⁡ K p ≤ ˙ X → p ≤ ˙ X
28 simpl3 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → Y ∈ B
29 1 2 6 latlem12 ⊢ K ∈ Lat ∧ p ∈ B ∧ X ∈ B ∧ Y ∈ B → p ≤ ˙ X ∧ p ≤ ˙ Y ↔ p ≤ ˙ X meet ⁡ K Y
30 18 21 22 28 29 syl13anc ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → p ≤ ˙ X ∧ p ≤ ˙ Y ↔ p ≤ ˙ X meet ⁡ K Y
31 30 notbid ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → ¬ p ≤ ˙ X ∧ p ≤ ˙ Y ↔ ¬ p ≤ ˙ X meet ⁡ K Y
32 1 2 5 13 latnle ⊢ K ∈ Lat ∧ X meet ⁡ K Y ∈ B ∧ p ∈ B → ¬ p ≤ ˙ X meet ⁡ K Y ↔ X meet ⁡ K Y < K X meet ⁡ K Y join ⁡ K p
33 18 19 21 32 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → ¬ p ≤ ˙ X meet ⁡ K Y ↔ X meet ⁡ K Y < K X meet ⁡ K Y join ⁡ K p
34 31 33 bitrd ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → ¬ p ≤ ˙ X ∧ p ≤ ˙ Y ↔ X meet ⁡ K Y < K X meet ⁡ K Y join ⁡ K p
35 34 24 anbi12d ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → ¬ p ≤ ˙ X ∧ p ≤ ˙ Y ∧ X meet ⁡ K Y ≤ ˙ X ∧ p ≤ ˙ X ↔ X meet ⁡ K Y < K X meet ⁡ K Y join ⁡ K p ∧ X meet ⁡ K Y join ⁡ K p ≤ ˙ X
36 pm3.21 ⊢ p ≤ ˙ Y → p ≤ ˙ X → p ≤ ˙ X ∧ p ≤ ˙ Y
37 orcom ⊢ p ≤ ˙ X ∧ p ≤ ˙ Y ∨ ¬ p ≤ ˙ X ↔ ¬ p ≤ ˙ X ∨ p ≤ ˙ X ∧ p ≤ ˙ Y
38 pm4.55 ⊢ ¬ ¬ p ≤ ˙ X ∧ p ≤ ˙ Y ∧ p ≤ ˙ X ↔ p ≤ ˙ X ∧ p ≤ ˙ Y ∨ ¬ p ≤ ˙ X
39 imor ⊢ p ≤ ˙ X → p ≤ ˙ X ∧ p ≤ ˙ Y ↔ ¬ p ≤ ˙ X ∨ p ≤ ˙ X ∧ p ≤ ˙ Y
40 37 38 39 3bitr4ri ⊢ p ≤ ˙ X → p ≤ ˙ X ∧ p ≤ ˙ Y ↔ ¬ ¬ p ≤ ˙ X ∧ p ≤ ˙ Y ∧ p ≤ ˙ X
41 36 40 sylib ⊢ p ≤ ˙ Y → ¬ ¬ p ≤ ˙ X ∧ p ≤ ˙ Y ∧ p ≤ ˙ X
42 41 con2i ⊢ ¬ p ≤ ˙ X ∧ p ≤ ˙ Y ∧ p ≤ ˙ X → ¬ p ≤ ˙ Y
43 42 adantrl ⊢ ¬ p ≤ ˙ X ∧ p ≤ ˙ Y ∧ X meet ⁡ K Y ≤ ˙ X ∧ p ≤ ˙ X → ¬ p ≤ ˙ Y
44 35 43 syl6bir ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → X meet ⁡ K Y < K X meet ⁡ K Y join ⁡ K p ∧ X meet ⁡ K Y join ⁡ K p ≤ ˙ X → ¬ p ≤ ˙ Y
45 27 44 jcad ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → X meet ⁡ K Y < K X meet ⁡ K Y join ⁡ K p ∧ X meet ⁡ K Y join ⁡ K p ≤ ˙ X → p ≤ ˙ X ∧ ¬ p ≤ ˙ Y
46 45 reximdva ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → ∃ p ∈ A X meet ⁡ K Y < K X meet ⁡ K Y join ⁡ K p ∧ X meet ⁡ K Y join ⁡ K p ≤ ˙ X → ∃ p ∈ A p ≤ ˙ X ∧ ¬ p ≤ ˙ Y
47 16 46 syld ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y < K X → ∃ p ∈ A p ≤ ˙ X ∧ ¬ p ≤ ˙ Y
48 8 47 sylbid ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → ¬ X ≤ ˙ Y → ∃ p ∈ A p ≤ ˙ X ∧ ¬ p ≤ ˙ Y
49 1 2 lattr ⊢ K ∈ Lat ∧ p ∈ B ∧ X ∈ B ∧ Y ∈ B → p ≤ ˙ X ∧ X ≤ ˙ Y → p ≤ ˙ Y
50 18 21 22 28 49 syl13anc ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B ∧ p ∈ A → p ≤ ˙ X ∧ X ≤ ˙ Y → p ≤ ˙ Y
51 50 exp4b ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → p ∈ A → p ≤ ˙ X → X ≤ ˙ Y → p ≤ ˙ Y
52 51 com34 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → p ∈ A → X ≤ ˙ Y → p ≤ ˙ X → p ≤ ˙ Y
53 52 com23 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y → p ∈ A → p ≤ ˙ X → p ≤ ˙ Y
54 53 ralrimdv ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y → ∀ p ∈ A p ≤ ˙ X → p ≤ ˙ Y
55 iman ⊢ p ≤ ˙ X → p ≤ ˙ Y ↔ ¬ p ≤ ˙ X ∧ ¬ p ≤ ˙ Y
56 55 ralbii ⊢ ∀ p ∈ A p ≤ ˙ X → p ≤ ˙ Y ↔ ∀ p ∈ A ¬ p ≤ ˙ X ∧ ¬ p ≤ ˙ Y
57 ralnex ⊢ ∀ p ∈ A ¬ p ≤ ˙ X ∧ ¬ p ≤ ˙ Y ↔ ¬ ∃ p ∈ A p ≤ ˙ X ∧ ¬ p ≤ ˙ Y
58 56 57 bitri ⊢ ∀ p ∈ A p ≤ ˙ X → p ≤ ˙ Y ↔ ¬ ∃ p ∈ A p ≤ ˙ X ∧ ¬ p ≤ ˙ Y
59 54 58 syl6ib ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y → ¬ ∃ p ∈ A p ≤ ˙ X ∧ ¬ p ≤ ˙ Y
60 59 con2d ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → ∃ p ∈ A p ≤ ˙ X ∧ ¬ p ≤ ˙ Y → ¬ X ≤ ˙ Y
61 48 60 impbid ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → ¬ X ≤ ˙ Y ↔ ∃ p ∈ A p ≤ ˙ X ∧ ¬ p ≤ ˙ Y