Step | Hyp | Ref
| Expression |
1 | | evthicc.1 |
. . . 4
β’ (π β π΄ β β) |
2 | | evthicc.2 |
. . . 4
β’ (π β π΅ β β) |
3 | | evthicc.3 |
. . . 4
β’ (π β π΄ β€ π΅) |
4 | | evthicc.4 |
. . . 4
β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) |
5 | 1, 2, 3, 4 | evthicc 24846 |
. . 3
β’ (π β (βπ β (π΄[,]π΅)βπ§ β (π΄[,]π΅)(πΉβπ§) β€ (πΉβπ) β§ βπ β (π΄[,]π΅)βπ§ β (π΄[,]π΅)(πΉβπ) β€ (πΉβπ§))) |
6 | | reeanv 3216 |
. . 3
β’
(βπ β
(π΄[,]π΅)βπ β (π΄[,]π΅)(βπ§ β (π΄[,]π΅)(πΉβπ§) β€ (πΉβπ) β§ βπ§ β (π΄[,]π΅)(πΉβπ) β€ (πΉβπ§)) β (βπ β (π΄[,]π΅)βπ§ β (π΄[,]π΅)(πΉβπ§) β€ (πΉβπ) β§ βπ β (π΄[,]π΅)βπ§ β (π΄[,]π΅)(πΉβπ) β€ (πΉβπ§))) |
7 | 5, 6 | sylibr 233 |
. 2
β’ (π β βπ β (π΄[,]π΅)βπ β (π΄[,]π΅)(βπ§ β (π΄[,]π΅)(πΉβπ§) β€ (πΉβπ) β§ βπ§ β (π΄[,]π΅)(πΉβπ) β€ (πΉβπ§))) |
8 | | r19.26 3111 |
. . . 4
β’
(βπ§ β
(π΄[,]π΅)((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§)) β (βπ§ β (π΄[,]π΅)(πΉβπ§) β€ (πΉβπ) β§ βπ§ β (π΄[,]π΅)(πΉβπ) β€ (πΉβπ§))) |
9 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β πΉ β ((π΄[,]π΅)βcnββ)) |
10 | | cncff 24279 |
. . . . . . . . 9
β’ (πΉ β ((π΄[,]π΅)βcnββ) β πΉ:(π΄[,]π΅)βΆβ) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β πΉ:(π΄[,]π΅)βΆβ) |
12 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β π β (π΄[,]π΅)) |
13 | 11, 12 | ffvelcdmd 7040 |
. . . . . . 7
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β (πΉβπ) β β) |
14 | 13 | adantr 482 |
. . . . . 6
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ βπ§ β (π΄[,]π΅)((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§))) β (πΉβπ) β β) |
15 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β π β (π΄[,]π΅)) |
16 | 11, 15 | ffvelcdmd 7040 |
. . . . . . 7
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β (πΉβπ) β β) |
17 | 16 | adantr 482 |
. . . . . 6
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ βπ§ β (π΄[,]π΅)((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§))) β (πΉβπ) β β) |
18 | 11 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ βπ§ β (π΄[,]π΅)((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§))) β πΉ:(π΄[,]π΅)βΆβ) |
19 | 18 | ffnd 6673 |
. . . . . . . . 9
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ βπ§ β (π΄[,]π΅)((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§))) β πΉ Fn (π΄[,]π΅)) |
20 | 16 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ π§ β (π΄[,]π΅)) β (πΉβπ) β β) |
21 | | elicc2 13338 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β ((πΉβπ§) β ((πΉβπ)[,](πΉβπ)) β ((πΉβπ§) β β β§ (πΉβπ) β€ (πΉβπ§) β§ (πΉβπ§) β€ (πΉβπ)))) |
22 | 13, 20, 21 | syl2an2r 684 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ π§ β (π΄[,]π΅)) β ((πΉβπ§) β ((πΉβπ)[,](πΉβπ)) β ((πΉβπ§) β β β§ (πΉβπ) β€ (πΉβπ§) β§ (πΉβπ§) β€ (πΉβπ)))) |
23 | | 3anass 1096 |
. . . . . . . . . . . . 13
β’ (((πΉβπ§) β β β§ (πΉβπ) β€ (πΉβπ§) β§ (πΉβπ§) β€ (πΉβπ)) β ((πΉβπ§) β β β§ ((πΉβπ) β€ (πΉβπ§) β§ (πΉβπ§) β€ (πΉβπ)))) |
24 | 22, 23 | bitrdi 287 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ π§ β (π΄[,]π΅)) β ((πΉβπ§) β ((πΉβπ)[,](πΉβπ)) β ((πΉβπ§) β β β§ ((πΉβπ) β€ (πΉβπ§) β§ (πΉβπ§) β€ (πΉβπ))))) |
25 | | ancom 462 |
. . . . . . . . . . . . 13
β’ (((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§)) β ((πΉβπ) β€ (πΉβπ§) β§ (πΉβπ§) β€ (πΉβπ))) |
26 | 11 | ffvelcdmda 7039 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ π§ β (π΄[,]π΅)) β (πΉβπ§) β β) |
27 | 26 | biantrurd 534 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ π§ β (π΄[,]π΅)) β (((πΉβπ) β€ (πΉβπ§) β§ (πΉβπ§) β€ (πΉβπ)) β ((πΉβπ§) β β β§ ((πΉβπ) β€ (πΉβπ§) β§ (πΉβπ§) β€ (πΉβπ))))) |
28 | 25, 27 | bitrid 283 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ π§ β (π΄[,]π΅)) β (((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§)) β ((πΉβπ§) β β β§ ((πΉβπ) β€ (πΉβπ§) β§ (πΉβπ§) β€ (πΉβπ))))) |
29 | 24, 28 | bitr4d 282 |
. . . . . . . . . . 11
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ π§ β (π΄[,]π΅)) β ((πΉβπ§) β ((πΉβπ)[,](πΉβπ)) β ((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§)))) |
30 | 29 | ralbidva 3169 |
. . . . . . . . . 10
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β (βπ§ β (π΄[,]π΅)(πΉβπ§) β ((πΉβπ)[,](πΉβπ)) β βπ§ β (π΄[,]π΅)((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§)))) |
31 | 30 | biimpar 479 |
. . . . . . . . 9
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ βπ§ β (π΄[,]π΅)((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§))) β βπ§ β (π΄[,]π΅)(πΉβπ§) β ((πΉβπ)[,](πΉβπ))) |
32 | | ffnfv 7070 |
. . . . . . . . 9
β’ (πΉ:(π΄[,]π΅)βΆ((πΉβπ)[,](πΉβπ)) β (πΉ Fn (π΄[,]π΅) β§ βπ§ β (π΄[,]π΅)(πΉβπ§) β ((πΉβπ)[,](πΉβπ)))) |
33 | 19, 31, 32 | sylanbrc 584 |
. . . . . . . 8
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ βπ§ β (π΄[,]π΅)((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§))) β πΉ:(π΄[,]π΅)βΆ((πΉβπ)[,](πΉβπ))) |
34 | 33 | frnd 6680 |
. . . . . . 7
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ βπ§ β (π΄[,]π΅)((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§))) β ran πΉ β ((πΉβπ)[,](πΉβπ))) |
35 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β π΄ β β) |
36 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β π΅ β β) |
37 | | ssidd 3971 |
. . . . . . . . 9
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β (π΄[,]π΅) β (π΄[,]π΅)) |
38 | | ax-resscn 11116 |
. . . . . . . . . . 11
β’ β
β β |
39 | | ssid 3970 |
. . . . . . . . . . 11
β’ β
β β |
40 | | cncfss 24285 |
. . . . . . . . . . 11
β’ ((β
β β β§ β β β) β ((π΄[,]π΅)βcnββ) β ((π΄[,]π΅)βcnββ)) |
41 | 38, 39, 40 | mp2an 691 |
. . . . . . . . . 10
β’ ((π΄[,]π΅)βcnββ) β ((π΄[,]π΅)βcnββ) |
42 | 41, 9 | sselid 3946 |
. . . . . . . . 9
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β πΉ β ((π΄[,]π΅)βcnββ)) |
43 | 11 | ffvelcdmda 7039 |
. . . . . . . . 9
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ π₯ β (π΄[,]π΅)) β (πΉβπ₯) β β) |
44 | 35, 36, 12, 15, 37, 42, 43 | ivthicc 24845 |
. . . . . . . 8
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β ((πΉβπ)[,](πΉβπ)) β ran πΉ) |
45 | 44 | adantr 482 |
. . . . . . 7
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ βπ§ β (π΄[,]π΅)((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§))) β ((πΉβπ)[,](πΉβπ)) β ran πΉ) |
46 | 34, 45 | eqssd 3965 |
. . . . . 6
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ βπ§ β (π΄[,]π΅)((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§))) β ran πΉ = ((πΉβπ)[,](πΉβπ))) |
47 | | rspceov 7408 |
. . . . . 6
β’ (((πΉβπ) β β β§ (πΉβπ) β β β§ ran πΉ = ((πΉβπ)[,](πΉβπ))) β βπ₯ β β βπ¦ β β ran πΉ = (π₯[,]π¦)) |
48 | 14, 17, 46, 47 | syl3anc 1372 |
. . . . 5
β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ βπ§ β (π΄[,]π΅)((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§))) β βπ₯ β β βπ¦ β β ran πΉ = (π₯[,]π¦)) |
49 | 48 | ex 414 |
. . . 4
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β (βπ§ β (π΄[,]π΅)((πΉβπ§) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ§)) β βπ₯ β β βπ¦ β β ran πΉ = (π₯[,]π¦))) |
50 | 8, 49 | biimtrrid 242 |
. . 3
β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β ((βπ§ β (π΄[,]π΅)(πΉβπ§) β€ (πΉβπ) β§ βπ§ β (π΄[,]π΅)(πΉβπ) β€ (πΉβπ§)) β βπ₯ β β βπ¦ β β ran πΉ = (π₯[,]π¦))) |
51 | 50 | rexlimdvva 3202 |
. 2
β’ (π β (βπ β (π΄[,]π΅)βπ β (π΄[,]π΅)(βπ§ β (π΄[,]π΅)(πΉβπ§) β€ (πΉβπ) β§ βπ§ β (π΄[,]π΅)(πΉβπ) β€ (πΉβπ§)) β βπ₯ β β βπ¦ β β ran πΉ = (π₯[,]π¦))) |
52 | 7, 51 | mpd 15 |
1
β’ (π β βπ₯ β β βπ¦ β β ran πΉ = (π₯[,]π¦)) |