Theorem rinvf1o

Description: Sufficient conditions for the restriction of an involution to be a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016)

	Ref	Expression
Hypotheses	rinvbij.1	⊢ Fun 𝐹
	rinvbij.2	⊢ ◡ 𝐹 = 𝐹
	rinvbij.3a	⊢ ( 𝐹 “ 𝐴 ) ⊆ 𝐵
	rinvbij.3b	⊢ ( 𝐹 “ 𝐵 ) ⊆ 𝐴
	rinvbij.4a	⊢ 𝐴 ⊆ dom 𝐹
	rinvbij.4b	⊢ 𝐵 ⊆ dom 𝐹
Assertion	rinvf1o	⊢ ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐵

Proof

Step	Hyp	Ref	Expression
1		rinvbij.1	⊢ Fun 𝐹
2		rinvbij.2	⊢ ◡ 𝐹 = 𝐹
3		rinvbij.3a	⊢ ( 𝐹 “ 𝐴 ) ⊆ 𝐵
4		rinvbij.3b	⊢ ( 𝐹 “ 𝐵 ) ⊆ 𝐴
5		rinvbij.4a	⊢ 𝐴 ⊆ dom 𝐹
6		rinvbij.4b	⊢ 𝐵 ⊆ dom 𝐹
7		fdmrn	⊢ ( Fun 𝐹 ↔ 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
8	1 7	mpbi	⊢ 𝐹 : dom 𝐹 ⟶ ran 𝐹
9	2	funeqi	⊢ ( Fun ◡ 𝐹 ↔ Fun 𝐹 )
10	1 9	mpbir	⊢ Fun ◡ 𝐹
11		df-f1	⊢ ( 𝐹 : dom 𝐹 –1-1→ ran 𝐹 ↔ ( 𝐹 : dom 𝐹 ⟶ ran 𝐹 ∧ Fun ◡ 𝐹 ) )
12	8 10 11	mpbir2an	⊢ 𝐹 : dom 𝐹 –1-1→ ran 𝐹
13		f1ores	⊢ ( ( 𝐹 : dom 𝐹 –1-1→ ran 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 ) )
14	12 5 13	mp2an	⊢ ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 )
15		funimass3	⊢ ( ( Fun 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐵 ) ⊆ 𝐴 ↔ 𝐵 ⊆ ( ◡ 𝐹 “ 𝐴 ) ) )
16	1 6 15	mp2an	⊢ ( ( 𝐹 “ 𝐵 ) ⊆ 𝐴 ↔ 𝐵 ⊆ ( ◡ 𝐹 “ 𝐴 ) )
17	4 16	mpbi	⊢ 𝐵 ⊆ ( ◡ 𝐹 “ 𝐴 )
18	2	imaeq1i	⊢ ( ◡ 𝐹 “ 𝐴 ) = ( 𝐹 “ 𝐴 )
19	17 18	sseqtri	⊢ 𝐵 ⊆ ( 𝐹 “ 𝐴 )
20	3 19	eqssi	⊢ ( 𝐹 “ 𝐴 ) = 𝐵
21		f1oeq3	⊢ ( ( 𝐹 “ 𝐴 ) = 𝐵 → ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 ) ↔ ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐵 ) )
22	20 21	ax-mp	⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 ) ↔ ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐵 )
23	14 22	mpbi	⊢ ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐵