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 ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1-onto→ 𝐷 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐶 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 ffrn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 ⟶ ran 𝐹 )
2 1 3ad2ant1 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → 𝐹 : 𝐴 ⟶ ran 𝐹 )
3 feq3 ⊢ ( ran 𝐹 = 𝐶 → ( 𝐹 : 𝐴 ⟶ ran 𝐹 ↔ 𝐹 : 𝐴 ⟶ 𝐶 ) )
4 3 3ad2ant3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( 𝐹 : 𝐴 ⟶ ran 𝐹 ↔ 𝐹 : 𝐴 ⟶ 𝐶 ) )
5 2 4 mpbid ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → 𝐹 : 𝐴 ⟶ 𝐶 )
6 f1cof1b ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐶 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ) )
7 5 6 syld3an1 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐶 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ) )
8 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
9 fnfocofob ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –onto→ 𝐷 ↔ 𝐺 : 𝐶 –onto→ 𝐷 ) )
10 8 9 syl3an1 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –onto→ 𝐷 ↔ 𝐺 : 𝐶 –onto→ 𝐷 ) )
11 7 10 anbi12d ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ∧ ( 𝐺 ∘ 𝐹 ) : 𝐴 –onto→ 𝐷 ) ↔ ( ( 𝐹 : 𝐴 –1-1→ 𝐶 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ) )
12 anass ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐶 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ↔ ( 𝐹 : 𝐴 –1-1→ 𝐶 ∧ ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ) )
13 11 12 bitrdi ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ∧ ( 𝐺 ∘ 𝐹 ) : 𝐴 –onto→ 𝐷 ) ↔ ( 𝐹 : 𝐴 –1-1→ 𝐶 ∧ ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ) ) )
14 df-f1o ⊢ ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1-onto→ 𝐷 ↔ ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ∧ ( 𝐺 ∘ 𝐹 ) : 𝐴 –onto→ 𝐷 ) )
15 df-f1o ⊢ ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 ↔ ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) )
16 15 anbi2i ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐶 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ) ↔ ( 𝐹 : 𝐴 –1-1→ 𝐶 ∧ ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ) )
17 13 14 16 3bitr4g ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1-onto→ 𝐷 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐶 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ) ) )