Proof of Theorem cdlemefrs29bpre0
Step | Hyp | Ref
| Expression |
1 | | df-ral 3068 |
. . 3
⊢
(∀𝑠 ∈
𝐴 (((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))) ↔ ∀𝑠(𝑠 ∈ 𝐴 → (((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))))) |
2 | | anass 468 |
. . . . . . 7
⊢ (((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) ↔ (𝑠 ∈ 𝐴 ∧ ((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅))) |
3 | 2 | imbi1i 349 |
. . . . . 6
⊢ ((((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))) ↔ ((𝑠 ∈ 𝐴 ∧ ((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅)) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)))) |
4 | | impexp 450 |
. . . . . 6
⊢ ((((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))) ↔ ((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) → ((𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅 → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))))) |
5 | | impexp 450 |
. . . . . 6
⊢ (((𝑠 ∈ 𝐴 ∧ ((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅)) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))) ↔ (𝑠 ∈ 𝐴 → (((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))))) |
6 | 3, 4, 5 | 3bitr3ri 301 |
. . . . 5
⊢ ((𝑠 ∈ 𝐴 → (((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)))) ↔ ((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) → ((𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅 → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))))) |
7 | | simpl11 1246 |
. . . . . . . . . . . 12
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
8 | | simpl2r 1225 |
. . . . . . . . . . . 12
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) |
9 | | cdlemefrs27.l |
. . . . . . . . . . . . 13
⊢ ≤ =
(le‘𝐾) |
10 | | cdlemefrs27.m |
. . . . . . . . . . . . 13
⊢ ∧ =
(meet‘𝐾) |
11 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(0.‘𝐾) =
(0.‘𝐾) |
12 | | cdlemefrs27.a |
. . . . . . . . . . . . 13
⊢ 𝐴 = (Atoms‘𝐾) |
13 | | cdlemefrs27.h |
. . . . . . . . . . . . 13
⊢ 𝐻 = (LHyp‘𝐾) |
14 | 9, 10, 11, 12, 13 | lhpmat 37971 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝑅 ∧ 𝑊) = (0.‘𝐾)) |
15 | 7, 8, 14 | syl2anc 583 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → (𝑅 ∧ 𝑊) = (0.‘𝐾)) |
16 | 15 | oveq2d 7271 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → (𝑠 ∨ (𝑅 ∧ 𝑊)) = (𝑠 ∨ (0.‘𝐾))) |
17 | | simp11l 1282 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → 𝐾 ∈ HL) |
18 | | hlol 37302 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → 𝐾 ∈ OL) |
20 | 19 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → 𝐾 ∈ OL) |
21 | | simprl 767 |
. . . . . . . . . . . 12
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → 𝑠 ∈ 𝐴) |
22 | | cdlemefrs27.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝐾) |
23 | 22, 12 | atbase 37230 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ 𝐴 → 𝑠 ∈ 𝐵) |
24 | 21, 23 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → 𝑠 ∈ 𝐵) |
25 | | cdlemefrs27.j |
. . . . . . . . . . . 12
⊢ ∨ =
(join‘𝐾) |
26 | 22, 25, 11 | olj01 37166 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ OL ∧ 𝑠 ∈ 𝐵) → (𝑠 ∨ (0.‘𝐾)) = 𝑠) |
27 | 20, 24, 26 | syl2anc 583 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → (𝑠 ∨ (0.‘𝐾)) = 𝑠) |
28 | 16, 27 | eqtrd 2778 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑠) |
29 | 28 | eqeq1d 2740 |
. . . . . . . 8
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → ((𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅 ↔ 𝑠 = 𝑅)) |
30 | 15 | oveq2d 7271 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → (𝑁 ∨ (𝑅 ∧ 𝑊)) = (𝑁 ∨ (0.‘𝐾))) |
31 | | simpl1 1189 |
. . . . . . . . . . . 12
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) |
32 | | simpl2l 1224 |
. . . . . . . . . . . 12
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → 𝑃 ≠ 𝑄) |
33 | | simprr 769 |
. . . . . . . . . . . 12
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) |
34 | | cdlemefrs27.nb |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄 ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → 𝑁 ∈ 𝐵) |
35 | 31, 32, 21, 33, 34 | syl112anc 1372 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → 𝑁 ∈ 𝐵) |
36 | 22, 25, 11 | olj01 37166 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ OL ∧ 𝑁 ∈ 𝐵) → (𝑁 ∨ (0.‘𝐾)) = 𝑁) |
37 | 20, 35, 36 | syl2anc 583 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → (𝑁 ∨ (0.‘𝐾)) = 𝑁) |
38 | 30, 37 | eqtrd 2778 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → (𝑁 ∨ (𝑅 ∧ 𝑊)) = 𝑁) |
39 | 38 | eqeq2d 2749 |
. . . . . . . 8
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → (𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)) ↔ 𝑧 = 𝑁)) |
40 | 29, 39 | imbi12d 344 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) ∧ (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑))) → (((𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅 → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))) ↔ (𝑠 = 𝑅 → 𝑧 = 𝑁))) |
41 | 40 | pm5.74da 800 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → (((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) → ((𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅 → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)))) ↔ ((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) → (𝑠 = 𝑅 → 𝑧 = 𝑁)))) |
42 | | impexp 450 |
. . . . . . 7
⊢ ((((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) ∧ 𝑠 = 𝑅) → 𝑧 = 𝑁) ↔ ((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) → (𝑠 = 𝑅 → 𝑧 = 𝑁))) |
43 | | simp2rl 1240 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → 𝑅 ∈ 𝐴) |
44 | | simp2rr 1241 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → ¬ 𝑅 ≤ 𝑊) |
45 | | simp3 1136 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → 𝜓) |
46 | | eleq1 2826 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑅 → (𝑠 ∈ 𝐴 ↔ 𝑅 ∈ 𝐴)) |
47 | | breq1 5073 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑅 → (𝑠 ≤ 𝑊 ↔ 𝑅 ≤ 𝑊)) |
48 | 47 | notbid 317 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑅 → (¬ 𝑠 ≤ 𝑊 ↔ ¬ 𝑅 ≤ 𝑊)) |
49 | | cdlemefrs27.eq |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑅 → (𝜑 ↔ 𝜓)) |
50 | 48, 49 | anbi12d 630 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑅 → ((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ↔ (¬ 𝑅 ≤ 𝑊 ∧ 𝜓))) |
51 | 46, 50 | anbi12d 630 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑅 → ((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) ↔ (𝑅 ∈ 𝐴 ∧ (¬ 𝑅 ≤ 𝑊 ∧ 𝜓)))) |
52 | 51 | biimprcd 249 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ 𝐴 ∧ (¬ 𝑅 ≤ 𝑊 ∧ 𝜓)) → (𝑠 = 𝑅 → (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)))) |
53 | 43, 44, 45, 52 | syl12anc 833 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → (𝑠 = 𝑅 → (𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)))) |
54 | 53 | pm4.71rd 562 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → (𝑠 = 𝑅 ↔ ((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) ∧ 𝑠 = 𝑅))) |
55 | 54 | imbi1d 341 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → ((𝑠 = 𝑅 → 𝑧 = 𝑁) ↔ (((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) ∧ 𝑠 = 𝑅) → 𝑧 = 𝑁))) |
56 | | eqcom 2745 |
. . . . . . . . 9
⊢ (𝑧 = 𝑁 ↔ 𝑁 = 𝑧) |
57 | 56 | imbi2i 335 |
. . . . . . . 8
⊢ ((𝑠 = 𝑅 → 𝑧 = 𝑁) ↔ (𝑠 = 𝑅 → 𝑁 = 𝑧)) |
58 | 55, 57 | bitr3di 285 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → ((((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) ∧ 𝑠 = 𝑅) → 𝑧 = 𝑁) ↔ (𝑠 = 𝑅 → 𝑁 = 𝑧))) |
59 | 42, 58 | bitr3id 284 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → (((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) → (𝑠 = 𝑅 → 𝑧 = 𝑁)) ↔ (𝑠 = 𝑅 → 𝑁 = 𝑧))) |
60 | 41, 59 | bitrd 278 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → (((𝑠 ∈ 𝐴 ∧ (¬ 𝑠 ≤ 𝑊 ∧ 𝜑)) → ((𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅 → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)))) ↔ (𝑠 = 𝑅 → 𝑁 = 𝑧))) |
61 | 6, 60 | syl5bb 282 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → ((𝑠 ∈ 𝐴 → (((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)))) ↔ (𝑠 = 𝑅 → 𝑁 = 𝑧))) |
62 | 61 | albidv 1924 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → (∀𝑠(𝑠 ∈ 𝐴 → (((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊)))) ↔ ∀𝑠(𝑠 = 𝑅 → 𝑁 = 𝑧))) |
63 | 1, 62 | syl5bb 282 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → (∀𝑠 ∈ 𝐴 (((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))) ↔ ∀𝑠(𝑠 = 𝑅 → 𝑁 = 𝑧))) |
64 | | nfcv 2906 |
. . . . 5
⊢
Ⅎ𝑠𝑧 |
65 | 64 | csbiebg 3861 |
. . . 4
⊢ (𝑅 ∈ 𝐴 → (∀𝑠(𝑠 = 𝑅 → 𝑁 = 𝑧) ↔ ⦋𝑅 / 𝑠⦌𝑁 = 𝑧)) |
66 | 43, 65 | syl 17 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → (∀𝑠(𝑠 = 𝑅 → 𝑁 = 𝑧) ↔ ⦋𝑅 / 𝑠⦌𝑁 = 𝑧)) |
67 | | eqcom 2745 |
. . 3
⊢
(⦋𝑅 /
𝑠⦌𝑁 = 𝑧 ↔ 𝑧 = ⦋𝑅 / 𝑠⦌𝑁) |
68 | 66, 67 | bitrdi 286 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → (∀𝑠(𝑠 = 𝑅 → 𝑁 = 𝑧) ↔ 𝑧 = ⦋𝑅 / 𝑠⦌𝑁)) |
69 | 63, 68 | bitrd 278 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝜓) → (∀𝑠 ∈ 𝐴 (((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) → 𝑧 = (𝑁 ∨ (𝑅 ∧ 𝑊))) ↔ 𝑧 = ⦋𝑅 / 𝑠⦌𝑁)) |