Step |
Hyp |
Ref |
Expression |
1 |
|
llncmp.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
2 |
|
llncmp.n |
⊢ 𝑁 = ( LLines ‘ 𝐾 ) |
3 |
|
simp2 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → 𝑋 ∈ 𝑁 ) |
4 |
|
simp1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → 𝐾 ∈ HL ) |
5 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
6 |
5 2
|
llnbase |
⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) ) |
7 |
6
|
3ad2ant2 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) ) |
8 |
|
eqid |
⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 ) |
9 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
10 |
5 8 9 2
|
islln4 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) |
11 |
4 7 10
|
syl2anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) |
12 |
3 11
|
mpbid |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) |
13 |
|
simpr3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑋 ≤ 𝑌 ) |
14 |
|
hlpos |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset ) |
15 |
14
|
3ad2ant1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → 𝐾 ∈ Poset ) |
16 |
15
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝐾 ∈ Poset ) |
17 |
7
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) ) |
18 |
|
simpl3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑌 ∈ 𝑁 ) |
19 |
5 2
|
llnbase |
⊢ ( 𝑌 ∈ 𝑁 → 𝑌 ∈ ( Base ‘ 𝐾 ) ) |
20 |
18 19
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) ) |
21 |
|
simpr1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) |
22 |
5 9
|
atbase |
⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) ) |
23 |
21 22
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) ) |
24 |
|
simpr2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) |
25 |
|
simpl1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝐾 ∈ HL ) |
26 |
5 1 8
|
cvrle |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑝 ≤ 𝑋 ) |
27 |
25 23 17 24 26
|
syl31anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑝 ≤ 𝑋 ) |
28 |
5 1
|
postr |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑝 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) → 𝑝 ≤ 𝑌 ) ) |
29 |
16 23 17 20 28
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( ( 𝑝 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) → 𝑝 ≤ 𝑌 ) ) |
30 |
27 13 29
|
mp2and |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑝 ≤ 𝑌 ) |
31 |
1 8 9 2
|
atcvrlln2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑝 ≤ 𝑌 ) → 𝑝 ( ⋖ ‘ 𝐾 ) 𝑌 ) |
32 |
25 21 18 30 31
|
syl31anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑝 ( ⋖ ‘ 𝐾 ) 𝑌 ) |
33 |
5 1 8
|
cvrcmp |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑌 ) ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) ) |
34 |
16 17 20 23 24 32 33
|
syl132anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) ) |
35 |
13 34
|
mpbid |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑋 = 𝑌 ) |
36 |
35
|
3exp2 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 → ( 𝑋 ≤ 𝑌 → 𝑋 = 𝑌 ) ) ) ) |
37 |
36
|
rexlimdv |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 → ( 𝑋 ≤ 𝑌 → 𝑋 = 𝑌 ) ) ) |
38 |
12 37
|
mpd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( 𝑋 ≤ 𝑌 → 𝑋 = 𝑌 ) ) |
39 |
5 1
|
posref |
⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → 𝑋 ≤ 𝑋 ) |
40 |
15 7 39
|
syl2anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → 𝑋 ≤ 𝑋 ) |
41 |
|
breq2 |
⊢ ( 𝑋 = 𝑌 → ( 𝑋 ≤ 𝑋 ↔ 𝑋 ≤ 𝑌 ) ) |
42 |
40 41
|
syl5ibcom |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( 𝑋 = 𝑌 → 𝑋 ≤ 𝑌 ) ) |
43 |
38 42
|
impbid |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) ) |