dff1o3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dff1o3		Structured version Visualization version GIF version

Theorem dff1o3 6830

Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

**Assertion**
Ref	Expression
dff1o3	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ^◡𝐹))

**Proof of Theorem dff1o3**
Step	Hyp	Ref	Expression
1		3anan32 1094	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ^◡𝐹))
2		dff1o2 6829	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6540	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 623	. 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ^◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ^◡𝐹))
5	1, 2, 4	3bitr4i 303	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ^◡𝐹))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∧ wa 395 ∧ w3a 1084 = wceq 1533 ^◡ccnv 5666 ran crn 5668 Fun wfun 6528 Fn wfn 6529 –onto→wfo 6532 –1-1-onto→wf1o 6533

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695

This theorem depends on definitions: df-bi 206 df-an 396 df-3an 1086 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-v 3468 df-in 3948 df-ss 3958 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541

This theorem is referenced by: f1ofo 6831 resdif 6845 f1opw 7656 f11o 7927 1stconst 8081 2ndconst 8082 curry1 8085 curry2 8088 f1o2ndf1 8103 ssdomg 8993 dif1enlem 9153 dif1enlemOLD 9154 phplem2 9205 php3 9209 phplem4OLD 9217 php3OLD 9221 f1opwfi 9353 cantnfp1lem3 9672 fpwwe2lem5 10627 canthp1lem2 10645 odf1o2 19485 dprdf1o 19946 relogf1o 26419 iseupthf1o 29927 padct 32416 ballotlemfrc 34017 poimirlem1 36983 poimirlem2 36984 poimirlem3 36985 poimirlem4 36986 poimirlem6 36988 poimirlem7 36989 poimirlem9 36991 poimirlem11 36993 poimirlem12 36994 poimirlem13 36995 poimirlem14 36996 poimirlem16 36998 poimirlem17 36999 poimirlem19 37001 poimirlem20 37002 poimirlem23 37005 poimirlem24 37006 poimirlem25 37007 poimirlem29 37011 poimirlem31 37013 ntrneifv2 43345