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 6829

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 6828	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6542	. . 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 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ^◡ccnv 5658 ran crn 5660 Fun wfun 6530 Fn wfn 6531 –onto→wfo 6534 –1-1-onto→wf1o 6535

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 2008 ax-9 2119 ax-ext 2708

This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1088 df-ex 1780 df-cleq 2728 df-ss 3948 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543

This theorem is referenced by: f1ofo 6830 resdif 6844 f1opw 7668 f11o 7950 1stconst 8104 2ndconst 8105 curry1 8108 curry2 8111 f1o2ndf1 8126 ssdomg 9019 dif1enlem 9175 dif1enlemOLD 9176 phplem2 9224 php3 9228 php3OLD 9238 f1opwfi 9373 cantnfp1lem3 9699 fpwwe2lem5 10654 canthp1lem2 10672 odf1o2 19559 dprdf1o 20020 relogf1o 26532 iseupthf1o 30188 padct 32702 ballotlemfrc 34564 poimirlem1 37650 poimirlem2 37651 poimirlem3 37652 poimirlem4 37653 poimirlem6 37655 poimirlem7 37656 poimirlem9 37658 poimirlem11 37660 poimirlem12 37661 poimirlem13 37662 poimirlem14 37663 poimirlem16 37665 poimirlem17 37666 poimirlem19 37668 poimirlem20 37669 poimirlem23 37672 poimirlem24 37673 poimirlem25 37674 poimirlem29 37678 poimirlem31 37680 ntrneifv2 44071 permaxpow 45001 upgrimpthslem1 47887 upgrimspths 47890 idfth 49065 idsubc 49066