Step | Hyp | Ref
| Expression |
1 | | simp-4l 782 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π) β§ βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π)) β§ π₯ β π΅) β πΎ β HL) |
2 | | ltrneq.h |
. . . . . . . . 9
β’ π» = (LHypβπΎ) |
3 | | eqid 2733 |
. . . . . . . . 9
β’
(LAutβπΎ) =
(LAutβπΎ) |
4 | | ltrneq.t |
. . . . . . . . 9
β’ π = ((LTrnβπΎ)βπ) |
5 | 2, 3, 4 | ltrnlaut 38636 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ β (LAutβπΎ)) |
6 | 5 | ad2antrr 725 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π) β§ βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π)) β§ π₯ β π΅) β πΉ β (LAutβπΎ)) |
7 | | simpr 486 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π) β§ βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π)) β§ π₯ β π΅) β π₯ β π΅) |
8 | | simplll 774 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π) β§ π β π΄) β§ π β€ π) β (πΎ β HL β§ π β π»)) |
9 | | simpllr 775 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π) β§ π β π΄) β§ π β€ π) β πΉ β π) |
10 | | ltrneq.b |
. . . . . . . . . . . . . . 15
β’ π΅ = (BaseβπΎ) |
11 | | ltrneq.a |
. . . . . . . . . . . . . . 15
β’ π΄ = (AtomsβπΎ) |
12 | 10, 11 | atbase 37801 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β π β π΅) |
13 | 12 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π) β§ π β π΄) β§ π β€ π) β π β π΅) |
14 | | simpr 486 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π) β§ π β π΄) β§ π β€ π) β π β€ π) |
15 | | ltrneq.l |
. . . . . . . . . . . . . 14
β’ β€ =
(leβπΎ) |
16 | 10, 15, 2, 4 | ltrnval1 38647 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΅ β§ π β€ π)) β (πΉβπ) = π) |
17 | 8, 9, 13, 14, 16 | syl112anc 1375 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π) β§ π β π΄) β§ π β€ π) β (πΉβπ) = π) |
18 | 17 | ex 414 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β π΄) β (π β€ π β (πΉβπ) = π)) |
19 | | pm2.61 191 |
. . . . . . . . . . 11
β’ ((π β€ π β (πΉβπ) = π) β ((Β¬ π β€ π β (πΉβπ) = π) β (πΉβπ) = π)) |
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β π΄) β ((Β¬ π β€ π β (πΉβπ) = π) β (πΉβπ) = π)) |
21 | 20 | ralimdva 3161 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π) β βπ β π΄ (πΉβπ) = π)) |
22 | 21 | imp 408 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π)) β βπ β π΄ (πΉβπ) = π) |
23 | 22 | adantr 482 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π) β§ βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π)) β§ π₯ β π΅) β βπ β π΄ (πΉβπ) = π) |
24 | 10, 11, 3 | lauteq 38608 |
. . . . . . 7
β’ (((πΎ β HL β§ πΉ β (LAutβπΎ) β§ π₯ β π΅) β§ βπ β π΄ (πΉβπ) = π) β (πΉβπ₯) = π₯) |
25 | 1, 6, 7, 23, 24 | syl31anc 1374 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π) β§ βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π)) β§ π₯ β π΅) β (πΉβπ₯) = π₯) |
26 | | fvresi 7123 |
. . . . . . 7
β’ (π₯ β π΅ β (( I βΎ π΅)βπ₯) = π₯) |
27 | 26 | adantl 483 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π) β§ βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π)) β§ π₯ β π΅) β (( I βΎ π΅)βπ₯) = π₯) |
28 | 25, 27 | eqtr4d 2776 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π) β§ βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π)) β§ π₯ β π΅) β (πΉβπ₯) = (( I βΎ π΅)βπ₯)) |
29 | 28 | ralrimiva 3140 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π)) β βπ₯ β π΅ (πΉβπ₯) = (( I βΎ π΅)βπ₯)) |
30 | 10, 2, 4 | ltrn1o 38637 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ:π΅β1-1-ontoβπ΅) |
31 | 30 | adantr 482 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π)) β πΉ:π΅β1-1-ontoβπ΅) |
32 | | f1ofn 6789 |
. . . . . 6
β’ (πΉ:π΅β1-1-ontoβπ΅ β πΉ Fn π΅) |
33 | 31, 32 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π)) β πΉ Fn π΅) |
34 | | fnresi 6634 |
. . . . 5
β’ ( I
βΎ π΅) Fn π΅ |
35 | | eqfnfv 6986 |
. . . . 5
β’ ((πΉ Fn π΅ β§ ( I βΎ π΅) Fn π΅) β (πΉ = ( I βΎ π΅) β βπ₯ β π΅ (πΉβπ₯) = (( I βΎ π΅)βπ₯))) |
36 | 33, 34, 35 | sylancl 587 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π)) β (πΉ = ( I βΎ π΅) β βπ₯ β π΅ (πΉβπ₯) = (( I βΎ π΅)βπ₯))) |
37 | 29, 36 | mpbird 257 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π)) β πΉ = ( I βΎ π΅)) |
38 | 37 | ex 414 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π) β πΉ = ( I βΎ π΅))) |
39 | 12 | adantl 483 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β π΄) β π β π΅) |
40 | | fvresi 7123 |
. . . . . 6
β’ (π β π΅ β (( I βΎ π΅)βπ) = π) |
41 | 39, 40 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β π΄) β (( I βΎ π΅)βπ) = π) |
42 | | fveq1 6845 |
. . . . . 6
β’ (πΉ = ( I βΎ π΅) β (πΉβπ) = (( I βΎ π΅)βπ)) |
43 | 42 | eqeq1d 2735 |
. . . . 5
β’ (πΉ = ( I βΎ π΅) β ((πΉβπ) = π β (( I βΎ π΅)βπ) = π)) |
44 | 41, 43 | syl5ibrcom 247 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β π΄) β (πΉ = ( I βΎ π΅) β (πΉβπ) = π)) |
45 | 44 | a1dd 50 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β π΄) β (πΉ = ( I βΎ π΅) β (Β¬ π β€ π β (πΉβπ) = π))) |
46 | 45 | ralrimdva 3148 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΉ = ( I βΎ π΅) β βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π))) |
47 | 38, 46 | impbid 211 |
1
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π) β πΉ = ( I βΎ π΅))) |