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 ) ) → ( 𝑋 𝑌 ) ∈ 𝐴 )