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 6840

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 1098	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ^◡𝐹))
2		dff1o2 6839	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6550	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 625	. 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 397 ∧ w3a 1088 = wceq 1542 ^◡ccnv 5676 ran crn 5678 Fun wfun 6538 Fn wfn 6539 –onto→wfo 6542 –1-1-onto→wf1o 6543

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704

This theorem depends on definitions: df-bi 206 df-an 398 df-3an 1090 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3956 df-ss 3966 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551

This theorem is referenced by: f1ofo 6841 resdif 6855 f1opw 7662 f11o 7933 1stconst 8086 2ndconst 8087 curry1 8090 curry2 8093 f1o2ndf1 8108 ssdomg 8996 dif1enlem 9156 dif1enlemOLD 9157 phplem2 9208 php3 9212 phplem4OLD 9220 php3OLD 9224 f1opwfi 9356 cantnfp1lem3 9675 fpwwe2lem5 10630 canthp1lem2 10648 odf1o2 19441 dprdf1o 19902 relogf1o 26075 iseupthf1o 29486 padct 31975 ballotlemfrc 33556 poimirlem1 36537 poimirlem2 36538 poimirlem3 36539 poimirlem4 36540 poimirlem6 36542 poimirlem7 36543 poimirlem9 36545 poimirlem11 36547 poimirlem12 36548 poimirlem13 36549 poimirlem14 36550 poimirlem16 36552 poimirlem17 36553 poimirlem19 36555 poimirlem20 36556 poimirlem23 36559 poimirlem24 36560 poimirlem25 36561 poimirlem29 36565 poimirlem31 36567 ntrneifv2 42879