Step |
Hyp |
Ref |
Expression |
1 |
|
lautj.b |
|- B = ( Base ` K ) |
2 |
|
lautj.j |
|- .\/ = ( join ` K ) |
3 |
|
lautj.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
|
latjcl |
|- ( ( 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
|
latjcl |
|- ( ( 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 3
|
laut1o |
|- ( ( K e. Lat /\ F e. I ) -> F : B -1-1-onto-> B ) |
21 |
20
|
3ad2antr1 |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> F : B -1-1-onto-> B ) |
22 |
|
f1ocnvfv1 |
|- ( ( F : B -1-1-onto-> B /\ ( X .\/ Y ) e. B ) -> ( `' F ` ( F ` ( X .\/ Y ) ) ) = ( X .\/ Y ) ) |
23 |
21 9 22
|
syl2anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( F ` ( X .\/ Y ) ) ) = ( X .\/ Y ) ) |
24 |
1 4 2
|
latlej1 |
|- ( ( K e. Lat /\ ( F ` X ) e. B /\ ( F ` Y ) e. B ) -> ( F ` X ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) ) |
25 |
5 14 17 24
|
syl3anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` X ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) ) |
26 |
|
f1ocnvfv2 |
|- ( ( F : B -1-1-onto-> B /\ ( ( F ` X ) .\/ ( F ` Y ) ) e. B ) -> ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) = ( ( F ` X ) .\/ ( F ` Y ) ) ) |
27 |
21 19 26
|
syl2anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) = ( ( F ` X ) .\/ ( F ` Y ) ) ) |
28 |
25 27
|
breqtrrd |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` X ) ( le ` K ) ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) |
29 |
|
f1ocnvdm |
|- ( ( F : B -1-1-onto-> B /\ ( ( F ` X ) .\/ ( F ` Y ) ) e. B ) -> ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) e. B ) |
30 |
21 19 29
|
syl2anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) e. B ) |
31 |
1 4 3
|
lautle |
|- ( ( ( K e. Lat /\ F e. I ) /\ ( X e. B /\ ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) e. B ) ) -> ( X ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) <-> ( F ` X ) ( le ` K ) ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) ) |
32 |
7 12 30 31
|
syl12anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) <-> ( F ` X ) ( le ` K ) ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) ) |
33 |
28 32
|
mpbird |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> X ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) |
34 |
1 4 2
|
latlej2 |
|- ( ( K e. Lat /\ ( F ` X ) e. B /\ ( F ` Y ) e. B ) -> ( F ` Y ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) ) |
35 |
5 14 17 34
|
syl3anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` Y ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) ) |
36 |
35 27
|
breqtrrd |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` Y ) ( le ` K ) ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) |
37 |
1 4 3
|
lautle |
|- ( ( ( K e. Lat /\ F e. I ) /\ ( Y e. B /\ ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) e. B ) ) -> ( Y ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) <-> ( F ` Y ) ( le ` K ) ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) ) |
38 |
7 15 30 37
|
syl12anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( Y ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) <-> ( F ` Y ) ( le ` K ) ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) ) |
39 |
36 38
|
mpbird |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> Y ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) |
40 |
1 4 2
|
latjle12 |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) e. B ) ) -> ( ( X ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) /\ Y ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) <-> ( X .\/ Y ) ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) |
41 |
5 12 15 30 40
|
syl13anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( X ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) /\ Y ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) <-> ( X .\/ Y ) ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) |
42 |
33 39 41
|
mpbi2and |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X .\/ Y ) ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) |
43 |
23 42
|
eqbrtrd |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( F ` ( X .\/ Y ) ) ) ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) |
44 |
1 4 3
|
lautcnvle |
|- ( ( ( K e. Lat /\ F e. I ) /\ ( ( F ` ( X .\/ Y ) ) e. B /\ ( ( F ` X ) .\/ ( F ` Y ) ) e. B ) ) -> ( ( F ` ( X .\/ Y ) ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) <-> ( `' F ` ( F ` ( X .\/ Y ) ) ) ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) |
45 |
7 11 19 44
|
syl12anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( F ` ( X .\/ Y ) ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) <-> ( `' F ` ( F ` ( X .\/ Y ) ) ) ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) |
46 |
43 45
|
mpbird |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( X .\/ Y ) ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) ) |
47 |
1 4 2
|
latlej1 |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X ( le ` K ) ( X .\/ Y ) ) |
48 |
47
|
3adant3r1 |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> X ( le ` K ) ( X .\/ Y ) ) |
49 |
1 4 3
|
lautle |
|- ( ( ( K e. Lat /\ F e. I ) /\ ( X e. B /\ ( X .\/ Y ) e. B ) ) -> ( X ( le ` K ) ( X .\/ Y ) <-> ( F ` X ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) ) |
50 |
7 12 9 49
|
syl12anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X ( le ` K ) ( X .\/ Y ) <-> ( F ` X ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) ) |
51 |
48 50
|
mpbid |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` X ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) |
52 |
1 4 2
|
latlej2 |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> Y ( le ` K ) ( X .\/ Y ) ) |
53 |
52
|
3adant3r1 |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> Y ( le ` K ) ( X .\/ Y ) ) |
54 |
1 4 3
|
lautle |
|- ( ( ( K e. Lat /\ F e. I ) /\ ( Y e. B /\ ( X .\/ Y ) e. B ) ) -> ( Y ( le ` K ) ( X .\/ Y ) <-> ( F ` Y ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) ) |
55 |
7 15 9 54
|
syl12anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( Y ( le ` K ) ( X .\/ Y ) <-> ( F ` Y ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) ) |
56 |
53 55
|
mpbid |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` Y ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) |
57 |
1 4 2
|
latjle12 |
|- ( ( K e. Lat /\ ( ( F ` X ) e. B /\ ( F ` Y ) e. B /\ ( F ` ( X .\/ Y ) ) e. B ) ) -> ( ( ( F ` X ) ( le ` K ) ( F ` ( X .\/ Y ) ) /\ ( F ` Y ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) <-> ( ( F ` X ) .\/ ( F ` Y ) ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) ) |
58 |
5 14 17 11 57
|
syl13anc |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( ( F ` X ) ( le ` K ) ( F ` ( X .\/ Y ) ) /\ ( F ` Y ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) <-> ( ( F ` X ) .\/ ( F ` Y ) ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) ) |
59 |
51 56 58
|
mpbi2and |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( F ` X ) .\/ ( F ` Y ) ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) |
60 |
1 4 5 11 19 46 59
|
latasymd |
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .\/ ( F ` Y ) ) ) |