Theorem cnvimassrndm

Description: The preimage of a superset of the range of a class is the domain of the class. Generalization of cnvimarndm for subsets. (Contributed by AV, 18-Sep-2024)

	Ref	Expression
Assertion	cnvimassrndm	⊢ ( ran 𝐹 ⊆ 𝐴 → ( ◡ 𝐹 “ 𝐴 ) = dom 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		ssequn1	⊢ ( ran 𝐹 ⊆ 𝐴 ↔ ( ran 𝐹 ∪ 𝐴 ) = 𝐴 )
2		imaeq2	⊢ ( 𝐴 = ( ran 𝐹 ∪ 𝐴 ) → ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ ( ran 𝐹 ∪ 𝐴 ) ) )
3		imaundi	⊢ ( ◡ 𝐹 “ ( ran 𝐹 ∪ 𝐴 ) ) = ( ( ◡ 𝐹 “ ran 𝐹 ) ∪ ( ◡ 𝐹 “ 𝐴 ) )
4	2 3	eqtrdi	⊢ ( 𝐴 = ( ran 𝐹 ∪ 𝐴 ) → ( ◡ 𝐹 “ 𝐴 ) = ( ( ◡ 𝐹 “ ran 𝐹 ) ∪ ( ◡ 𝐹 “ 𝐴 ) ) )
5		cnvimarndm	⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
6	5	uneq1i	⊢ ( ( ◡ 𝐹 “ ran 𝐹 ) ∪ ( ◡ 𝐹 “ 𝐴 ) ) = ( dom 𝐹 ∪ ( ◡ 𝐹 “ 𝐴 ) )
7		cnvimass	⊢ ( ◡ 𝐹 “ 𝐴 ) ⊆ dom 𝐹
8		ssequn2	⊢ ( ( ◡ 𝐹 “ 𝐴 ) ⊆ dom 𝐹 ↔ ( dom 𝐹 ∪ ( ◡ 𝐹 “ 𝐴 ) ) = dom 𝐹 )
9	7 8	mpbi	⊢ ( dom 𝐹 ∪ ( ◡ 𝐹 “ 𝐴 ) ) = dom 𝐹
10	6 9	eqtri	⊢ ( ( ◡ 𝐹 “ ran 𝐹 ) ∪ ( ◡ 𝐹 “ 𝐴 ) ) = dom 𝐹
11	4 10	eqtrdi	⊢ ( 𝐴 = ( ran 𝐹 ∪ 𝐴 ) → ( ◡ 𝐹 “ 𝐴 ) = dom 𝐹 )
12	11	eqcoms	⊢ ( ( ran 𝐹 ∪ 𝐴 ) = 𝐴 → ( ◡ 𝐹 “ 𝐴 ) = dom 𝐹 )
13	1 12	sylbi	⊢ ( ran 𝐹 ⊆ 𝐴 → ( ◡ 𝐹 “ 𝐴 ) = dom 𝐹 )