Step | Hyp | Ref
| Expression |
1 | | nlfnval 30872 |
. . . . . 6
β’ (π: ββΆβ β
(nullβπ) = (β‘π β {0})) |
2 | | cnvimass 6037 |
. . . . . 6
β’ (β‘π β {0}) β dom π |
3 | 1, 2 | eqsstrdi 4002 |
. . . . 5
β’ (π: ββΆβ β
(nullβπ) β dom
π) |
4 | | fdm 6681 |
. . . . 5
β’ (π: ββΆβ β
dom π =
β) |
5 | 3, 4 | sseqtrd 3988 |
. . . 4
β’ (π: ββΆβ β
(nullβπ) β
β) |
6 | 5 | sseld 3947 |
. . 3
β’ (π: ββΆβ β
(π΄ β (nullβπ) β π΄ β β)) |
7 | 6 | pm4.71rd 564 |
. 2
β’ (π: ββΆβ β
(π΄ β (nullβπ) β (π΄ β β β§ π΄ β (nullβπ)))) |
8 | 1 | eleq2d 2820 |
. . . . 5
β’ (π: ββΆβ β
(π΄ β (nullβπ) β π΄ β (β‘π β {0}))) |
9 | 8 | adantr 482 |
. . . 4
β’ ((π: ββΆβ β§
π΄ β β) β
(π΄ β (nullβπ) β π΄ β (β‘π β {0}))) |
10 | | ffn 6672 |
. . . . 5
β’ (π: ββΆβ β
π Fn
β) |
11 | | eleq1 2822 |
. . . . . . . 8
β’ (π₯ = π΄ β (π₯ β (β‘π β {0}) β π΄ β (β‘π β {0}))) |
12 | | fveqeq2 6855 |
. . . . . . . 8
β’ (π₯ = π΄ β ((πβπ₯) = 0 β (πβπ΄) = 0)) |
13 | 11, 12 | bibi12d 346 |
. . . . . . 7
β’ (π₯ = π΄ β ((π₯ β (β‘π β {0}) β (πβπ₯) = 0) β (π΄ β (β‘π β {0}) β (πβπ΄) = 0))) |
14 | 13 | imbi2d 341 |
. . . . . 6
β’ (π₯ = π΄ β ((π Fn β β (π₯ β (β‘π β {0}) β (πβπ₯) = 0)) β (π Fn β β (π΄ β (β‘π β {0}) β (πβπ΄) = 0)))) |
15 | | 0cn 11155 |
. . . . . . . . 9
β’ 0 β
β |
16 | | vex 3451 |
. . . . . . . . . 10
β’ π₯ β V |
17 | 16 | eliniseg 6050 |
. . . . . . . . 9
β’ (0 β
β β (π₯ β
(β‘π β {0}) β π₯π0)) |
18 | 15, 17 | ax-mp 5 |
. . . . . . . 8
β’ (π₯ β (β‘π β {0}) β π₯π0) |
19 | | fnbrfvb 6899 |
. . . . . . . 8
β’ ((π Fn β β§ π₯ β β) β ((πβπ₯) = 0 β π₯π0)) |
20 | 18, 19 | bitr4id 290 |
. . . . . . 7
β’ ((π Fn β β§ π₯ β β) β (π₯ β (β‘π β {0}) β (πβπ₯) = 0)) |
21 | 20 | expcom 415 |
. . . . . 6
β’ (π₯ β β β (π Fn β β (π₯ β (β‘π β {0}) β (πβπ₯) = 0))) |
22 | 14, 21 | vtoclga 3536 |
. . . . 5
β’ (π΄ β β β (π Fn β β (π΄ β (β‘π β {0}) β (πβπ΄) = 0))) |
23 | 10, 22 | mpan9 508 |
. . . 4
β’ ((π: ββΆβ β§
π΄ β β) β
(π΄ β (β‘π β {0}) β (πβπ΄) = 0)) |
24 | 9, 23 | bitrd 279 |
. . 3
β’ ((π: ββΆβ β§
π΄ β β) β
(π΄ β (nullβπ) β (πβπ΄) = 0)) |
25 | 24 | pm5.32da 580 |
. 2
β’ (π: ββΆβ β
((π΄ β β β§
π΄ β (nullβπ)) β (π΄ β β β§ (πβπ΄) = 0))) |
26 | 7, 25 | bitrd 279 |
1
β’ (π: ββΆβ β
(π΄ β (nullβπ) β (π΄ β β β§ (πβπ΄) = 0))) |