![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fn0 | Structured version Visualization version GIF version |
Description: A function with empty domain is empty. (Contributed by NM, 15-Apr-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Ref | Expression |
---|---|
fn0 | ⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnrel 6602 | . . 3 ⊢ (𝐹 Fn ∅ → Rel 𝐹) | |
2 | fndm 6603 | . . 3 ⊢ (𝐹 Fn ∅ → dom 𝐹 = ∅) | |
3 | reldm0 5882 | . . . 4 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) | |
4 | 3 | biimpar 478 | . . 3 ⊢ ((Rel 𝐹 ∧ dom 𝐹 = ∅) → 𝐹 = ∅) |
5 | 1, 2, 4 | syl2anc 584 | . 2 ⊢ (𝐹 Fn ∅ → 𝐹 = ∅) |
6 | fun0 6564 | . . . 4 ⊢ Fun ∅ | |
7 | dm0 5875 | . . . 4 ⊢ dom ∅ = ∅ | |
8 | df-fn 6497 | . . . 4 ⊢ (∅ Fn ∅ ↔ (Fun ∅ ∧ dom ∅ = ∅)) | |
9 | 6, 7, 8 | mpbir2an 709 | . . 3 ⊢ ∅ Fn ∅ |
10 | fneq1 6591 | . . 3 ⊢ (𝐹 = ∅ → (𝐹 Fn ∅ ↔ ∅ Fn ∅)) | |
11 | 9, 10 | mpbiri 257 | . 2 ⊢ (𝐹 = ∅ → 𝐹 Fn ∅) |
12 | 5, 11 | impbii 208 | 1 ⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1541 ∅c0 4281 dom cdm 5632 Rel wrel 5637 Fun wfun 6488 Fn wfn 6489 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-sep 5255 ax-nul 5262 ax-pr 5383 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-mo 2538 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-sn 4586 df-pr 4588 df-op 4592 df-br 5105 df-opab 5167 df-id 5530 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-fun 6496 df-fn 6497 |
This theorem is referenced by: mpt0 6641 f0 6721 f00 6722 f0bi 6723 f1o00 6817 fo00 6818 tpos0 8184 ixp0x 8861 0fz1 13458 hashf1 14353 fuchom 17846 fuchomOLD 17847 grpinvfvi 18790 mulgfval 18870 mulgfvalALT 18871 mulgfvi 18874 0frgp 19557 invrfval 20098 psrvscafval 21354 tmdgsum 23442 deg1fvi 25446 hon0 30633 fnchoice 43214 dvnprodlem3 44159 |
Copyright terms: Public domain | W3C validator |