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 6731

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 1096	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ^◡𝐹))
2		dff1o2 6730	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6443	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 624	. 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 396 ∧ w3a 1086 = wceq 1539 ^◡ccnv 5589 ran crn 5591 Fun wfun 6431 Fn wfn 6432 –onto→wfo 6435 –1-1-onto→wf1o 6436

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 2710

This theorem depends on definitions: df-bi 206 df-an 397 df-3an 1088 df-tru 1542 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-v 3435 df-in 3895 df-ss 3905 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444

This theorem is referenced by: f1ofo 6732 resdif 6746 f1opw 7534 f11o 7798 1stconst 7949 2ndconst 7950 curry1 7953 curry2 7956 f1o2ndf1 7972 ssdomg 8795 dif1enlem 8952 phplem2 9000 php3 9004 phplem4OLD 9012 php3OLD 9016 f1opwfi 9132 cantnfp1lem3 9447 fpwwe2lem5 10400 canthp1lem2 10418 odf1o2 19187 dprdf1o 19644 relogf1o 25731 iseupthf1o 28575 padct 31063 ballotlemfrc 32502 poimirlem1 35787 poimirlem2 35788 poimirlem3 35789 poimirlem4 35790 poimirlem6 35792 poimirlem7 35793 poimirlem9 35795 poimirlem11 35797 poimirlem12 35798 poimirlem13 35799 poimirlem14 35800 poimirlem16 35802 poimirlem17 35803 poimirlem19 35805 poimirlem20 35806 poimirlem23 35809 poimirlem24 35810 poimirlem25 35811 poimirlem29 35815 poimirlem31 35817 ntrneifv2 41697