Step | Hyp | Ref
| Expression |
1 | | eldmg 5859 |
. . . 4
β’ (πΉ β dom
βπ β (πΉ β dom βπ
β βπ₯ πΉ βπ
π₯)) |
2 | 1 | ibi 267 |
. . 3
β’ (πΉ β dom
βπ β βπ₯ πΉ βπ π₯) |
3 | | simpr 486 |
. . . . . 6
β’ ((π β§ πΉ βπ π₯) β πΉ βπ π₯) |
4 | | rlimrel 15382 |
. . . . . . . . . . . 12
β’ Rel
βπ |
5 | 4 | brrelex1i 5693 |
. . . . . . . . . . 11
β’ (πΉ βπ
π₯ β πΉ β V) |
6 | 5 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ πΉ βπ π₯) β πΉ β V) |
7 | | vex 3452 |
. . . . . . . . . . 11
β’ π₯ β V |
8 | 7 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ πΉ βπ π₯) β π₯ β V) |
9 | | breldmg 5870 |
. . . . . . . . . 10
β’ ((πΉ β V β§ π₯ β V β§ πΉ βπ
π₯) β πΉ β dom βπ
) |
10 | 6, 8, 3, 9 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ πΉ βπ π₯) β πΉ β dom βπ
) |
11 | | breq2 5114 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β (πΉ βπ π¦ β πΉ βπ π₯)) |
12 | 11 | biimprd 248 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β (πΉ βπ π₯ β πΉ βπ π¦)) |
13 | 12 | spimevw 1999 |
. . . . . . . . . . 11
β’ (πΉ βπ
π₯ β βπ¦ πΉ βπ π¦) |
14 | 13 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ πΉ βπ π₯) β βπ¦ πΉ βπ π¦) |
15 | | rlimdmafv2.1 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:π΄βΆβ) |
16 | 15 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΉ βπ π₯) β πΉ:π΄βΆβ) |
17 | 16 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ πΉ βπ π₯) β§ (πΉ βπ π¦ β§ πΉ βπ π§)) β πΉ:π΄βΆβ) |
18 | | rlimdmafv2.2 |
. . . . . . . . . . . . . . 15
β’ (π β sup(π΄, β*, < ) =
+β) |
19 | 18 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΉ βπ π₯) β sup(π΄, β*, < ) =
+β) |
20 | 19 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ πΉ βπ π₯) β§ (πΉ βπ π¦ β§ πΉ βπ π§)) β sup(π΄, β*, < ) =
+β) |
21 | | simprl 770 |
. . . . . . . . . . . . 13
β’ (((π β§ πΉ βπ π₯) β§ (πΉ βπ π¦ β§ πΉ βπ π§)) β πΉ βπ π¦) |
22 | | simprr 772 |
. . . . . . . . . . . . 13
β’ (((π β§ πΉ βπ π₯) β§ (πΉ βπ π¦ β§ πΉ βπ π§)) β πΉ βπ π§) |
23 | 17, 20, 21, 22 | rlimuni 15439 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ βπ π₯) β§ (πΉ βπ π¦ β§ πΉ βπ π§)) β π¦ = π§) |
24 | 23 | ex 414 |
. . . . . . . . . . 11
β’ ((π β§ πΉ βπ π₯) β ((πΉ βπ π¦ β§ πΉ βπ π§) β π¦ = π§)) |
25 | 24 | alrimivv 1932 |
. . . . . . . . . 10
β’ ((π β§ πΉ βπ π₯) β βπ¦βπ§((πΉ βπ π¦ β§ πΉ βπ π§) β π¦ = π§)) |
26 | | breq2 5114 |
. . . . . . . . . . 11
β’ (π¦ = π§ β (πΉ βπ π¦ β πΉ βπ π§)) |
27 | 26 | eu4 2616 |
. . . . . . . . . 10
β’
(β!π¦ πΉ βπ
π¦ β (βπ¦ πΉ βπ π¦ β§ βπ¦βπ§((πΉ βπ π¦ β§ πΉ βπ π§) β π¦ = π§))) |
28 | 14, 25, 27 | sylanbrc 584 |
. . . . . . . . 9
β’ ((π β§ πΉ βπ π₯) β β!π¦ πΉ βπ π¦) |
29 | | dfdfat2 45434 |
. . . . . . . . 9
β’ (
βπ defAt πΉ β (πΉ β dom βπ
β§ β!π¦ πΉ βπ
π¦)) |
30 | 10, 28, 29 | sylanbrc 584 |
. . . . . . . 8
β’ ((π β§ πΉ βπ π₯) β
βπ defAt πΉ) |
31 | | dfatafv2iota 45516 |
. . . . . . . 8
β’ (
βπ defAt πΉ β ( βπ
''''πΉ) =
(β©π€πΉ βπ π€)) |
32 | 30, 31 | syl 17 |
. . . . . . 7
β’ ((π β§ πΉ βπ π₯) β (
βπ ''''πΉ) = (β©π€πΉ βπ π€)) |
33 | 15 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (πΉ βπ π₯ β§ πΉ βπ π€)) β πΉ:π΄βΆβ) |
34 | 18 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (πΉ βπ π₯ β§ πΉ βπ π€)) β sup(π΄, β*, < ) =
+β) |
35 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((π β§ (πΉ βπ π₯ β§ πΉ βπ π€)) β πΉ βπ π€) |
36 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((π β§ (πΉ βπ π₯ β§ πΉ βπ π€)) β πΉ βπ π₯) |
37 | 33, 34, 35, 36 | rlimuni 15439 |
. . . . . . . . . . . 12
β’ ((π β§ (πΉ βπ π₯ β§ πΉ βπ π€)) β π€ = π₯) |
38 | 37 | expr 458 |
. . . . . . . . . . 11
β’ ((π β§ πΉ βπ π₯) β (πΉ βπ π€ β π€ = π₯)) |
39 | | breq2 5114 |
. . . . . . . . . . . 12
β’ (π€ = π₯ β (πΉ βπ π€ β πΉ βπ π₯)) |
40 | 3, 39 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ ((π β§ πΉ βπ π₯) β (π€ = π₯ β πΉ βπ π€)) |
41 | 38, 40 | impbid 211 |
. . . . . . . . . 10
β’ ((π β§ πΉ βπ π₯) β (πΉ βπ π€ β π€ = π₯)) |
42 | 41 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ πΉ βπ π₯) β§ π₯ β V) β (πΉ βπ π€ β π€ = π₯)) |
43 | 42 | iota5 6484 |
. . . . . . . 8
β’ (((π β§ πΉ βπ π₯) β§ π₯ β V) β (β©π€πΉ βπ π€) = π₯) |
44 | 43 | elvd 3455 |
. . . . . . 7
β’ ((π β§ πΉ βπ π₯) β (β©π€πΉ βπ π€) = π₯) |
45 | 32, 44 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ πΉ βπ π₯) β (
βπ ''''πΉ) = π₯) |
46 | 3, 45 | breqtrrd 5138 |
. . . . 5
β’ ((π β§ πΉ βπ π₯) β πΉ βπ (
βπ ''''πΉ)) |
47 | 46 | ex 414 |
. . . 4
β’ (π β (πΉ βπ π₯ β πΉ βπ (
βπ ''''πΉ))) |
48 | 47 | exlimdv 1937 |
. . 3
β’ (π β (βπ₯ πΉ βπ π₯ β πΉ βπ (
βπ ''''πΉ))) |
49 | 2, 48 | syl5 34 |
. 2
β’ (π β (πΉ β dom βπ
β πΉ
βπ ( βπ ''''πΉ))) |
50 | 4 | releldmi 5908 |
. 2
β’ (πΉ βπ (
βπ ''''πΉ) β πΉ β dom βπ
) |
51 | 49, 50 | impbid1 224 |
1
β’ (π β (πΉ β dom βπ
β πΉ
βπ ( βπ ''''πΉ))) |