Step | Hyp | Ref
| Expression |
1 | | cdlemg1c.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
2 | | cdlemg1c.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
3 | | cdlemg1c.h |
. . . . . . . 8
β’ π» = (LHypβπΎ) |
4 | | cdlemg1c.t |
. . . . . . . 8
β’ π = ((LTrnβπΎ)βπ) |
5 | 1, 2, 3, 4 | ltrnel 38602 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) |
6 | 5 | 3expa 1118 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) |
7 | 6 | simpld 495 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) β π΄) |
8 | | simprr 771 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β Β¬ π β€ π) |
9 | 6 | simprd 496 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β Β¬ (πΉβπ) β€ π) |
10 | | simpll 765 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΎ β HL β§ π β π»)) |
11 | | simpr 485 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β π΄ β§ Β¬ π β€ π)) |
12 | | simplr 767 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) |
13 | 1, 2, 3, 4 | cdlemeiota 39048 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β πΉ = (β©π β π (πβπ) = (πΉβπ))) |
14 | 10, 11, 12, 13 | syl3anc 1371 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ = (β©π β π (πβπ) = (πΉβπ))) |
15 | | breq1 5108 |
. . . . . . . 8
β’ (π = (πΉβπ) β (π β€ π β (πΉβπ) β€ π)) |
16 | 15 | notbid 317 |
. . . . . . 7
β’ (π = (πΉβπ) β (Β¬ π β€ π β Β¬ (πΉβπ) β€ π)) |
17 | | eqeq2 2748 |
. . . . . . . . 9
β’ (π = (πΉβπ) β ((πβπ) = π β (πβπ) = (πΉβπ))) |
18 | 17 | riotabidv 7315 |
. . . . . . . 8
β’ (π = (πΉβπ) β (β©π β π (πβπ) = π) = (β©π β π (πβπ) = (πΉβπ))) |
19 | 18 | eqeq2d 2747 |
. . . . . . 7
β’ (π = (πΉβπ) β (πΉ = (β©π β π (πβπ) = π) β πΉ = (β©π β π (πβπ) = (πΉβπ)))) |
20 | 16, 19 | 3anbi23d 1439 |
. . . . . 6
β’ (π = (πΉβπ) β ((Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π)) β (Β¬ π β€ π β§ Β¬ (πΉβπ) β€ π β§ πΉ = (β©π β π (πβπ) = (πΉβπ))))) |
21 | 20 | rspcev 3581 |
. . . . 5
β’ (((πΉβπ) β π΄ β§ (Β¬ π β€ π β§ Β¬ (πΉβπ) β€ π β§ πΉ = (β©π β π (πβπ) = (πΉβπ)))) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π))) |
22 | 7, 8, 9, 14, 21 | syl13anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π))) |
23 | 1, 2, 3 | lhpexnle 38469 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β βπ β π΄ Β¬ π β€ π) |
24 | 23 | adantr 481 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β βπ β π΄ Β¬ π β€ π) |
25 | 22, 24 | reximddv 3168 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β βπ β π΄ βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π))) |
26 | 25 | ex 413 |
. 2
β’ ((πΎ β HL β§ π β π») β (πΉ β π β βπ β π΄ βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π)))) |
27 | | simp1 1136 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π))) β (πΎ β HL β§ π β π»)) |
28 | | simp2l 1199 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π))) β π β π΄) |
29 | | simp31 1209 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π))) β Β¬ π β€ π) |
30 | 28, 29 | jca 512 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π))) β (π β π΄ β§ Β¬ π β€ π)) |
31 | | simp2r 1200 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π))) β π β π΄) |
32 | | simp32 1210 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π))) β Β¬ π β€ π) |
33 | 31, 32 | jca 512 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π))) β (π β π΄ β§ Β¬ π β€ π)) |
34 | | simp33 1211 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π))) β πΉ = (β©π β π (πβπ) = π)) |
35 | 1, 2, 3, 4 | cdlemg1ci2 39049 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ = (β©π β π (πβπ) = π)) β πΉ β π) |
36 | 27, 30, 33, 34, 35 | syl31anc 1373 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π))) β πΉ β π) |
37 | 36 | 3exp 1119 |
. . 3
β’ ((πΎ β HL β§ π β π») β ((π β π΄ β§ π β π΄) β ((Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π)) β πΉ β π))) |
38 | 37 | rexlimdvv 3204 |
. 2
β’ ((πΎ β HL β§ π β π») β (βπ β π΄ βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π)) β πΉ β π)) |
39 | 26, 38 | impbid 211 |
1
β’ ((πΎ β HL β§ π β π») β (πΉ β π β βπ β π΄ βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π)))) |