funfocofob

Description: If the domain of a function G is a subset of the range of a function F , then the composition ( G o. F ) is surjective iff G is surjective. (Contributed by GL and AV, 29-Sep-2024)

		Ref	Expression
	Assertion	funfocofob	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to ((G \circ F) : F^{-1} [A] \underset{onto}{⟶} B \leftrightarrow G : A \underset{onto}{⟶} B)$

Proof

Step	Hyp	Ref	Expression
1		fdmrn	$⊢ Fun F \leftrightarrow F : dom F ⟶ ran F$
2	1	biimpi	$⊢ Fun F \to F : dom F ⟶ ran F$
3	2	3ad2ant1	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to F : dom F ⟶ ran F$
4	3	adantr	$⊢ ((Fun F \land G : A ⟶ B \land A \subseteq ran F) \land (G \circ F) : F^{-1} [A] \underset{onto}{⟶} B) \to F : dom F ⟶ ran F$
5		eqid	$⊢ ran F \cap A = ran F \cap A$
6		eqid	$⊢ F^{-1} [A] = F^{-1} [A]$
7		eqid	$⊢ {F ↾}_{F^{-1} [A]} = {F ↾}_{F^{-1} [A]}$
8		simp2	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to G : A ⟶ B$
9	8	adantr	$⊢ ((Fun F \land G : A ⟶ B \land A \subseteq ran F) \land (G \circ F) : F^{-1} [A] \underset{onto}{⟶} B) \to G : A ⟶ B$
10		eqid	$⊢ {G ↾}_{(ran F \cap A)} = {G ↾}_{(ran F \cap A)}$
11		simpr	$⊢ ((Fun F \land G : A ⟶ B \land A \subseteq ran F) \land (G \circ F) : F^{-1} [A] \underset{onto}{⟶} B) \to (G \circ F) : F^{-1} [A] \underset{onto}{⟶} B$
12	4 5 6 7 9 10 11	fcoresfo	$⊢ ((Fun F \land G : A ⟶ B \land A \subseteq ran F) \land (G \circ F) : F^{-1} [A] \underset{onto}{⟶} B) \to ({G ↾}_{(ran F \cap A)}) : ran F \cap A \underset{onto}{⟶} B$
13	12	ex	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to ((G \circ F) : F^{-1} [A] \underset{onto}{⟶} B \to ({G ↾}_{(ran F \cap A)}) : ran F \cap A \underset{onto}{⟶} B)$
14		sseqin2	$⊢ A \subseteq ran F \leftrightarrow ran F \cap A = A$
15	14	biimpi	$⊢ A \subseteq ran F \to ran F \cap A = A$
16	15	3ad2ant3	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to ran F \cap A = A$
17	8	fdmd	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to dom G = A$
18	16 17	eqtr4d	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to ran F \cap A = dom G$
19	18	reseq2d	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to {G ↾}_{(ran F \cap A)} = {G ↾}_{dom G}$
20	8	freld	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to Rel G$
21		resdm	$⊢ Rel G \to {G ↾}_{dom G} = G$
22	20 21	syl	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to {G ↾}_{dom G} = G$
23	19 22	eqtrd	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to {G ↾}_{(ran F \cap A)} = G$
24		eqidd	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to B = B$
25	23 16 24	foeq123d	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to (({G ↾}_{(ran F \cap A)}) : ran F \cap A \underset{onto}{⟶} B \leftrightarrow G : A \underset{onto}{⟶} B)$
26	13 25	sylibd	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to ((G \circ F) : F^{-1} [A] \underset{onto}{⟶} B \to G : A \underset{onto}{⟶} B)$
27		simpr	$⊢ ((Fun F \land G : A ⟶ B \land A \subseteq ran F) \land G : A \underset{onto}{⟶} B) \to G : A \underset{onto}{⟶} B$
28		simpl1	$⊢ ((Fun F \land G : A ⟶ B \land A \subseteq ran F) \land G : A \underset{onto}{⟶} B) \to Fun F$
29		simpl3	$⊢ ((Fun F \land G : A ⟶ B \land A \subseteq ran F) \land G : A \underset{onto}{⟶} B) \to A \subseteq ran F$
30		focofo	$⊢ (G : A \underset{onto}{⟶} B \land Fun F \land A \subseteq ran F) \to (G \circ F) : F^{-1} [A] \underset{onto}{⟶} B$
31	27 28 29 30	syl3anc	$⊢ ((Fun F \land G : A ⟶ B \land A \subseteq ran F) \land G : A \underset{onto}{⟶} B) \to (G \circ F) : F^{-1} [A] \underset{onto}{⟶} B$
32	31	ex	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to (G : A \underset{onto}{⟶} B \to (G \circ F) : F^{-1} [A] \underset{onto}{⟶} B)$
33	26 32	impbid	$⊢ (Fun F \land G : A ⟶ B \land A \subseteq ran F) \to ((G \circ F) : F^{-1} [A] \underset{onto}{⟶} B \leftrightarrow G : A \underset{onto}{⟶} B)$

Metamath Proof Explorer

Theorem funfocofob

Proof