Metamath Proof Explorer

Theorem f1imadifssran

Description: Condition for the range of a one-to-one function to be the range of one its restrictions. Variant of imadifssran . (Contributed by AV, 4-Oct-2025)

Ref Expression
Assertion f1imadifssran ( Fun ◡ 𝐹 → ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 imadmrn ⊢ ( 𝐹 “ dom 𝐹 ) = ran 𝐹
2 imadif ⊢ ( Fun ◡ 𝐹 → ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) = ( ( 𝐹 “ dom 𝐹 ) ∖ ( 𝐹 “ 𝐴 ) ) )
3 2 sseq1d ⊢ ( Fun ◡ 𝐹 → ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ( 𝐹 “ 𝐴 ) ↔ ( ( 𝐹 “ dom 𝐹 ) ∖ ( 𝐹 “ 𝐴 ) ) ⊆ ( 𝐹 “ 𝐴 ) ) )
4 ssundif ⊢ ( ( 𝐹 “ dom 𝐹 ) ⊆ ( ( 𝐹 “ 𝐴 ) ∪ ( 𝐹 “ 𝐴 ) ) ↔ ( ( 𝐹 “ dom 𝐹 ) ∖ ( 𝐹 “ 𝐴 ) ) ⊆ ( 𝐹 “ 𝐴 ) )
5 unidm ⊢ ( ( 𝐹 “ 𝐴 ) ∪ ( 𝐹 “ 𝐴 ) ) = ( 𝐹 “ 𝐴 )
6 5 sseq2i ⊢ ( ( 𝐹 “ dom 𝐹 ) ⊆ ( ( 𝐹 “ 𝐴 ) ∪ ( 𝐹 “ 𝐴 ) ) ↔ ( 𝐹 “ dom 𝐹 ) ⊆ ( 𝐹 “ 𝐴 ) )
7 id ⊢ ( ( 𝐹 “ dom 𝐹 ) ⊆ ( 𝐹 “ 𝐴 ) → ( 𝐹 “ dom 𝐹 ) ⊆ ( 𝐹 “ 𝐴 ) )
8 imassrn ⊢ ( 𝐹 “ 𝐴 ) ⊆ ran 𝐹
9 8 1 sseqtrri ⊢ ( 𝐹 “ 𝐴 ) ⊆ ( 𝐹 “ dom 𝐹 )
10 9 a1i ⊢ ( ( 𝐹 “ dom 𝐹 ) ⊆ ( 𝐹 “ 𝐴 ) → ( 𝐹 “ 𝐴 ) ⊆ ( 𝐹 “ dom 𝐹 ) )
11 7 10 eqssd ⊢ ( ( 𝐹 “ dom 𝐹 ) ⊆ ( 𝐹 “ 𝐴 ) → ( 𝐹 “ dom 𝐹 ) = ( 𝐹 “ 𝐴 ) )
12 6 11 sylbi ⊢ ( ( 𝐹 “ dom 𝐹 ) ⊆ ( ( 𝐹 “ 𝐴 ) ∪ ( 𝐹 “ 𝐴 ) ) → ( 𝐹 “ dom 𝐹 ) = ( 𝐹 “ 𝐴 ) )
13 4 12 sylbir ⊢ ( ( ( 𝐹 “ dom 𝐹 ) ∖ ( 𝐹 “ 𝐴 ) ) ⊆ ( 𝐹 “ 𝐴 ) → ( 𝐹 “ dom 𝐹 ) = ( 𝐹 “ 𝐴 ) )
14 3 13 biimtrdi ⊢ ( Fun ◡ 𝐹 → ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ( 𝐹 “ 𝐴 ) → ( 𝐹 “ dom 𝐹 ) = ( 𝐹 “ 𝐴 ) ) )
15 14 imp ⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ( 𝐹 “ 𝐴 ) ) → ( 𝐹 “ dom 𝐹 ) = ( 𝐹 “ 𝐴 ) )
16 1 15 eqtr3id ⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ( 𝐹 “ 𝐴 ) ) → ran 𝐹 = ( 𝐹 “ 𝐴 ) )
17 16 ex ⊢ ( Fun ◡ 𝐹 → ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ( 𝐹 “ 𝐴 ) → ran 𝐹 = ( 𝐹 “ 𝐴 ) ) )
18 df-ima ⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
19 18 eqcomi ⊢ ran ( 𝐹 ↾ 𝐴 ) = ( 𝐹 “ 𝐴 )
20 19 sseq2i ⊢ ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) ↔ ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ( 𝐹 “ 𝐴 ) )
21 19 eqeq2i ⊢ ( ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) ↔ ran 𝐹 = ( 𝐹 “ 𝐴 ) )
22 17 20 21 3imtr4g ⊢ ( Fun ◡ 𝐹 → ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) ) )