![]() |
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 6331 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) | |
2 | dffo2 6569 | . . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)) | |
3 | f1f 6549 | . . . . 5 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) | |
4 | 3 | biantrurd 536 | . . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → (ran 𝐹 = 𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))) |
5 | 2, 4 | bitr4id 293 | . . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹:𝐴–onto→𝐵 ↔ ran 𝐹 = 𝐵)) |
6 | 5 | pm5.32i 578 | . 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵)) |
7 | 1, 6 | bitri 278 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 = wceq 1538 ran crn 5520 ⟶wf 6320 –1-1→wf1 6321 –onto→wfo 6322 –1-1-onto→wf1o 6323 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-in 3888 df-ss 3898 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 |
This theorem is referenced by: f1orescnv 6605 domdifsn 8583 sucdom2 8610 ackbij1 9649 ackbij2 9654 fin4en1 9720 om2uzf1oi 13316 s4f1o 14271 fvcosymgeq 18549 indlcim 20529 2lgslem1b 25976 ausgrusgrb 26958 usgrexmpledg 27052 cdleme50f1o 37842 diaf1oN 38426 pwssplit4 40033 meadjiunlem 43104 |
Copyright terms: Public domain | W3C validator |