This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1ocnv

Description: The converse of a one-to-one onto function is also one-to-one onto. (Contributed by NM, 11-Feb-1997) (Proof shortened by Andrew Salmon, 22-Oct-2011)

		Ref	Expression
	Assertion	f1ocnv	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ^◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fnrel	⊢ ( 𝐹 Fn 𝐴 → Rel 𝐹 )
2		dfrel2	⊢ ( Rel 𝐹 ↔ ^◡ ^◡ 𝐹 = 𝐹 )
3		fneq1	⊢ ( ^◡ ^◡ 𝐹 = 𝐹 → ( ^◡ ^◡ 𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴 ) )
4	3	biimprd	⊢ ( ^◡ ^◡ 𝐹 = 𝐹 → ( 𝐹 Fn 𝐴 → ^◡ ^◡ 𝐹 Fn 𝐴 ) )
5	2 4	sylbi	⊢ ( Rel 𝐹 → ( 𝐹 Fn 𝐴 → ^◡ ^◡ 𝐹 Fn 𝐴 ) )
6	1 5	mpcom	⊢ ( 𝐹 Fn 𝐴 → ^◡ ^◡ 𝐹 Fn 𝐴 )
7	6	anim1ci	⊢ ( ( 𝐹 Fn 𝐴 ∧ ^◡ 𝐹 Fn 𝐵 ) → ( ^◡ 𝐹 Fn 𝐵 ∧ ^◡ ^◡ 𝐹 Fn 𝐴 ) )
8		dff1o4	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ^◡ 𝐹 Fn 𝐵 ) )
9		dff1o4	⊢ ( ^◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 ↔ ( ^◡ 𝐹 Fn 𝐵 ∧ ^◡ ^◡ 𝐹 Fn 𝐴 ) )
10	7 8 9	3imtr4i	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ^◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )