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 6836

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 1097	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ^◡𝐹))
2		dff1o2 6835	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6546	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 624	. 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ^◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ^◡𝐹))
5	1, 2, 4	3bitr4i 302	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ^◡𝐹))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ^◡ccnv 5674 ran crn 5676 Fun wfun 6534 Fn wfn 6535 –onto→wfo 6538 –1-1-onto→wf1o 6539

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 2703

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 2710 df-cleq 2724 df-clel 2810 df-v 3476 df-in 3954 df-ss 3964 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547

This theorem is referenced by: f1ofo 6837 resdif 6851 f1opw 7658 f11o 7929 1stconst 8082 2ndconst 8083 curry1 8086 curry2 8089 f1o2ndf1 8104 ssdomg 8992 dif1enlem 9152 dif1enlemOLD 9153 phplem2 9204 php3 9208 phplem4OLD 9216 php3OLD 9220 f1opwfi 9352 cantnfp1lem3 9671 fpwwe2lem5 10626 canthp1lem2 10644 odf1o2 19435 dprdf1o 19896 relogf1o 26066 iseupthf1o 29444 padct 31931 ballotlemfrc 33513 poimirlem1 36477 poimirlem2 36478 poimirlem3 36479 poimirlem4 36480 poimirlem6 36482 poimirlem7 36483 poimirlem9 36485 poimirlem11 36487 poimirlem12 36488 poimirlem13 36489 poimirlem14 36490 poimirlem16 36492 poimirlem17 36493 poimirlem19 36495 poimirlem20 36496 poimirlem23 36499 poimirlem24 36500 poimirlem25 36501 poimirlem29 36505 poimirlem31 36507 ntrneifv2 42816