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

Metamath Proof Explorer

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→ 𝐵