Step |
Hyp |
Ref |
Expression |
1 |
|
ltrneq.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
ltrneq.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
ltrneq.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
4 |
|
ltrneq.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
5 |
|
ltrneq.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
6 |
|
ralinexa |
⊢ ( ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ¬ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ↔ ¬ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) |
7 |
|
nne |
⊢ ( ¬ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ↔ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) |
8 |
7
|
biimpi |
⊢ ( ¬ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) |
9 |
8
|
imim2i |
⊢ ( ( ¬ 𝑝 ≤ 𝑊 → ¬ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) → ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) |
10 |
9
|
ralimi |
⊢ ( ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ¬ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) → ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) |
11 |
6 10
|
sylbir |
⊢ ( ¬ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) → ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) |
12 |
1 2 3 4 5
|
ltrnid |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ↔ 𝐹 = ( I ↾ 𝐵 ) ) ) |
13 |
11 12
|
syl5ib |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ¬ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) → 𝐹 = ( I ↾ 𝐵 ) ) ) |
14 |
13
|
necon1ad |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) ) |
15 |
14
|
3impia |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) |