| Step |
Hyp |
Ref |
Expression |
| 1 |
|
linepsub.n |
⊢ 𝑁 = ( Lines ‘ 𝐾 ) |
| 2 |
|
linepsub.s |
⊢ 𝑆 = ( PSubSp ‘ 𝐾 ) |
| 3 |
|
ssrab2 |
⊢ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ⊆ ( Atoms ‘ 𝐾 ) |
| 4 |
|
sseq1 |
⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ↔ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ⊆ ( Atoms ‘ 𝐾 ) ) ) |
| 5 |
3 4
|
mpbiri |
⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) |
| 6 |
5
|
a1i |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) ) |
| 7 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
| 8 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
| 9 |
7 8
|
atbase |
⊢ ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) → 𝑎 ∈ ( Base ‘ 𝐾 ) ) |
| 10 |
7 8
|
atbase |
⊢ ( 𝑏 ∈ ( Atoms ‘ 𝐾 ) → 𝑏 ∈ ( Base ‘ 𝐾 ) ) |
| 11 |
9 10
|
anim12i |
⊢ ( ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑎 ∈ ( Base ‘ 𝐾 ) ∧ 𝑏 ∈ ( Base ‘ 𝐾 ) ) ) |
| 12 |
|
eqid |
⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) |
| 13 |
7 12
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑎 ∈ ( Base ‘ 𝐾 ) ∧ 𝑏 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) |
| 14 |
13
|
3expb |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ∈ ( Base ‘ 𝐾 ) ∧ 𝑏 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) |
| 15 |
11 14
|
sylan2 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) |
| 16 |
|
eleq2 |
⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑝 ∈ 𝑋 ↔ 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ) |
| 17 |
|
breq1 |
⊢ ( 𝑐 = 𝑝 → ( 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ↔ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 18 |
17
|
elrab |
⊢ ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ↔ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 19 |
7 8
|
atbase |
⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) ) |
| 20 |
19
|
anim1i |
⊢ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 21 |
18 20
|
sylbi |
⊢ ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 22 |
16 21
|
syl6bi |
⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑝 ∈ 𝑋 → ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) |
| 23 |
|
eleq2 |
⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑞 ∈ 𝑋 ↔ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ) |
| 24 |
|
breq1 |
⊢ ( 𝑐 = 𝑞 → ( 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ↔ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 25 |
24
|
elrab |
⊢ ( 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ↔ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 26 |
7 8
|
atbase |
⊢ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) → 𝑞 ∈ ( Base ‘ 𝐾 ) ) |
| 27 |
26
|
anim1i |
⊢ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 28 |
25 27
|
sylbi |
⊢ ( 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 29 |
23 28
|
syl6bi |
⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑞 ∈ 𝑋 → ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) |
| 30 |
22 29
|
anim12d |
⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ∧ ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) |
| 31 |
|
an4 |
⊢ ( ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ∧ ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ↔ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) |
| 32 |
30 31
|
syl6ib |
⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) |
| 33 |
32
|
imp |
⊢ ( ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) |
| 34 |
33
|
anim2i |
⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) ) → ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) |
| 35 |
34
|
anassrs |
⊢ ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) → ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) |
| 36 |
7 8
|
atbase |
⊢ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → 𝑟 ∈ ( Base ‘ 𝐾 ) ) |
| 37 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
| 38 |
7 37 12
|
latjle12 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ↔ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 39 |
38
|
biimpd |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 40 |
39
|
3exp2 |
⊢ ( 𝐾 ∈ Lat → ( 𝑝 ∈ ( Base ‘ 𝐾 ) → ( 𝑞 ∈ ( Base ‘ 𝐾 ) → ( ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) ) |
| 41 |
40
|
impd |
⊢ ( 𝐾 ∈ Lat → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) |
| 42 |
41
|
com23 |
⊢ ( 𝐾 ∈ Lat → ( ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) |
| 43 |
42
|
imp43 |
⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) |
| 44 |
43
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) |
| 45 |
7 12
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ) |
| 46 |
45
|
3expib |
⊢ ( 𝐾 ∈ Lat → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ) ) |
| 47 |
7 37
|
lattr |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑟 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 48 |
47
|
3exp2 |
⊢ ( 𝐾 ∈ Lat → ( 𝑟 ∈ ( Base ‘ 𝐾 ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) ) |
| 49 |
48
|
com24 |
⊢ ( 𝐾 ∈ Lat → ( ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) → ( 𝑟 ∈ ( Base ‘ 𝐾 ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) ) |
| 50 |
46 49
|
syl5d |
⊢ ( 𝐾 ∈ Lat → ( ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑟 ∈ ( Base ‘ 𝐾 ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) ) |
| 51 |
50
|
imp41 |
⊢ ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 52 |
51
|
adantlrr |
⊢ ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 53 |
44 52
|
mpan2d |
⊢ ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 54 |
35 36 53
|
syl2an |
⊢ ( ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 55 |
|
simpr |
⊢ ( ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) |
| 56 |
54 55
|
jctild |
⊢ ( ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) |
| 57 |
|
eleq2 |
⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑟 ∈ 𝑋 ↔ 𝑟 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ) |
| 58 |
|
breq1 |
⊢ ( 𝑐 = 𝑟 → ( 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ↔ 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 59 |
58
|
elrab |
⊢ ( 𝑟 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ↔ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) |
| 60 |
57 59
|
bitrdi |
⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑟 ∈ 𝑋 ↔ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) |
| 61 |
60
|
ad3antlr |
⊢ ( ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑟 ∈ 𝑋 ↔ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) |
| 62 |
56 61
|
sylibrd |
⊢ ( ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) |
| 63 |
62
|
ralrimiva |
⊢ ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) → ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) |
| 64 |
63
|
ralrimivva |
⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) → ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) |
| 65 |
64
|
ex |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) |
| 66 |
15 65
|
syldan |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) |
| 67 |
6 66
|
jcad |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) ) |
| 68 |
67
|
adantld |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) ) |
| 69 |
68
|
rexlimdvva |
⊢ ( 𝐾 ∈ Lat → ( ∃ 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ( 𝑎 ≠ 𝑏 ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) ) |
| 70 |
37 12 8 1
|
isline |
⊢ ( 𝐾 ∈ Lat → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ( 𝑎 ≠ 𝑏 ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ) ) |
| 71 |
37 12 8 2
|
ispsubsp |
⊢ ( 𝐾 ∈ Lat → ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) ) |
| 72 |
69 70 71
|
3imtr4d |
⊢ ( 𝐾 ∈ Lat → ( 𝑋 ∈ 𝑁 → 𝑋 ∈ 𝑆 ) ) |
| 73 |
72
|
imp |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝑁 ) → 𝑋 ∈ 𝑆 ) |