Metamath Proof Explorer

Theorem intnatN

Description: If the intersection with a non-majorizing element is an atom, the intersecting element is not an atom. (Contributed by NM, 26-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses intnat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
intnat.l ⊢ ≤ = ( le ‘ 𝐾 )
intnat.m ⊢ ∧ = ( meet ‘ 𝐾 )
intnat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion intnatN ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ¬ 𝑌 ≤ 𝑋 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ) → ¬ 𝑌 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 intnat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 intnat.l ⊢ ≤ = ( le ‘ 𝐾 )
3 intnat.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 intnat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
6 5 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ AtLat )
7 6 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝐾 ∈ AtLat )
8 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
9 8 4 atn0 ⊢ ( ( 𝐾 ∈ AtLat ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) ≠ ( 0. ‘ 𝐾 ) )
10 7 9 sylancom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) ≠ ( 0. ‘ 𝐾 ) )
11 10 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 → ( 𝑋 ∧ 𝑌 ) ≠ ( 0. ‘ 𝐾 ) ) )
12 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → 𝐾 ∈ HL )
13 12 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → 𝐾 ∈ Lat )
14 simpll2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
15 simpll3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
16 1 3 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )
17 13 14 15 16 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )
18 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ¬ 𝑌 ≤ 𝑋 )
19 12 5 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
20 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 )
21 1 2 3 8 4 atnle ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ¬ 𝑌 ≤ 𝑋 ↔ ( 𝑌 ∧ 𝑋 ) = ( 0. ‘ 𝐾 ) ) )
22 19 20 14 21 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( ¬ 𝑌 ≤ 𝑋 ↔ ( 𝑌 ∧ 𝑋 ) = ( 0. ‘ 𝐾 ) ) )
23 18 22 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∧ 𝑋 ) = ( 0. ‘ 𝐾 ) )
24 17 23 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) = ( 0. ‘ 𝐾 ) )
25 24 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) → ( 𝑌 ∈ 𝐴 → ( 𝑋 ∧ 𝑌 ) = ( 0. ‘ 𝐾 ) ) )
26 25 necon3ad ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑌 ) ≠ ( 0. ‘ 𝐾 ) → ¬ 𝑌 ∈ 𝐴 ) )
27 11 26 syld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑌 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 → ¬ 𝑌 ∈ 𝐴 ) )
28 27 impr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ¬ 𝑌 ≤ 𝑋 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ) → ¬ 𝑌 ∈ 𝐴 )