![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dff1o4 | Structured version Visualization version GIF version |
Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Ref | Expression |
---|---|
dff1o4 | ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dff1o2 6825 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) | |
2 | 3anass 1095 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))) | |
3 | df-rn 5680 | . . . . . 6 ⊢ ran 𝐹 = dom ◡𝐹 | |
4 | 3 | eqeq1i 2736 | . . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ◡𝐹 = 𝐵) |
5 | 4 | anbi2i 623 | . . . 4 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵)) |
6 | df-fn 6535 | . . . 4 ⊢ (◡𝐹 Fn 𝐵 ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵)) | |
7 | 5, 6 | bitr4i 277 | . . 3 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ◡𝐹 Fn 𝐵) |
8 | 7 | anbi2i 623 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵)) |
9 | 1, 2, 8 | 3bitri 296 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ◡ccnv 5668 dom cdm 5669 ran crn 5670 Fun wfun 6526 Fn wfn 6527 –1-1-onto→wf1o 6531 |
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 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-3an 1089 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-in 3951 df-ss 3961 df-rn 5680 df-fn 6535 df-f 6536 df-f1 6537 df-fo 6538 df-f1o 6539 |
This theorem is referenced by: f1ocnv 6832 f1oun 6839 f1o00 6855 f1oi 6858 f1osn 6860 f1oprswap 6864 f1ompt 7095 f1ofveu 7387 f1ocnvd 7640 curry1 8072 curry2 8075 mapsnf1o2 8871 omxpenlem 9056 sbthlem9 9074 compssiso 10351 mptfzshft 15706 invf1o 17698 mhmf1o 18658 grpinvf1o 18867 ghmf1o 19088 rhmf1o 20219 srngf1o 20411 lmhmf1o 20606 hmeof1o2 23196 axcontlem2 28088 f1o3d 31719 padct 31815 f1od2 31817 cdleme51finvN 39232 fsovf1od 42538 isomushgr 46266 mgmhmf1o 46329 rnghmf1o 46449 |
Copyright terms: Public domain | W3C validator |