Proof of Theorem trlval3
| Step | Hyp | Ref
| Expression |
| 1 | | simpl1 1192 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 2 | | simpl31 1255 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
| 3 | | simpl2 1193 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → 𝐹 ∈ 𝑇) |
| 4 | | simpr 484 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝐹‘𝑃) = 𝑃) |
| 5 | | trlval3.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
| 6 | | eqid 2737 |
. . . . 5
⊢
(0.‘𝐾) =
(0.‘𝐾) |
| 7 | | trlval3.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
| 8 | | trlval3.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
| 9 | | trlval3.t |
. . . . 5
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 10 | | trlval3.r |
. . . . 5
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
| 11 | 5, 6, 7, 8, 9, 10 | trl0 40172 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → (𝑅‘𝐹) = (0.‘𝐾)) |
| 12 | 1, 2, 3, 4, 11 | syl112anc 1376 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝑅‘𝐹) = (0.‘𝐾)) |
| 13 | | simpl33 1257 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄))) |
| 14 | | simpl1l 1225 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → 𝐾 ∈ HL) |
| 15 | | hlatl 39361 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
| 16 | 14, 15 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → 𝐾 ∈ AtLat) |
| 17 | 4 | oveq2d 7447 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝑃 ∨ (𝐹‘𝑃)) = (𝑃 ∨ 𝑃)) |
| 18 | | simp31l 1297 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) → 𝑃 ∈ 𝐴) |
| 19 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → 𝑃 ∈ 𝐴) |
| 20 | | trlval3.j |
. . . . . . . . 9
⊢ ∨ =
(join‘𝐾) |
| 21 | 20, 7 | hlatjidm 39370 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → (𝑃 ∨ 𝑃) = 𝑃) |
| 22 | 14, 19, 21 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝑃 ∨ 𝑃) = 𝑃) |
| 23 | 17, 22 | eqtrd 2777 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝑃 ∨ (𝐹‘𝑃)) = 𝑃) |
| 24 | 23, 19 | eqeltrd 2841 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝑃 ∨ (𝐹‘𝑃)) ∈ 𝐴) |
| 25 | | simp1 1137 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 26 | | simp2 1138 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) → 𝐹 ∈ 𝑇) |
| 27 | | simp31 1210 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
| 28 | | simp32 1211 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
| 29 | 5, 7, 8, 9 | ltrn2ateq 40182 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → ((𝐹‘𝑃) = 𝑃 ↔ (𝐹‘𝑄) = 𝑄)) |
| 30 | 25, 26, 27, 28, 29 | syl13anc 1374 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) → ((𝐹‘𝑃) = 𝑃 ↔ (𝐹‘𝑄) = 𝑄)) |
| 31 | 30 | biimpa 476 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝐹‘𝑄) = 𝑄) |
| 32 | 31 | oveq2d 7447 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝑄 ∨ (𝐹‘𝑄)) = (𝑄 ∨ 𝑄)) |
| 33 | | simp32l 1299 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) → 𝑄 ∈ 𝐴) |
| 34 | 33 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → 𝑄 ∈ 𝐴) |
| 35 | 20, 7 | hlatjidm 39370 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → (𝑄 ∨ 𝑄) = 𝑄) |
| 36 | 14, 34, 35 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝑄 ∨ 𝑄) = 𝑄) |
| 37 | 32, 36 | eqtrd 2777 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝑄 ∨ (𝐹‘𝑄)) = 𝑄) |
| 38 | 37, 34 | eqeltrd 2841 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝑄 ∨ (𝐹‘𝑄)) ∈ 𝐴) |
| 39 | | trlval3.m |
. . . . . 6
⊢ ∧ =
(meet‘𝐾) |
| 40 | 39, 6, 7 | atnem0 39319 |
. . . . 5
⊢ ((𝐾 ∈ AtLat ∧ (𝑃 ∨ (𝐹‘𝑃)) ∈ 𝐴 ∧ (𝑄 ∨ (𝐹‘𝑄)) ∈ 𝐴) → ((𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)) ↔ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) = (0.‘𝐾))) |
| 41 | 16, 24, 38, 40 | syl3anc 1373 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → ((𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)) ↔ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) = (0.‘𝐾))) |
| 42 | 13, 41 | mpbid 232 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) = (0.‘𝐾)) |
| 43 | 12, 42 | eqtr4d 2780 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) = 𝑃) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄)))) |
| 44 | | simpl1 1192 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 45 | | simpl2 1193 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝐹 ∈ 𝑇) |
| 46 | | simpl31 1255 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
| 47 | 5, 20, 39, 7, 8, 9,
10 | trlval2 40165 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊)) |
| 48 | 44, 45, 46, 47 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊)) |
| 49 | | simpl1l 1225 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝐾 ∈ HL) |
| 50 | 49 | hllatd 39365 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝐾 ∈ Lat) |
| 51 | 18 | adantr 480 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝑃 ∈ 𝐴) |
| 52 | 5, 7, 8, 9 | ltrnat 40142 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴) |
| 53 | 44, 45, 51, 52 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝐹‘𝑃) ∈ 𝐴) |
| 54 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 55 | 54, 20, 7 | hlatjcl 39368 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ 𝐴) → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾)) |
| 56 | 49, 51, 53, 55 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾)) |
| 57 | | simpl1r 1226 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝑊 ∈ 𝐻) |
| 58 | 54, 8 | lhpbase 40000 |
. . . . . . 7
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
| 59 | 57, 58 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝑊 ∈ (Base‘𝐾)) |
| 60 | 54, 5, 39 | latmle1 18509 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ≤ (𝑃 ∨ (𝐹‘𝑃))) |
| 61 | 50, 56, 59, 60 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ≤ (𝑃 ∨ (𝐹‘𝑃))) |
| 62 | 48, 61 | eqbrtrd 5165 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) ≤ (𝑃 ∨ (𝐹‘𝑃))) |
| 63 | | simpl32 1256 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
| 64 | 5, 20, 39, 7, 8, 9,
10 | trlval2 40165 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑄 ∨ (𝐹‘𝑄)) ∧ 𝑊)) |
| 65 | 44, 45, 63, 64 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) = ((𝑄 ∨ (𝐹‘𝑄)) ∧ 𝑊)) |
| 66 | 33 | adantr 480 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝑄 ∈ 𝐴) |
| 67 | 5, 7, 8, 9 | ltrnat 40142 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐴) → (𝐹‘𝑄) ∈ 𝐴) |
| 68 | 44, 45, 66, 67 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝐹‘𝑄) ∈ 𝐴) |
| 69 | 54, 20, 7 | hlatjcl 39368 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ (𝐹‘𝑄) ∈ 𝐴) → (𝑄 ∨ (𝐹‘𝑄)) ∈ (Base‘𝐾)) |
| 70 | 49, 66, 68, 69 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑄 ∨ (𝐹‘𝑄)) ∈ (Base‘𝐾)) |
| 71 | 54, 5, 39 | latmle1 18509 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ (𝐹‘𝑄)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑄 ∨ (𝐹‘𝑄)) ∧ 𝑊) ≤ (𝑄 ∨ (𝐹‘𝑄))) |
| 72 | 50, 70, 59, 71 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → ((𝑄 ∨ (𝐹‘𝑄)) ∧ 𝑊) ≤ (𝑄 ∨ (𝐹‘𝑄))) |
| 73 | 65, 72 | eqbrtrd 5165 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) ≤ (𝑄 ∨ (𝐹‘𝑄))) |
| 74 | 54, 8, 9, 10 | trlcl 40166 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) ∈ (Base‘𝐾)) |
| 75 | 44, 45, 74 | syl2anc 584 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) ∈ (Base‘𝐾)) |
| 76 | 54, 5, 39 | latlem12 18511 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ ((𝑅‘𝐹) ∈ (Base‘𝐾) ∧ (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾) ∧ (𝑄 ∨ (𝐹‘𝑄)) ∈ (Base‘𝐾))) → (((𝑅‘𝐹) ≤ (𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑅‘𝐹) ≤ (𝑄 ∨ (𝐹‘𝑄))) ↔ (𝑅‘𝐹) ≤ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))))) |
| 77 | 50, 75, 56, 70, 76 | syl13anc 1374 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (((𝑅‘𝐹) ≤ (𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑅‘𝐹) ≤ (𝑄 ∨ (𝐹‘𝑄))) ↔ (𝑅‘𝐹) ≤ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))))) |
| 78 | 62, 73, 77 | mpbi2and 712 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) ≤ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄)))) |
| 79 | 49, 15 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝐾 ∈ AtLat) |
| 80 | | simpr 484 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝐹‘𝑃) ≠ 𝑃) |
| 81 | 5, 7, 8, 9, 10 | trlat 40171 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑅‘𝐹) ∈ 𝐴) |
| 82 | 44, 46, 45, 80, 81 | syl112anc 1376 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) ∈ 𝐴) |
| 83 | 54, 39 | latmcl 18485 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾) ∧ (𝑄 ∨ (𝐹‘𝑄)) ∈ (Base‘𝐾)) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) ∈ (Base‘𝐾)) |
| 84 | 50, 56, 70, 83 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) ∈ (Base‘𝐾)) |
| 85 | 54, 5, 6, 7 | atlen0 39311 |
. . . . . . 7
⊢ (((𝐾 ∈ AtLat ∧ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) ∈ (Base‘𝐾) ∧ (𝑅‘𝐹) ∈ 𝐴) ∧ (𝑅‘𝐹) ≤ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄)))) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) ≠ (0.‘𝐾)) |
| 86 | 79, 84, 82, 78, 85 | syl31anc 1375 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) ≠ (0.‘𝐾)) |
| 87 | 86 | neneqd 2945 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → ¬ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) = (0.‘𝐾)) |
| 88 | | simpl33 1257 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄))) |
| 89 | 20, 39, 6, 7 | 2atmat0 39528 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ 𝐴) ∧ (𝑄 ∈ 𝐴 ∧ (𝐹‘𝑄) ∈ 𝐴 ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) → (((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) ∈ 𝐴 ∨ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) = (0.‘𝐾))) |
| 90 | 49, 51, 53, 66, 68, 88, 89 | syl33anc 1387 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) ∈ 𝐴 ∨ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) = (0.‘𝐾))) |
| 91 | 90 | ord 865 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (¬ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) ∈ 𝐴 → ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) = (0.‘𝐾))) |
| 92 | 87, 91 | mt3d 148 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) ∈ 𝐴) |
| 93 | 5, 7 | atcmp 39312 |
. . . 4
⊢ ((𝐾 ∈ AtLat ∧ (𝑅‘𝐹) ∈ 𝐴 ∧ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) ∈ 𝐴) → ((𝑅‘𝐹) ≤ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) ↔ (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))))) |
| 94 | 79, 82, 92, 93 | syl3anc 1373 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → ((𝑅‘𝐹) ≤ ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))) ↔ (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄))))) |
| 95 | 78, 94 | mpbid 232 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄)))) |
| 96 | 43, 95 | pm2.61dane 3029 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ∨ (𝐹‘𝑃)) ≠ (𝑄 ∨ (𝐹‘𝑄)))) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑄 ∨ (𝐹‘𝑄)))) |