# 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 ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ¬ 𝑌 𝑋 ∧ ( 𝑋 𝑌 ) ∈ 𝐴 ) ) → ¬ 𝑌𝐴 )