dff1o4 - Metamath Proof Explorer

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

Theorem dff1o4 6452

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
dff1o4	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ^◡𝐹 Fn 𝐵))

**Proof of Theorem dff1o4**
Step	Hyp	Ref	Expression
1		dff1o2 6449	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵))
2		3anass 1076	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵)))
3		df-rn 5418	. . . . . 6 ⊢ ran 𝐹 = dom ^◡𝐹
4	3	eqeq1i 2784	. . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ^◡𝐹 = 𝐵)
5	4	anbi2i 613	. . . 4 ⊢ ((Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ^◡𝐹 ∧ dom ^◡𝐹 = 𝐵))
6		df-fn 6191	. . . 4 ⊢ (^◡𝐹 Fn 𝐵 ↔ (Fun ^◡𝐹 ∧ dom ^◡𝐹 = 𝐵))
7	5, 6	bitr4i 270	. . 3 ⊢ ((Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ^◡𝐹 Fn 𝐵)
8	7	anbi2i 613	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ (Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ ^◡𝐹 Fn 𝐵))
9	1, 2, 8	3bitri 289	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ^◡𝐹 Fn 𝐵))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ^◡ccnv 5406 dom cdm 5407 ran crn 5408 Fun wfun 6182 Fn wfn 6183 –1-1-onto→wf1o 6187

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2751

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2760 df-cleq 2772 df-clel 2847 df-in 3837 df-ss 3844 df-rn 5418 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195

This theorem is referenced by: f1ocnv 6456 f1oun 6463 f1o00 6478 f1oi 6481 f1osn 6483 f1oprswap 6487 f1ompt 6698 f1ofveu 6971 f1ocnvd 7214 curry1 7607 curry2 7610 mapsnf1o2 8256 omxpenlem 8414 sbthlem9 8431 compssiso 9594 mptfzshft 14993 fprodrev 15191 invf1o 16897 mhmf1o 17813 grpinvf1o 17956 ghmf1o 18159 rhmf1o 19207 srngf1o 19347 lmhmf1o 19540 hmeof1o2 22075 axcontlem2 26454 f1o3d 30136 padct 30207 f1od2 30209 cdleme51finvN 37134 fsovf1od 39722 isomushgr 43357 mgmhmf1o 43420 rnghmf1o 43536