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 6477 | . . 3 ⊢ (𝐹 Fn ∅ → Rel 𝐹) | |
2 | fndm 6478 | . . 3 ⊢ (𝐹 Fn ∅ → dom 𝐹 = ∅) | |
3 | reldm0 5794 | . . . 4 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) | |
4 | 3 | biimpar 481 | . . 3 ⊢ ((Rel 𝐹 ∧ dom 𝐹 = ∅) → 𝐹 = ∅) |
5 | 1, 2, 4 | syl2anc 587 | . 2 ⊢ (𝐹 Fn ∅ → 𝐹 = ∅) |
6 | fun0 6442 | . . . 4 ⊢ Fun ∅ | |
7 | dm0 5786 | . . . 4 ⊢ dom ∅ = ∅ | |
8 | df-fn 6380 | . . . 4 ⊢ (∅ Fn ∅ ↔ (Fun ∅ ∧ dom ∅ = ∅)) | |
9 | 6, 7, 8 | mpbir2an 711 | . . 3 ⊢ ∅ Fn ∅ |
10 | fneq1 6467 | . . 3 ⊢ (𝐹 = ∅ → (𝐹 Fn ∅ ↔ ∅ Fn ∅)) | |
11 | 9, 10 | mpbiri 261 | . 2 ⊢ (𝐹 = ∅ → 𝐹 Fn ∅) |
12 | 5, 11 | impbii 212 | 1 ⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1543 ∅c0 4234 dom cdm 5548 Rel wrel 5553 Fun wfun 6371 Fn wfn 6372 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5189 ax-nul 5196 ax-pr 5319 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ral 3063 df-rex 3064 df-rab 3067 df-v 3407 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-nul 4235 df-if 4437 df-sn 4539 df-pr 4541 df-op 4545 df-br 5051 df-opab 5113 df-id 5452 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-fun 6379 df-fn 6380 |
This theorem is referenced by: mpt0 6517 f0 6597 f00 6598 f0bi 6599 f1o00 6692 fo00 6693 tpos0 7995 ixp0x 8604 0fz1 13129 hashf1 14020 fuchom 17466 fuchomOLD 17467 grpinvfvi 18407 mulgfval 18487 mulgfvalALT 18488 mulgfvi 18491 0frgp 19166 invrfval 19688 psrvscafval 20912 tmdgsum 22989 deg1fvi 24980 hon0 29871 fnchoice 42243 dvnprodlem3 43162 |
Copyright terms: Public domain | W3C validator |