![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dff1o5 | Structured version Visualization version GIF version |
Description: Alternate definition of one-to-one onto function. (Contributed by NM, 10-Dec-2003.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Ref | Expression |
---|---|
dff1o5 | ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f1o 5933 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) | |
2 | f1f 6139 | . . . . 5 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) | |
3 | 2 | biantrurd 528 | . . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → (ran 𝐹 = 𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))) |
4 | dffo2 6157 | . . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)) | |
5 | 3, 4 | syl6rbbr 279 | . . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹:𝐴–onto→𝐵 ↔ ran 𝐹 = 𝐵)) |
6 | 5 | pm5.32i 670 | . 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵)) |
7 | 1, 6 | bitri 264 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 = wceq 1523 ran crn 5144 ⟶wf 5922 –1-1→wf1 5923 –onto→wfo 5924 –1-1-onto→wf1o 5925 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-in 3614 df-ss 3621 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 |
This theorem is referenced by: f1orescnv 6190 domdifsn 8084 sucdom2 8197 ackbij1 9098 ackbij2 9103 fin4en1 9169 om2uzf1oi 12792 s4f1o 13709 fvcosymgeq 17895 indlcim 20227 2lgslem1b 25162 ausgrusgrb 26105 usgrexmpledg 26199 cdleme50f1o 36151 diaf1oN 36736 pwssplit4 37976 meadjiunlem 41000 |
Copyright terms: Public domain | W3C validator |