Proof of Theorem cdlemg11b
Step | Hyp | Ref
| Expression |
1 | | simp33 1099 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄)) |
2 | | simpl1 1064 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
3 | | simpl31 1142 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝐺 ∈ 𝑇) |
4 | | simpl2l 1114 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
5 | | cdlemg8.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
6 | | cdlemg8.j |
. . . . . . 7
⊢ ∨ =
(join‘𝐾) |
7 | | cdlemg8.m |
. . . . . . 7
⊢ ∧ =
(meet‘𝐾) |
8 | | cdlemg8.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
9 | | cdlemg8.h |
. . . . . . 7
⊢ 𝐻 = (LHyp‘𝐾) |
10 | | cdlemg8.t |
. . . . . . 7
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
11 | | cdlemg10.r |
. . . . . . 7
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
12 | 5, 6, 7, 8, 9, 10,
11 | trlval2 35450 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊)) |
13 | 2, 3, 4, 12 | syl3anc 1326 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊)) |
14 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝐾) =
(Base‘𝐾) |
15 | | simpl1l 1112 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝐾 ∈ HL) |
16 | | hllat 34650 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝐾 ∈ Lat) |
18 | | simp2ll 1128 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → 𝑃 ∈ 𝐴) |
19 | 18 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑃 ∈ 𝐴) |
20 | 14, 8 | atbase 34576 |
. . . . . . . . 9
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑃 ∈ (Base‘𝐾)) |
22 | 14, 9, 10 | ltrncl 35411 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ (Base‘𝐾)) → (𝐺‘𝑃) ∈ (Base‘𝐾)) |
23 | 2, 3, 21, 22 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐺‘𝑃) ∈ (Base‘𝐾)) |
24 | 14, 6 | latjcl 17051 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝐺‘𝑃) ∈ (Base‘𝐾)) → (𝑃 ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾)) |
25 | 17, 21, 23, 24 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾)) |
26 | | simpl1r 1113 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑊 ∈ 𝐻) |
27 | 14, 9 | lhpbase 35284 |
. . . . . . . 8
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑊 ∈ (Base‘𝐾)) |
29 | 14, 7 | latmcl 17052 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ∈ (Base‘𝐾)) |
30 | 17, 25, 28, 29 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ∈ (Base‘𝐾)) |
31 | | simpl2r 1115 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑄 ∈ 𝐴) |
32 | 14, 8 | atbase 34576 |
. . . . . . . 8
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾)) |
33 | 31, 32 | syl 17 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑄 ∈ (Base‘𝐾)) |
34 | 14, 6 | latjcl 17051 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
35 | 17, 21, 33, 34 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
36 | 14, 5, 7 | latmle1 17076 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ≤ (𝑃 ∨ (𝐺‘𝑃))) |
37 | 17, 25, 28, 36 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ≤ (𝑃 ∨ (𝐺‘𝑃))) |
38 | 14, 5, 6 | latlej1 17060 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → 𝑃 ≤ (𝑃 ∨ 𝑄)) |
39 | 17, 21, 33, 38 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑃 ≤ (𝑃 ∨ 𝑄)) |
40 | 14, 9, 10 | ltrncl 35411 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑄 ∈ (Base‘𝐾)) → (𝐺‘𝑄) ∈ (Base‘𝐾)) |
41 | 2, 3, 33, 40 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐺‘𝑄) ∈ (Base‘𝐾)) |
42 | 14, 5, 6 | latlej1 17060 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ (𝐺‘𝑃) ∈ (Base‘𝐾) ∧ (𝐺‘𝑄) ∈ (Base‘𝐾)) → (𝐺‘𝑃) ≤ ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) |
43 | 17, 23, 41, 42 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐺‘𝑃) ≤ ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) |
44 | | simpr 477 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) |
45 | 43, 44 | breqtrrd 4681 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐺‘𝑃) ≤ (𝑃 ∨ 𝑄)) |
46 | 14, 5, 6 | latjle12 17062 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ (𝐺‘𝑃) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))) → ((𝑃 ≤ (𝑃 ∨ 𝑄) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ 𝑄))) |
47 | 17, 21, 23, 35, 46 | syl13anc 1328 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → ((𝑃 ≤ (𝑃 ∨ 𝑄) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ 𝑄))) |
48 | 39, 45, 47 | mpbi2and 956 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ 𝑄)) |
49 | 14, 5, 17, 30, 25, 35, 37, 48 | lattrd 17058 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ≤ (𝑃 ∨ 𝑄)) |
50 | 13, 49 | eqbrtrd 4675 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄)) |
51 | 50 | ex 450 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄)) → (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) |
52 | 51 | necon3bd 2808 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) → (𝑃 ∨ 𝑄) ≠ ((𝐺‘𝑃) ∨ (𝐺‘𝑄)))) |
53 | 1, 52 | mpd 15 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝑃 ∨ 𝑄) ≠ ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) |