Proof of Theorem ltrncnvel
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ltrnel.l | . . . 4
⊢  ≤ =
(le‘𝐾) | 
| 2 |  | ltrnel.a | . . . 4
⊢ 𝐴 = (Atoms‘𝐾) | 
| 3 |  | ltrnel.h | . . . 4
⊢ 𝐻 = (LHyp‘𝐾) | 
| 4 |  | ltrnel.t | . . . 4
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | 
| 5 | 1, 2, 3, 4 | ltrncnvat 40143 | . . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (◡𝐹‘𝑃) ∈ 𝐴) | 
| 6 | 5 | 3adant3r 1182 | . 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (◡𝐹‘𝑃) ∈ 𝐴) | 
| 7 |  | simp3r 1203 | . . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ¬ 𝑃 ≤ 𝑊) | 
| 8 |  | simp1 1137 | . . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | 
| 9 |  | simp2 1138 | . . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇) | 
| 10 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 11 | 10, 2 | atbase 39290 | . . . . . 6
⊢ ((◡𝐹‘𝑃) ∈ 𝐴 → (◡𝐹‘𝑃) ∈ (Base‘𝐾)) | 
| 12 | 6, 11 | syl 17 | . . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (◡𝐹‘𝑃) ∈ (Base‘𝐾)) | 
| 13 |  | simp1r 1199 | . . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻) | 
| 14 | 10, 3 | lhpbase 40000 | . . . . . 6
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) | 
| 15 | 13, 14 | syl 17 | . . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ (Base‘𝐾)) | 
| 16 | 10, 1, 3, 4 | ltrnle 40131 | . . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((◡𝐹‘𝑃) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((◡𝐹‘𝑃) ≤ 𝑊 ↔ (𝐹‘(◡𝐹‘𝑃)) ≤ (𝐹‘𝑊))) | 
| 17 | 8, 9, 12, 15, 16 | syl112anc 1376 | . . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((◡𝐹‘𝑃) ≤ 𝑊 ↔ (𝐹‘(◡𝐹‘𝑃)) ≤ (𝐹‘𝑊))) | 
| 18 | 10, 3, 4 | ltrn1o 40126 | . . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾)) | 
| 19 | 18 | 3adant3 1133 | . . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾)) | 
| 20 |  | simp3l 1202 | . . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴) | 
| 21 | 10, 2 | atbase 39290 | . . . . . . 7
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) | 
| 22 | 20, 21 | syl 17 | . . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ (Base‘𝐾)) | 
| 23 |  | f1ocnvfv2 7297 | . . . . . 6
⊢ ((𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾)) → (𝐹‘(◡𝐹‘𝑃)) = 𝑃) | 
| 24 | 19, 22, 23 | syl2anc 584 | . . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘(◡𝐹‘𝑃)) = 𝑃) | 
| 25 |  | simp1l 1198 | . . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL) | 
| 26 | 25 | hllatd 39365 | . . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ Lat) | 
| 27 | 10, 1 | latref 18486 | . . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ 𝑊 ∈ (Base‘𝐾)) → 𝑊 ≤ 𝑊) | 
| 28 | 26, 15, 27 | syl2anc 584 | . . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ≤ 𝑊) | 
| 29 | 10, 1, 3, 4 | ltrnval1 40136 | . . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑊 ∈ (Base‘𝐾) ∧ 𝑊 ≤ 𝑊)) → (𝐹‘𝑊) = 𝑊) | 
| 30 | 8, 9, 15, 28, 29 | syl112anc 1376 | . . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑊) = 𝑊) | 
| 31 | 24, 30 | breq12d 5156 | . . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘(◡𝐹‘𝑃)) ≤ (𝐹‘𝑊) ↔ 𝑃 ≤ 𝑊)) | 
| 32 | 17, 31 | bitrd 279 | . . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((◡𝐹‘𝑃) ≤ 𝑊 ↔ 𝑃 ≤ 𝑊)) | 
| 33 | 7, 32 | mtbird 325 | . 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ¬ (◡𝐹‘𝑃) ≤ 𝑊) | 
| 34 | 6, 33 | jca 511 | 1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((◡𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (◡𝐹‘𝑃) ≤ 𝑊)) |