Theorem f1orescnv

Description: The converse of a one-to-one-onto restricted function. (Contributed by Paul Chapman, 21-Apr-2008)

	Ref	Expression
Assertion	f1orescnv	⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 ) → ( ◡ 𝐹 ↾ 𝑃 ) : 𝑃 –1-1-onto→ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		f1ocnv	⊢ ( ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 → ◡ ( 𝐹 ↾ 𝑅 ) : 𝑃 –1-1-onto→ 𝑅 )
2	1	adantl	⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 ) → ◡ ( 𝐹 ↾ 𝑅 ) : 𝑃 –1-1-onto→ 𝑅 )
3		funcnvres	⊢ ( Fun ◡ 𝐹 → ◡ ( 𝐹 ↾ 𝑅 ) = ( ◡ 𝐹 ↾ ( 𝐹 “ 𝑅 ) ) )
4		df-ima	⊢ ( 𝐹 “ 𝑅 ) = ran ( 𝐹 ↾ 𝑅 )
5		dff1o5	⊢ ( ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 ↔ ( ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1→ 𝑃 ∧ ran ( 𝐹 ↾ 𝑅 ) = 𝑃 ) )
6	5	simprbi	⊢ ( ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 → ran ( 𝐹 ↾ 𝑅 ) = 𝑃 )
7	4 6	syl5eq	⊢ ( ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 → ( 𝐹 “ 𝑅 ) = 𝑃 )
8	7	reseq2d	⊢ ( ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 → ( ◡ 𝐹 ↾ ( 𝐹 “ 𝑅 ) ) = ( ◡ 𝐹 ↾ 𝑃 ) )
9	3 8	sylan9eq	⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 ) → ◡ ( 𝐹 ↾ 𝑅 ) = ( ◡ 𝐹 ↾ 𝑃 ) )
10		f1oeq1	⊢ ( ◡ ( 𝐹 ↾ 𝑅 ) = ( ◡ 𝐹 ↾ 𝑃 ) → ( ◡ ( 𝐹 ↾ 𝑅 ) : 𝑃 –1-1-onto→ 𝑅 ↔ ( ◡ 𝐹 ↾ 𝑃 ) : 𝑃 –1-1-onto→ 𝑅 ) )
11	9 10	syl	⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 ) → ( ◡ ( 𝐹 ↾ 𝑅 ) : 𝑃 –1-1-onto→ 𝑅 ↔ ( ◡ 𝐹 ↾ 𝑃 ) : 𝑃 –1-1-onto→ 𝑅 ) )
12	2 11	mpbid	⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 ) → ( ◡ 𝐹 ↾ 𝑃 ) : 𝑃 –1-1-onto→ 𝑅 )