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 6058

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 6055	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵))
2		3anass 1035	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵)))
3		df-rn 5049	. . . . . 6 ⊢ ran 𝐹 = dom ^◡𝐹
4	3	eqeq1i 2615	. . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ^◡𝐹 = 𝐵)
5	4	anbi2i 726	. . . 4 ⊢ ((Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ^◡𝐹 ∧ dom ^◡𝐹 = 𝐵))
6		df-fn 5807	. . . 4 ⊢ (^◡𝐹 Fn 𝐵 ↔ (Fun ^◡𝐹 ∧ dom ^◡𝐹 = 𝐵))
7	5, 6	bitr4i 266	. . 3 ⊢ ((Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ^◡𝐹 Fn 𝐵)
8	7	anbi2i 726	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ (Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ ^◡𝐹 Fn 𝐵))
9	1, 2, 8	3bitri 285	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ^◡𝐹 Fn 𝐵))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ^◡ccnv 5037 dom cdm 5038 ran crn 5039 Fun wfun 5798 Fn wfn 5799 –1-1-onto→wf1o 5803

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-in 3547 df-ss 3554 df-rn 5049 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811

This theorem is referenced by: f1ocnv 6062 f1oun 6069 f1o00 6083 f1oi 6086 f1osn 6088 f1oprswap 6092 f1ompt 6290 f1ofveu 6544 f1ocnvd 6782 curry1 7156 curry2 7159 mapsnf1o2 7791 omxpenlem 7946 sbthlem9 7963 compssiso 9079 mptfzshft 14352 fsumrev 14353 fprodrev 14546 invf1o 16252 mhmf1o 17168 grpinvf1o 17308 ghmf1o 17513 rhmf1o 18555 srngf1o 18677 lmhmf1o 18867 hmeof1o2 21376 axcontlem2 25645 f1o3d 28813 padct 28885 f1od2 28887 cdleme51finvN 34862 fsovf1od 37330 mgmhmf1o 41577 rnghmf1o 41693