Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemftr.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
cdlemftr.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
3 |
|
cdlemftr.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
cdlemftr.r |
⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
1 2 3 4
|
cdlemftr2 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ) ) |
6 |
|
3simpa |
⊢ ( ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ) → ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ) ) |
7 |
6
|
reximi |
⊢ ( ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ) → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ) ) |
8 |
5 7
|
syl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ) ) |