Step |
Hyp |
Ref |
Expression |
1 |
|
lautm.b |
|- B = ( Base ` K ) |
2 |
|
lautm.m |
|- ./\ = ( meet ` K ) |
3 |
|
lautm.i |
|- I = ( LAut ` K ) |
4 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
5 |
|
simpl |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> K e. Lat ) |
6 |
|
simpr1 |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> F e. I ) |
7 |
5 6
|
jca |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( K e. Lat /\ F e. I ) ) |
8 |
1 2
|
latmcl |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B ) |
9 |
8
|
3adant3r1 |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X ./\ Y ) e. B ) |
10 |
1 3
|
lautcl |
|- ( ( ( K e. Lat /\ F e. I ) /\ ( X ./\ Y ) e. B ) -> ( F ` ( X ./\ Y ) ) e. B ) |
11 |
7 9 10
|
syl2anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( X ./\ Y ) ) e. B ) |
12 |
|
simpr2 |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> X e. B ) |
13 |
1 3
|
lautcl |
|- ( ( ( K e. Lat /\ F e. I ) /\ X e. B ) -> ( F ` X ) e. B ) |
14 |
7 12 13
|
syl2anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` X ) e. B ) |
15 |
|
simpr3 |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> Y e. B ) |
16 |
1 3
|
lautcl |
|- ( ( ( K e. Lat /\ F e. I ) /\ Y e. B ) -> ( F ` Y ) e. B ) |
17 |
7 15 16
|
syl2anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` Y ) e. B ) |
18 |
1 2
|
latmcl |
|- ( ( K e. Lat /\ ( F ` X ) e. B /\ ( F ` Y ) e. B ) -> ( ( F ` X ) ./\ ( F ` Y ) ) e. B ) |
19 |
5 14 17 18
|
syl3anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( F ` X ) ./\ ( F ` Y ) ) e. B ) |
20 |
1 4 2
|
latmle1 |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) ( le ` K ) X ) |
21 |
20
|
3adant3r1 |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X ./\ Y ) ( le ` K ) X ) |
22 |
1 4 3
|
lautle |
|- ( ( ( K e. Lat /\ F e. I ) /\ ( ( X ./\ Y ) e. B /\ X e. B ) ) -> ( ( X ./\ Y ) ( le ` K ) X <-> ( F ` ( X ./\ Y ) ) ( le ` K ) ( F ` X ) ) ) |
23 |
7 9 12 22
|
syl12anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( X ./\ Y ) ( le ` K ) X <-> ( F ` ( X ./\ Y ) ) ( le ` K ) ( F ` X ) ) ) |
24 |
21 23
|
mpbid |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( X ./\ Y ) ) ( le ` K ) ( F ` X ) ) |
25 |
1 4 2
|
latmle2 |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) ( le ` K ) Y ) |
26 |
25
|
3adant3r1 |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X ./\ Y ) ( le ` K ) Y ) |
27 |
1 4 3
|
lautle |
|- ( ( ( K e. Lat /\ F e. I ) /\ ( ( X ./\ Y ) e. B /\ Y e. B ) ) -> ( ( X ./\ Y ) ( le ` K ) Y <-> ( F ` ( X ./\ Y ) ) ( le ` K ) ( F ` Y ) ) ) |
28 |
7 9 15 27
|
syl12anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( X ./\ Y ) ( le ` K ) Y <-> ( F ` ( X ./\ Y ) ) ( le ` K ) ( F ` Y ) ) ) |
29 |
26 28
|
mpbid |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( X ./\ Y ) ) ( le ` K ) ( F ` Y ) ) |
30 |
1 4 2
|
latlem12 |
|- ( ( K e. Lat /\ ( ( F ` ( X ./\ Y ) ) e. B /\ ( F ` X ) e. B /\ ( F ` Y ) e. B ) ) -> ( ( ( F ` ( X ./\ Y ) ) ( le ` K ) ( F ` X ) /\ ( F ` ( X ./\ Y ) ) ( le ` K ) ( F ` Y ) ) <-> ( F ` ( X ./\ Y ) ) ( le ` K ) ( ( F ` X ) ./\ ( F ` Y ) ) ) ) |
31 |
5 11 14 17 30
|
syl13anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( ( F ` ( X ./\ Y ) ) ( le ` K ) ( F ` X ) /\ ( F ` ( X ./\ Y ) ) ( le ` K ) ( F ` Y ) ) <-> ( F ` ( X ./\ Y ) ) ( le ` K ) ( ( F ` X ) ./\ ( F ` Y ) ) ) ) |
32 |
24 29 31
|
mpbi2and |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( X ./\ Y ) ) ( le ` K ) ( ( F ` X ) ./\ ( F ` Y ) ) ) |
33 |
1 3
|
laut1o |
|- ( ( K e. Lat /\ F e. I ) -> F : B -1-1-onto-> B ) |
34 |
33
|
3ad2antr1 |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> F : B -1-1-onto-> B ) |
35 |
|
f1ocnvfv2 |
|- ( ( F : B -1-1-onto-> B /\ ( ( F ` X ) ./\ ( F ` Y ) ) e. B ) -> ( F ` ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ) = ( ( F ` X ) ./\ ( F ` Y ) ) ) |
36 |
34 19 35
|
syl2anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ) = ( ( F ` X ) ./\ ( F ` Y ) ) ) |
37 |
1 4 2
|
latmle1 |
|- ( ( K e. Lat /\ ( F ` X ) e. B /\ ( F ` Y ) e. B ) -> ( ( F ` X ) ./\ ( F ` Y ) ) ( le ` K ) ( F ` X ) ) |
38 |
5 14 17 37
|
syl3anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( F ` X ) ./\ ( F ` Y ) ) ( le ` K ) ( F ` X ) ) |
39 |
1 4 3
|
lautcnvle |
|- ( ( ( K e. Lat /\ F e. I ) /\ ( ( ( F ` X ) ./\ ( F ` Y ) ) e. B /\ ( F ` X ) e. B ) ) -> ( ( ( F ` X ) ./\ ( F ` Y ) ) ( le ` K ) ( F ` X ) <-> ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) ( `' F ` ( F ` X ) ) ) ) |
40 |
7 19 14 39
|
syl12anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( ( F ` X ) ./\ ( F ` Y ) ) ( le ` K ) ( F ` X ) <-> ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) ( `' F ` ( F ` X ) ) ) ) |
41 |
38 40
|
mpbid |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) ( `' F ` ( F ` X ) ) ) |
42 |
|
f1ocnvfv1 |
|- ( ( F : B -1-1-onto-> B /\ X e. B ) -> ( `' F ` ( F ` X ) ) = X ) |
43 |
34 12 42
|
syl2anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( F ` X ) ) = X ) |
44 |
41 43
|
breqtrd |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) X ) |
45 |
1 4 2
|
latmle2 |
|- ( ( K e. Lat /\ ( F ` X ) e. B /\ ( F ` Y ) e. B ) -> ( ( F ` X ) ./\ ( F ` Y ) ) ( le ` K ) ( F ` Y ) ) |
46 |
5 14 17 45
|
syl3anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( F ` X ) ./\ ( F ` Y ) ) ( le ` K ) ( F ` Y ) ) |
47 |
1 4 3
|
lautcnvle |
|- ( ( ( K e. Lat /\ F e. I ) /\ ( ( ( F ` X ) ./\ ( F ` Y ) ) e. B /\ ( F ` Y ) e. B ) ) -> ( ( ( F ` X ) ./\ ( F ` Y ) ) ( le ` K ) ( F ` Y ) <-> ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) ( `' F ` ( F ` Y ) ) ) ) |
48 |
7 19 17 47
|
syl12anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( ( F ` X ) ./\ ( F ` Y ) ) ( le ` K ) ( F ` Y ) <-> ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) ( `' F ` ( F ` Y ) ) ) ) |
49 |
46 48
|
mpbid |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) ( `' F ` ( F ` Y ) ) ) |
50 |
|
f1ocnvfv1 |
|- ( ( F : B -1-1-onto-> B /\ Y e. B ) -> ( `' F ` ( F ` Y ) ) = Y ) |
51 |
34 15 50
|
syl2anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( F ` Y ) ) = Y ) |
52 |
49 51
|
breqtrd |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) Y ) |
53 |
|
f1ocnvdm |
|- ( ( F : B -1-1-onto-> B /\ ( ( F ` X ) ./\ ( F ` Y ) ) e. B ) -> ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) e. B ) |
54 |
34 19 53
|
syl2anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) e. B ) |
55 |
1 4 2
|
latlem12 |
|- ( ( K e. Lat /\ ( ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) e. B /\ X e. B /\ Y e. B ) ) -> ( ( ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) X /\ ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) Y ) <-> ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) ( X ./\ Y ) ) ) |
56 |
5 54 12 15 55
|
syl13anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) X /\ ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) Y ) <-> ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) ( X ./\ Y ) ) ) |
57 |
44 52 56
|
mpbi2and |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) ( X ./\ Y ) ) |
58 |
1 4 3
|
lautle |
|- ( ( ( K e. Lat /\ F e. I ) /\ ( ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) e. B /\ ( X ./\ Y ) e. B ) ) -> ( ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) ( X ./\ Y ) <-> ( F ` ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ) ( le ` K ) ( F ` ( X ./\ Y ) ) ) ) |
59 |
7 54 9 58
|
syl12anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ( le ` K ) ( X ./\ Y ) <-> ( F ` ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ) ( le ` K ) ( F ` ( X ./\ Y ) ) ) ) |
60 |
57 59
|
mpbid |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( `' F ` ( ( F ` X ) ./\ ( F ` Y ) ) ) ) ( le ` K ) ( F ` ( X ./\ Y ) ) ) |
61 |
36 60
|
eqbrtrrd |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( F ` X ) ./\ ( F ` Y ) ) ( le ` K ) ( F ` ( X ./\ Y ) ) ) |
62 |
1 4 5 11 19 32 61
|
latasymd |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( X ./\ Y ) ) = ( ( F ` X ) ./\ ( F ` Y ) ) ) |