Step |
Hyp |
Ref |
Expression |
1 |
|
llncmp.l |
|- .<_ = ( le ` K ) |
2 |
|
llncmp.n |
|- N = ( LLines ` K ) |
3 |
|
simp2 |
|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> X e. N ) |
4 |
|
simp1 |
|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> K e. HL ) |
5 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
6 |
5 2
|
llnbase |
|- ( X e. N -> X e. ( Base ` K ) ) |
7 |
6
|
3ad2ant2 |
|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> X e. ( Base ` K ) ) |
8 |
|
eqid |
|- ( |
9 |
|
eqid |
|- ( Atoms ` K ) = ( Atoms ` K ) |
10 |
5 8 9 2
|
islln4 |
|- ( ( K e. HL /\ X e. ( Base ` K ) ) -> ( X e. N <-> E. p e. ( Atoms ` K ) p ( |
11 |
4 7 10
|
syl2anc |
|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X e. N <-> E. p e. ( Atoms ` K ) p ( |
12 |
3 11
|
mpbid |
|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> E. p e. ( Atoms ` K ) p ( |
13 |
|
simpr3 |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( X .<_ Y ) |
14 |
|
hlpos |
|- ( K e. HL -> K e. Poset ) |
15 |
14
|
3ad2ant1 |
|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> K e. Poset ) |
16 |
15
|
adantr |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( K e. Poset ) |
17 |
7
|
adantr |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( X e. ( Base ` K ) ) |
18 |
|
simpl3 |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( Y e. N ) |
19 |
5 2
|
llnbase |
|- ( Y e. N -> Y e. ( Base ` K ) ) |
20 |
18 19
|
syl |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( Y e. ( Base ` K ) ) |
21 |
|
simpr1 |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( p e. ( Atoms ` K ) ) |
22 |
5 9
|
atbase |
|- ( p e. ( Atoms ` K ) -> p e. ( Base ` K ) ) |
23 |
21 22
|
syl |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( p e. ( Base ` K ) ) |
24 |
|
simpr2 |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( p ( |
25 |
|
simpl1 |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( K e. HL ) |
26 |
5 1 8
|
cvrle |
|- ( ( ( K e. HL /\ p e. ( Base ` K ) /\ X e. ( Base ` K ) ) /\ p ( p .<_ X ) |
27 |
25 23 17 24 26
|
syl31anc |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( p .<_ X ) |
28 |
5 1
|
postr |
|- ( ( K e. Poset /\ ( p e. ( Base ` K ) /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) ) -> ( ( p .<_ X /\ X .<_ Y ) -> p .<_ Y ) ) |
29 |
16 23 17 20 28
|
syl13anc |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( ( ( p .<_ X /\ X .<_ Y ) -> p .<_ Y ) ) |
30 |
27 13 29
|
mp2and |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( p .<_ Y ) |
31 |
1 8 9 2
|
atcvrlln2 |
|- ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ Y e. N ) /\ p .<_ Y ) -> p ( |
32 |
25 21 18 30 31
|
syl31anc |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( p ( |
33 |
5 1 8
|
cvrcmp |
|- ( ( K e. Poset /\ ( X e. ( Base ` K ) /\ Y e. ( Base ` K ) /\ p e. ( Base ` K ) ) /\ ( p ( ( X .<_ Y <-> X = Y ) ) |
34 |
16 17 20 23 24 32 33
|
syl132anc |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( ( X .<_ Y <-> X = Y ) ) |
35 |
13 34
|
mpbid |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ p ( X = Y ) |
36 |
35
|
3exp2 |
|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( p e. ( Atoms ` K ) -> ( p ( ( X .<_ Y -> X = Y ) ) ) ) |
37 |
36
|
rexlimdv |
|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( E. p e. ( Atoms ` K ) p ( ( X .<_ Y -> X = Y ) ) ) |
38 |
12 37
|
mpd |
|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X .<_ Y -> X = Y ) ) |
39 |
5 1
|
posref |
|- ( ( K e. Poset /\ X e. ( Base ` K ) ) -> X .<_ X ) |
40 |
15 7 39
|
syl2anc |
|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> X .<_ X ) |
41 |
|
breq2 |
|- ( X = Y -> ( X .<_ X <-> X .<_ Y ) ) |
42 |
40 41
|
syl5ibcom |
|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X = Y -> X .<_ Y ) ) |
43 |
38 42
|
impbid |
|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X .<_ Y <-> X = Y ) ) |