Step | Hyp | Ref
| Expression |
1 | | allbutfifvre.5 |
. . . 4
β’ (π β π β π·) |
2 | | allbutfifvre.4 |
. . . 4
β’ π· = βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
3 | 1, 2 | eleqtrdi 2844 |
. . 3
β’ (π β π β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ)) |
4 | | allbutfifvre.2 |
. . . 4
β’ π =
(β€β₯βπ) |
5 | | eqid 2733 |
. . . 4
β’ βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) = βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
6 | 4, 5 | allbutfi 44103 |
. . 3
β’ (π β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β βπ β π βπ β (β€β₯βπ)π β dom (πΉβπ)) |
7 | 3, 6 | sylib 217 |
. 2
β’ (π β βπ β π βπ β (β€β₯βπ)π β dom (πΉβπ)) |
8 | | allbutfifvre.1 |
. . . . 5
β’
β²ππ |
9 | | nfv 1918 |
. . . . 5
β’
β²π π β π |
10 | 8, 9 | nfan 1903 |
. . . 4
β’
β²π(π β§ π β π) |
11 | | simpll 766 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π) |
12 | 4 | uztrn2 12841 |
. . . . . . . 8
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
13 | 12 | ssd 43769 |
. . . . . . 7
β’ (π β π β (β€β₯βπ) β π) |
14 | 13 | sselda 3983 |
. . . . . 6
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
15 | 14 | adantll 713 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
16 | | allbutfifvre.3 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
17 | 16 | ffvelcdmda 7087 |
. . . . . 6
β’ (((π β§ π β π) β§ π β dom (πΉβπ)) β ((πΉβπ)βπ) β β) |
18 | 17 | ex 414 |
. . . . 5
β’ ((π β§ π β π) β (π β dom (πΉβπ) β ((πΉβπ)βπ) β β)) |
19 | 11, 15, 18 | syl2anc 585 |
. . . 4
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (π β dom (πΉβπ) β ((πΉβπ)βπ) β β)) |
20 | 10, 19 | ralimdaa 3258 |
. . 3
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)π β dom (πΉβπ) β βπ β (β€β₯βπ)((πΉβπ)βπ) β β)) |
21 | 20 | reximdva 3169 |
. 2
β’ (π β (βπ β π βπ β (β€β₯βπ)π β dom (πΉβπ) β βπ β π βπ β (β€β₯βπ)((πΉβπ)βπ) β β)) |
22 | 7, 21 | mpd 15 |
1
β’ (π β βπ β π βπ β (β€β₯βπ)((πΉβπ)βπ) β β) |