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 6842

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 6839	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵))
2		3anass 1093	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵)))
3		df-rn 5684	. . . . . 6 ⊢ ran 𝐹 = dom ^◡𝐹
4	3	eqeq1i 2733	. . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ^◡𝐹 = 𝐵)
5	4	anbi2i 622	. . . 4 ⊢ ((Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ^◡𝐹 ∧ dom ^◡𝐹 = 𝐵))
6		df-fn 6546	. . . 4 ⊢ (^◡𝐹 Fn 𝐵 ↔ (Fun ^◡𝐹 ∧ dom ^◡𝐹 = 𝐵))
7	5, 6	bitr4i 278	. . 3 ⊢ ((Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ^◡𝐹 Fn 𝐵)
8	7	anbi2i 622	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ (Fun ^◡𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ ^◡𝐹 Fn 𝐵))
9	1, 2, 8	3bitri 297	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ^◡𝐹 Fn 𝐵))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1534 ^◡ccnv 5672 dom cdm 5673 ran crn 5674 Fun wfun 6537 Fn wfn 6538 –1-1-onto→wf1o 6542

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699

This theorem depends on definitions: df-bi 206 df-an 396 df-3an 1087 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3472 df-in 3952 df-ss 3962 df-rn 5684 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550

This theorem is referenced by: f1ocnv 6846 f1oun 6853 f1o00 6869 f1oi 6872 f1osn 6874 f1oprswap 6878 f1ompt 7116 f1ofveu 7409 f1ocnvd 7667 curry1 8104 curry2 8107 mapsnf1o2 8907 omxpenlem 9092 sbthlem9 9110 compssiso 10392 mptfzshft 15751 invf1o 17746 mgmhmf1o 18654 mhmf1o 18747 grpinvf1o 18959 ghmf1o 19196 rnghmf1o 20385 rhmf1o 20424 srngf1o 20728 lmhmf1o 20925 hmeof1o2 23661 axcontlem2 28770 f1o3d 32406 padct 32496 f1od2 32498 cdleme51finvN 40024 fsovf1od 43437 gricushgr 47174

	
		OSZAR »