This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1ocof1ob

Description: If the range of F equals the domain of G , then the composition ( G o. F ) is bijective iff F and G are both bijective. (Contributed by GL and AV, 7-Oct-2024)

		Ref	Expression
	Assertion	f1ocof1ob	\|- ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -1-1-onto-> D <-> ( F : A -1-1-> C /\ G : C -1-1-onto-> D ) ) )

Proof

Step	Hyp	Ref	Expression
1		ffrn	\|- ( F : A --> B -> F : A --> ran F )
2	1	3ad2ant1	\|- ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> F : A --> ran F )
3		feq3	\|- ( ran F = C -> ( F : A --> ran F <-> F : A --> C ) )
4	3	3ad2ant3	\|- ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( F : A --> ran F <-> F : A --> C ) )
5	2 4	mpbid	\|- ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> F : A --> C )
6		f1cof1b	\|- ( ( F : A --> C /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -1-1-> D <-> ( F : A -1-1-> C /\ G : C -1-1-> D ) ) )
7	5 6	syld3an1	\|- ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -1-1-> D <-> ( F : A -1-1-> C /\ G : C -1-1-> D ) ) )
8		ffn	\|- ( F : A --> B -> F Fn A )
9		fnfocofob	\|- ( ( F Fn A /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -onto-> D <-> G : C -onto-> D ) )
10	8 9	syl3an1	\|- ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -onto-> D <-> G : C -onto-> D ) )
11	7 10	anbi12d	\|- ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( ( G o. F ) : A -1-1-> D /\ ( G o. F ) : A -onto-> D ) <-> ( ( F : A -1-1-> C /\ G : C -1-1-> D ) /\ G : C -onto-> D ) ) )
12		anass	\|- ( ( ( F : A -1-1-> C /\ G : C -1-1-> D ) /\ G : C -onto-> D ) <-> ( F : A -1-1-> C /\ ( G : C -1-1-> D /\ G : C -onto-> D ) ) )
13	11 12	bitrdi	\|- ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( ( G o. F ) : A -1-1-> D /\ ( G o. F ) : A -onto-> D ) <-> ( F : A -1-1-> C /\ ( G : C -1-1-> D /\ G : C -onto-> D ) ) ) )
14		df-f1o	\|- ( ( G o. F ) : A -1-1-onto-> D <-> ( ( G o. F ) : A -1-1-> D /\ ( G o. F ) : A -onto-> D ) )
15		df-f1o	\|- ( G : C -1-1-onto-> D <-> ( G : C -1-1-> D /\ G : C -onto-> D ) )
16	15	anbi2i	\|- ( ( F : A -1-1-> C /\ G : C -1-1-onto-> D ) <-> ( F : A -1-1-> C /\ ( G : C -1-1-> D /\ G : C -onto-> D ) ) )
17	13 14 16	3bitr4g	\|- ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -1-1-onto-> D <-> ( F : A -1-1-> C /\ G : C -1-1-onto-> D ) ) )