focnvimacdmdm

Description: The preimage of the codomain of a surjection is its domain. (Contributed by AV, 29-Sep-2024)

		Ref	Expression
	Assertion	focnvimacdmdm	$⊢ G : A \underset{onto}{⟶} B \to G^{-1} [B] = A$

Step	Hyp	Ref	Expression
1		forn	$⊢ G : A \underset{onto}{⟶} B \to ran G = B$
2	1	eqcomd	$⊢ G : A \underset{onto}{⟶} B \to B = ran G$
3	2	imaeq2d	$⊢ G : A \underset{onto}{⟶} B \to G^{-1} [B] = G^{-1} [ran G]$
4		cnvimarndm	$⊢ G^{-1} [ran G] = dom G$
5	3 4	eqtrdi	$⊢ G : A \underset{onto}{⟶} B \to G^{-1} [B] = dom G$
6		fof	$⊢ G : A \underset{onto}{⟶} B \to G : A ⟶ B$
7	6	fdmd	$⊢ G : A \underset{onto}{⟶} B \to dom G = A$
8	5 7	eqtrd	$⊢ G : A \underset{onto}{⟶} B \to G^{-1} [B] = A$

Metamath Proof Explorer