Step |
Hyp |
Ref |
Expression |
1 |
|
2lnat.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
2lnat.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
3 |
|
2lnat.z |
⊢ 0 = ( 0. ‘ 𝐾 ) |
4 |
|
2lnat.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
5 |
|
2lnat.n |
⊢ 𝑁 = ( Lines ‘ 𝐾 ) |
6 |
|
2lnat.f |
⊢ 𝐹 = ( pmap ‘ 𝐾 ) |
7 |
|
simp11 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → 𝐾 ∈ HL ) |
8 |
|
hlatl |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat ) |
9 |
7 8
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → 𝐾 ∈ AtLat ) |
10 |
7
|
hllatd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → 𝐾 ∈ Lat ) |
11 |
|
simp12 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → 𝑋 ∈ 𝐵 ) |
12 |
|
simp13 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → 𝑌 ∈ 𝐵 ) |
13 |
1 2
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ) |
14 |
10 11 12 13
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ) |
15 |
|
simp3r |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( 𝑋 ∧ 𝑌 ) ≠ 0 ) |
16 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
17 |
1 16 3 4
|
atlex |
⊢ ( ( 𝐾 ∈ AtLat ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) |
18 |
9 14 15 17
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ∃ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) |
19 |
|
simp13l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑋 ≠ 𝑌 ) |
20 |
|
simp11 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) |
21 |
|
simp12l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ) |
22 |
|
simp12r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) |
23 |
1 16 5 6
|
lncmp |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ 𝑋 = 𝑌 ) ) |
24 |
20 21 22 23
|
syl12anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ 𝑋 = 𝑌 ) ) |
25 |
|
simp111 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝐾 ∈ HL ) |
26 |
25
|
hllatd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝐾 ∈ Lat ) |
27 |
|
simp112 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑋 ∈ 𝐵 ) |
28 |
|
simp113 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑌 ∈ 𝐵 ) |
29 |
1 16 2
|
latleeqm1 |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) ) |
30 |
26 27 28 29
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) ) |
31 |
24 30
|
bitr3d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 = 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) ) |
32 |
31
|
necon3bid |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 ≠ 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) ≠ 𝑋 ) ) |
33 |
19 32
|
mpbid |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ≠ 𝑋 ) |
34 |
|
simp3 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) |
35 |
1 16 2
|
latmle1 |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 ) |
36 |
26 27 28 35
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 ) |
37 |
|
hlpos |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset ) |
38 |
25 37
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝐾 ∈ Poset ) |
39 |
1 4
|
atbase |
⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 ) |
40 |
39
|
3ad2ant2 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑝 ∈ 𝐵 ) |
41 |
26 27 28 13
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ) |
42 |
|
simp2 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑝 ∈ 𝐴 ) |
43 |
1 16 26 40 41 27 34 36
|
lattrd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑝 ( le ‘ 𝐾 ) 𝑋 ) |
44 |
|
eqid |
⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 ) |
45 |
1 16 44 4 5 6
|
lncvrat |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) |
46 |
25 27 42 21 43 45
|
syl32anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) |
47 |
1 16 44
|
cvrnbtwn4 |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 ) ↔ ( 𝑝 = ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) ) ) |
48 |
38 40 27 41 46 47
|
syl131anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 ) ↔ ( 𝑝 = ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) ) ) |
49 |
34 36 48
|
mpbi2and |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑝 = ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) ) |
50 |
|
neor |
⊢ ( ( 𝑝 = ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) ↔ ( 𝑝 ≠ ( 𝑋 ∧ 𝑌 ) → ( 𝑋 ∧ 𝑌 ) = 𝑋 ) ) |
51 |
49 50
|
sylib |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( 𝑝 ≠ ( 𝑋 ∧ 𝑌 ) → ( 𝑋 ∧ 𝑌 ) = 𝑋 ) ) |
52 |
51
|
necon1d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( ( 𝑋 ∧ 𝑌 ) ≠ 𝑋 → 𝑝 = ( 𝑋 ∧ 𝑌 ) ) ) |
53 |
33 52
|
mpd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → 𝑝 = ( 𝑋 ∧ 𝑌 ) ) |
54 |
53
|
3exp |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( 𝑝 ∈ 𝐴 → ( 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) → 𝑝 = ( 𝑋 ∧ 𝑌 ) ) ) ) |
55 |
54
|
reximdvai |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( ∃ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) → ∃ 𝑝 ∈ 𝐴 𝑝 = ( 𝑋 ∧ 𝑌 ) ) ) |
56 |
18 55
|
mpd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ∃ 𝑝 ∈ 𝐴 𝑝 = ( 𝑋 ∧ 𝑌 ) ) |
57 |
|
risset |
⊢ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ↔ ∃ 𝑝 ∈ 𝐴 𝑝 = ( 𝑋 ∧ 𝑌 ) ) |
58 |
56 57
|
sylibr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑁 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑋 ≠ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) |