Step | Hyp | Ref
| Expression |
1 | | neik0pk1imk0.k1 |
. . . 4
β’ (π β βπ₯ β π΅ βπ β π« π΅βπ‘ β π« π΅((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯))) |
2 | | neik0pk1imk0.bex |
. . . . . . 7
β’ (π β π΅ β π) |
3 | | pwidg 4623 |
. . . . . . 7
β’ (π΅ β π β π΅ β π« π΅) |
4 | | sseq2 4009 |
. . . . . . . . . 10
β’ (π‘ = π΅ β (π β π‘ β π β π΅)) |
5 | 4 | anbi2d 628 |
. . . . . . . . 9
β’ (π‘ = π΅ β ((π β (πβπ₯) β§ π β π‘) β (π β (πβπ₯) β§ π β π΅))) |
6 | | eleq1 2820 |
. . . . . . . . 9
β’ (π‘ = π΅ β (π‘ β (πβπ₯) β π΅ β (πβπ₯))) |
7 | 5, 6 | imbi12d 343 |
. . . . . . . 8
β’ (π‘ = π΅ β (((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)) β ((π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯)))) |
8 | 7 | rspcv 3609 |
. . . . . . 7
β’ (π΅ β π« π΅ β (βπ‘ β π« π΅((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)) β ((π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯)))) |
9 | 2, 3, 8 | 3syl 18 |
. . . . . 6
β’ (π β (βπ‘ β π« π΅((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)) β ((π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯)))) |
10 | 9 | ralimdv 3168 |
. . . . 5
β’ (π β (βπ β π« π΅βπ‘ β π« π΅((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)) β βπ β π« π΅((π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯)))) |
11 | 10 | ralimdv 3168 |
. . . 4
β’ (π β (βπ₯ β π΅ βπ β π« π΅βπ‘ β π« π΅((π β (πβπ₯) β§ π β π‘) β π‘ β (πβπ₯)) β βπ₯ β π΅ βπ β π« π΅((π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯)))) |
12 | 1, 11 | mpd 15 |
. . 3
β’ (π β βπ₯ β π΅ βπ β π« π΅((π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯))) |
13 | | r19.23v 3181 |
. . . . . 6
β’
(βπ β
π« π΅((π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯)) β (βπ β π« π΅(π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯))) |
14 | 13 | biimpi 215 |
. . . . 5
β’
(βπ β
π« π΅((π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯)) β (βπ β π« π΅(π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯))) |
15 | 14 | a1i 11 |
. . . 4
β’ (π β (βπ β π« π΅((π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯)) β (βπ β π« π΅(π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯)))) |
16 | 15 | ralimdv 3168 |
. . 3
β’ (π β (βπ₯ β π΅ βπ β π« π΅((π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯)) β βπ₯ β π΅ (βπ β π« π΅(π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯)))) |
17 | 12, 16 | mpd 15 |
. 2
β’ (π β βπ₯ β π΅ (βπ β π« π΅(π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯))) |
18 | | neik0pk1imk0.k0p |
. . 3
β’ (π β βπ₯ β π΅ (πβπ₯) β β
) |
19 | | neik0pk1imk0.n |
. . . . . . . . . . . . . 14
β’ (π β π β (π« π« π΅ βm π΅)) |
20 | | elmapi 8846 |
. . . . . . . . . . . . . 14
β’ (π β (π« π«
π΅ βm π΅) β π:π΅βΆπ« π« π΅) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π:π΅βΆπ« π« π΅) |
22 | 21 | ffvelcdmda 7087 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΅) β (πβπ₯) β π« π« π΅) |
23 | 22 | elpwid 4612 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΅) β (πβπ₯) β π« π΅) |
24 | 23 | sseld 3982 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β (π β (πβπ₯) β π β π« π΅)) |
25 | 24 | ancrd 551 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β (π β (πβπ₯) β (π β π« π΅ β§ π β (πβπ₯)))) |
26 | 25 | eximdv 1919 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β (βπ π β (πβπ₯) β βπ (π β π« π΅ β§ π β (πβπ₯)))) |
27 | | n0 4347 |
. . . . . . . 8
β’ ((πβπ₯) β β
β βπ π β (πβπ₯)) |
28 | | df-rex 3070 |
. . . . . . . 8
β’
(βπ β
π« π΅π β (πβπ₯) β βπ (π β π« π΅ β§ π β (πβπ₯))) |
29 | 26, 27, 28 | 3imtr4g 295 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β ((πβπ₯) β β
β βπ β π« π΅π β (πβπ₯))) |
30 | 29 | imp 406 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (πβπ₯) β β
) β βπ β π« π΅π β (πβπ₯)) |
31 | | elpwi 4610 |
. . . . . . . . 9
β’ (π β π« π΅ β π β π΅) |
32 | 24, 31 | syl6 35 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β (π β (πβπ₯) β π β π΅)) |
33 | 32 | ralrimivw 3149 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β βπ β π« π΅(π β (πβπ₯) β π β π΅)) |
34 | 33 | adantr 480 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (πβπ₯) β β
) β βπ β π« π΅(π β (πβπ₯) β π β π΅)) |
35 | 30, 34 | r19.29imd 3117 |
. . . . 5
β’ (((π β§ π₯ β π΅) β§ (πβπ₯) β β
) β βπ β π« π΅(π β (πβπ₯) β§ π β π΅)) |
36 | 35 | ex 412 |
. . . 4
β’ ((π β§ π₯ β π΅) β ((πβπ₯) β β
β βπ β π« π΅(π β (πβπ₯) β§ π β π΅))) |
37 | 36 | ralimdva 3166 |
. . 3
β’ (π β (βπ₯ β π΅ (πβπ₯) β β
β βπ₯ β π΅ βπ β π« π΅(π β (πβπ₯) β§ π β π΅))) |
38 | 18, 37 | mpd 15 |
. 2
β’ (π β βπ₯ β π΅ βπ β π« π΅(π β (πβπ₯) β§ π β π΅)) |
39 | | ralim 3085 |
. 2
β’
(βπ₯ β
π΅ (βπ β π« π΅(π β (πβπ₯) β§ π β π΅) β π΅ β (πβπ₯)) β (βπ₯ β π΅ βπ β π« π΅(π β (πβπ₯) β§ π β π΅) β βπ₯ β π΅ π΅ β (πβπ₯))) |
40 | 17, 38, 39 | sylc 65 |
1
β’ (π β βπ₯ β π΅ π΅ β (πβπ₯)) |