Metamath Proof Explorer

Theorem imadifssranOLD

Description: Obsolete version of imadifssrn as of 29-Sep-2026. (Contributed by AV, 4-Oct-2025) Remove antecedent. (Revised by Eric Schmidt, 10-Jul-2026) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion imadifssranOLD ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 df-ima ⊢ ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) = ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) )
2 1 sseq1i ⊢ ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) ↔ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) )
3 ssun2 ⊢ dom 𝐹 ⊆ ( 𝐴 ∪ dom 𝐹 )
4 undif2 ⊢ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) = ( 𝐴 ∪ dom 𝐹 )
5 3 4 sseqtrri ⊢ dom 𝐹 ⊆ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) )
6 ssres2 ⊢ ( dom 𝐹 ⊆ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) → ( 𝐹 ↾ dom 𝐹 ) ⊆ ( 𝐹 ↾ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) ) )
7 5 6 ax-mp ⊢ ( 𝐹 ↾ dom 𝐹 ) ⊆ ( 𝐹 ↾ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) )
8 resundi ⊢ ( 𝐹 ↾ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) ) = ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) )
9 7 8 sseqtri ⊢ ( 𝐹 ↾ dom 𝐹 ) ⊆ ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) )
10 9 rnssi ⊢ ran ( 𝐹 ↾ dom 𝐹 ) ⊆ ran ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) )
11 rnun ⊢ ran ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) = ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) )
12 10 11 sseqtri ⊢ ran ( 𝐹 ↾ dom 𝐹 ) ⊆ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) )
13 12 sseli ⊢ ( 𝑦 ∈ ran ( 𝐹 ↾ dom 𝐹 ) → 𝑦 ∈ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) )
14 elun ⊢ ( 𝑦 ∈ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) ↔ ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) )
15 13 14 sylib ⊢ ( 𝑦 ∈ ran ( 𝐹 ↾ dom 𝐹 ) → ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) )
16 inv1 ⊢ ( dom 𝐹 ∩ V ) = dom 𝐹
17 16 ineqcomi ⊢ ( V ∩ dom 𝐹 ) = dom 𝐹
18 17 reseq2i ⊢ ( 𝐹 ↾ ( V ∩ dom 𝐹 ) ) = ( 𝐹 ↾ dom 𝐹 )
19 resindm ⊢ ( 𝐹 ↾ ( V ∩ dom 𝐹 ) ) = ( 𝐹 ↾ V )
20 18 19 eqtr3i ⊢ ( 𝐹 ↾ dom 𝐹 ) = ( 𝐹 ↾ V )
21 20 rneqi ⊢ ran ( 𝐹 ↾ dom 𝐹 ) = ran ( 𝐹 ↾ V )
22 rnresv ⊢ ran ( 𝐹 ↾ V ) = ran 𝐹
23 21 22 eqtr2i ⊢ ran 𝐹 = ran ( 𝐹 ↾ dom 𝐹 )
24 15 23 eleq2s ⊢ ( 𝑦 ∈ ran 𝐹 → ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) )
25 ssel ⊢ ( ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
26 pm2.27 ⊢ ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → ( ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
27 26 jao1i ⊢ ( ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) → ( ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
28 24 25 27 syl2imc ⊢ ( ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ( 𝑦 ∈ ran 𝐹 → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
29 28 ssrdv ⊢ ( ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 ⊆ ran ( 𝐹 ↾ 𝐴 ) )
30 rnresss ⊢ ran ( 𝐹 ↾ 𝐴 ) ⊆ ran 𝐹
31 30 a1i ⊢ ( ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran ( 𝐹 ↾ 𝐴 ) ⊆ ran 𝐹 )
32 29 31 eqssd ⊢ ( ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) )
33 2 32 sylbi ⊢ ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) )