| 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 6568 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) | |
| 2 | dffo2 6824 | . . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)) | |
| 3 | f1f 6804 | . . . . 5 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) | |
| 4 | 3 | biantrurd 532 | . . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → (ran 𝐹 = 𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))) |
| 5 | 2, 4 | bitr4id 290 | . . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹:𝐴–onto→𝐵 ↔ ran 𝐹 = 𝐵)) |
| 6 | 5 | pm5.32i 574 | . 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵)) |
| 7 | 1, 6 | bitri 275 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1540 ran crn 5686 ⟶wf 6557 –1-1→wf1 6558 –onto→wfo 6559 –1-1-onto→wf1o 6560 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ss 3968 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 |
| This theorem is referenced by: f1orescnv 6863 f1ounsn 7292 domdifsn 9094 sucdom2OLD 9122 sucdom2 9243 ackbij1 10277 ackbij2 10282 fin4en1 10349 om2uzf1oi 13994 s4f1o 14957 fvcosymgeq 19447 indlcim 21860 2lgslem1b 27436 ausgrusgrb 29182 usgrexmpledg 29279 wrdpmtrlast 33113 cdleme50f1o 40548 diaf1oN 41132 aks6d1c2 42131 pwssplit4 43101 cantnf2 43338 meadjiunlem 46480 |
| Copyright terms: Public domain | W3C validator |