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 | | rlimdmafv.1 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:π΄βΆβ) |
16 | 15 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΉ βπ π₯) β πΉ:π΄βΆβ) |
17 | 16 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ πΉ βπ π₯) β§ (πΉ βπ π¦ β§ πΉ βπ π§)) β πΉ:π΄βΆβ) |
18 | | rlimdmafv.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 | | afvfundmfveq 45444 |
. . . . . . . 8
β’ (
βπ defAt πΉ β ( βπ
'''πΉ) = (
βπ βπΉ)) |
32 | 30, 31 | syl 17 |
. . . . . . 7
β’ ((π β§ πΉ βπ π₯) β (
βπ '''πΉ) = ( βπ
βπΉ)) |
33 | | df-fv 6509 |
. . . . . . . 8
β’ (
βπ βπΉ) = (β©π€πΉ βπ π€) |
34 | 15 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πΉ βπ π₯ β§ πΉ βπ π€)) β πΉ:π΄βΆβ) |
35 | 18 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πΉ βπ π₯ β§ πΉ βπ π€)) β sup(π΄, β*, < ) =
+β) |
36 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πΉ βπ π₯ β§ πΉ βπ π€)) β πΉ βπ π€) |
37 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πΉ βπ π₯ β§ πΉ βπ π€)) β πΉ βπ π₯) |
38 | 34, 35, 36, 37 | rlimuni 15439 |
. . . . . . . . . . . . 13
β’ ((π β§ (πΉ βπ π₯ β§ πΉ βπ π€)) β π€ = π₯) |
39 | 38 | expr 458 |
. . . . . . . . . . . 12
β’ ((π β§ πΉ βπ π₯) β (πΉ βπ π€ β π€ = π₯)) |
40 | | breq2 5114 |
. . . . . . . . . . . . 13
β’ (π€ = π₯ β (πΉ βπ π€ β πΉ βπ π₯)) |
41 | 3, 40 | syl5ibrcom 247 |
. . . . . . . . . . . 12
β’ ((π β§ πΉ βπ π₯) β (π€ = π₯ β πΉ βπ π€)) |
42 | 39, 41 | impbid 211 |
. . . . . . . . . . 11
β’ ((π β§ πΉ βπ π₯) β (πΉ βπ π€ β π€ = π₯)) |
43 | 42 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ πΉ βπ π₯) β§ π₯ β V) β (πΉ βπ π€ β π€ = π₯)) |
44 | 43 | iota5 6484 |
. . . . . . . . 9
β’ (((π β§ πΉ βπ π₯) β§ π₯ β V) β (β©π€πΉ βπ π€) = π₯) |
45 | 44 | elvd 3455 |
. . . . . . . 8
β’ ((π β§ πΉ βπ π₯) β (β©π€πΉ βπ π€) = π₯) |
46 | 33, 45 | eqtrid 2789 |
. . . . . . 7
β’ ((π β§ πΉ βπ π₯) β (
βπ βπΉ) = π₯) |
47 | 32, 46 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ πΉ βπ π₯) β (
βπ '''πΉ) = π₯) |
48 | 3, 47 | breqtrrd 5138 |
. . . . 5
β’ ((π β§ πΉ βπ π₯) β πΉ βπ (
βπ '''πΉ)) |
49 | 48 | ex 414 |
. . . 4
β’ (π β (πΉ βπ π₯ β πΉ βπ (
βπ '''πΉ))) |
50 | 49 | exlimdv 1937 |
. . 3
β’ (π β (βπ₯ πΉ βπ π₯ β πΉ βπ (
βπ '''πΉ))) |
51 | 2, 50 | syl5 34 |
. 2
β’ (π β (πΉ β dom βπ
β πΉ
βπ ( βπ '''πΉ))) |
52 | 4 | releldmi 5908 |
. 2
β’ (πΉ βπ (
βπ '''πΉ) β πΉ β dom βπ
) |
53 | 51, 52 | impbid1 224 |
1
β’ (π β (πΉ β dom βπ
β πΉ
βπ ( βπ '''πΉ))) |