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 6625

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 6622	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵))
2		3anass 1091	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵)))
3		df-rn 5568	. . . . . 6 ⊢ ran 𝐹 = dom ^◡𝐹
4	3	eqeq1i 2828	. . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ^◡𝐹 = 𝐵)
5	4	anbi2i 624	. . . 4 ⊢ ((Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ^◡𝐹 ∧ dom ^◡𝐹 = 𝐵))
6		df-fn 6360	. . . 4 ⊢ (^◡𝐹 Fn 𝐵 ↔ (Fun ^◡𝐹 ∧ dom ^◡𝐹 = 𝐵))
7	5, 6	bitr4i 280	. . 3 ⊢ ((Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ^◡𝐹 Fn 𝐵)
8	7	anbi2i 624	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ (Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ ^◡𝐹 Fn 𝐵))
9	1, 2, 8	3bitri 299	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ^◡𝐹 Fn 𝐵))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ^◡ccnv 5556 dom cdm 5557 ran crn 5558 Fun wfun 6351 Fn wfn 6352 –1-1-onto→wf1o 6356

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-in 3945 df-ss 3954 df-rn 5568 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364

This theorem is referenced by: f1ocnv 6629 f1oun 6636 f1o00 6651 f1oi 6654 f1osn 6656 f1oprswap 6660 f1ompt 6877 f1ofveu 7153 f1ocnvd 7398 curry1 7801 curry2 7804 mapsnf1o2 8460 omxpenlem 8620 sbthlem9 8637 compssiso 9798 mptfzshft 15135 fprodrev 15333 invf1o 17041 mhmf1o 17968 grpinvf1o 18171 ghmf1o 18390 rhmf1o 19486 srngf1o 19627 lmhmf1o 19820 hmeof1o2 22373 axcontlem2 26753 f1o3d 30374 padct 30457 f1od2 30459 cdleme51finvN 37694 fsovf1od 40369 isomushgr 43998 mgmhmf1o 44061 rnghmf1o 44181