Step |
Hyp |
Ref |
Expression |
1 |
|
poml4.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
2 |
|
poml4.p |
⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 ) |
3 |
|
simp1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → 𝐾 ∈ HL ) |
4 |
|
simp3 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) |
5 |
1 2
|
polssatN |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑌 ) ⊆ 𝐴 ) |
6 |
5
|
3adant3 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( ⊥ ‘ 𝑌 ) ⊆ 𝐴 ) |
7 |
4 6
|
sstrd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → 𝑋 ⊆ 𝐴 ) |
8 |
3 7 6
|
3jca |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ 𝑌 ) ⊆ 𝐴 ) ) |
9 |
1 2
|
3polN |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) = ( ⊥ ‘ 𝑌 ) ) |
10 |
9
|
3adant3 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) = ( ⊥ ‘ 𝑌 ) ) |
11 |
4 10
|
jca |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) = ( ⊥ ‘ 𝑌 ) ) ) |
12 |
1 2
|
poml4N |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ 𝑌 ) ⊆ 𝐴 ) → ( ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) = ( ⊥ ‘ 𝑌 ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) ) ∩ ( ⊥ ‘ 𝑌 ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) |
13 |
8 11 12
|
sylc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) ) ∩ ( ⊥ ‘ 𝑌 ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) |