Metamath Proof Explorer

Theorem 2lnat

Description: Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012)

Ref Expression
Hypotheses 2lnat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2lnat.m ⊢ ∧ = ( meet ‘ 𝐾 )
2lnat.z ⊢ 0 = ( 0. ‘ 𝐾 )
2lnat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2lnat.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
2lnat.f ⊢ 𝐹 = ( pmap ‘ 𝐾 )
Assertion 2lnat ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 2lnat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 2lnat.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 2lnat.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 2lnat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 2lnat.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
6 2lnat.f ⊢ 𝐹 = ( pmap ‘ 𝐾 )
7 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → 𝐾 ∈ HL )
8 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
9 7 8 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → 𝐾 ∈ AtLat )
10 7 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → 𝐾 ∈ Lat )
11 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → 𝑋 ∈ 𝐵 )
12 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → 𝑌 ∈ 𝐵 )
13 1 2 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
14 10 11 12 13 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
15 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( 𝑋 ∧ 𝑌 ) ≠ 0 )
16 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
17 1 16 3 4 atlex ⊢ ( ( 𝐾 ∈ AtLat ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) )
18 9 14 15 17 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ∃ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) )
19 simp13l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑋 ≠ 𝑌 )
20 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
21 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 )
22 simp12r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 )
23 1 16 5 6 lncmp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ 𝑋 = 𝑌 ) )
24 20 21 22 23 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ 𝑋 = 𝑌 ) )
25 simp111 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝐾 ∈ HL )
26 25 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝐾 ∈ Lat )
27 simp112 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑋 ∈ 𝐵 )
28 simp113 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑌 ∈ 𝐵 )
29 1 16 2 latleeqm1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) )
30 26 27 28 29 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) )
31 24 30 bitr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 = 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) )
32 31 necon3bid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 ≠ 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) ≠ 𝑋 ) )
33 19 32 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ≠ 𝑋 )
34 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) )
35 1 16 2 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 )
36 26 27 28 35 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 )
37 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
38 25 37 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝐾 ∈ Poset )
39 1 4 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
40 39 3ad2ant2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑝 ∈ 𝐵 )
41 26 27 28 13 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
42 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑝 ∈ 𝐴 )
43 1 16 26 40 41 27 34 36 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑝 ( le ‘ 𝐾 ) 𝑋 )
44 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
45 1 16 44 4 5 6 lncvrat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 )
46 25 27 42 21 43 45 syl32anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 )
47 1 16 44 cvrnbtwn4 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 ) ↔ ( 𝑝 = ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) ) )
48 38 40 27 41 46 47 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 ) ↔ ( 𝑝 = ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) ) )
49 34 36 48 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑝 = ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) )
50 neor ⊢ ( ( 𝑝 = ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) ↔ ( 𝑝 ≠ ( 𝑋 ∧ 𝑌 ) → ( 𝑋 ∧ 𝑌 ) = 𝑋 ) )
51 49 50 sylib ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑝 ≠ ( 𝑋 ∧ 𝑌 ) → ( 𝑋 ∧ 𝑌 ) = 𝑋 ) )
52 51 necon1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( ( 𝑋 ∧ 𝑌 ) ≠ 𝑋 → 𝑝 = ( 𝑋 ∧ 𝑌 ) ) )
53 33 52 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑝 = ( 𝑋 ∧ 𝑌 ) )
54 53 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( 𝑝 ∈ 𝐴 → ( 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) → 𝑝 = ( 𝑋 ∧ 𝑌 ) ) ) )
55 54 reximdvai ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( ∃ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) → ∃ 𝑝 ∈ 𝐴 𝑝 = ( 𝑋 ∧ 𝑌 ) ) )
56 18 55 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ∃ 𝑝 ∈ 𝐴 𝑝 = ( 𝑋 ∧ 𝑌 ) )
57 risset ⊢ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ↔ ∃ 𝑝 ∈ 𝐴 𝑝 = ( 𝑋 ∧ 𝑌 ) )
58 56 57 sylibr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )