Metamath Proof Explorer

Theorem 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 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → ( ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐴 ) –onto→ 𝐵 ↔ 𝐺 : 𝐴 –onto→ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fdmrn ⊢ ( Fun 𝐹 ↔ 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
2 1 biimpi ⊢ ( Fun 𝐹 → 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
3 2 3ad2ant1 ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
4 3 adantr ⊢ ( ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) ∧ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐴 ) –onto→ 𝐵 ) → 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
5 eqid ⊢ ( ran 𝐹 ∩ 𝐴 ) = ( ran 𝐹 ∩ 𝐴 )
6 eqid ⊢ ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ 𝐴 )
7 eqid ⊢ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐴 ) ) = ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐴 ) )
8 simp2 ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → 𝐺 : 𝐴 ⟶ 𝐵 )
9 8 adantr ⊢ ( ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) ∧ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐴 ) –onto→ 𝐵 ) → 𝐺 : 𝐴 ⟶ 𝐵 )
10 eqid ⊢ ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐴 ) ) = ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐴 ) )
11 simpr ⊢ ( ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) ∧ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐴 ) –onto→ 𝐵 ) → ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐴 ) –onto→ 𝐵 )
12 4 5 6 7 9 10 11 fcoresfo ⊢ ( ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) ∧ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐴 ) –onto→ 𝐵 ) → ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐴 ) ) : ( ran 𝐹 ∩ 𝐴 ) –onto→ 𝐵 )
13 12 ex ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → ( ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐴 ) –onto→ 𝐵 → ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐴 ) ) : ( ran 𝐹 ∩ 𝐴 ) –onto→ 𝐵 ) )
14 sseqin2 ⊢ ( 𝐴 ⊆ ran 𝐹 ↔ ( ran 𝐹 ∩ 𝐴 ) = 𝐴 )
15 14 biimpi ⊢ ( 𝐴 ⊆ ran 𝐹 → ( ran 𝐹 ∩ 𝐴 ) = 𝐴 )
16 15 3ad2ant3 ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → ( ran 𝐹 ∩ 𝐴 ) = 𝐴 )
17 8 fdmd ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → dom 𝐺 = 𝐴 )
18 16 17 eqtr4d ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → ( ran 𝐹 ∩ 𝐴 ) = dom 𝐺 )
19 18 reseq2d ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐴 ) ) = ( 𝐺 ↾ dom 𝐺 ) )
20 8 freld ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → Rel 𝐺 )
21 resdm ⊢ ( Rel 𝐺 → ( 𝐺 ↾ dom 𝐺 ) = 𝐺 )
22 20 21 syl ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → ( 𝐺 ↾ dom 𝐺 ) = 𝐺 )
23 19 22 eqtrd ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐴 ) ) = 𝐺 )
24 eqidd ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → 𝐵 = 𝐵 )
25 23 16 24 foeq123d ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐴 ) ) : ( ran 𝐹 ∩ 𝐴 ) –onto→ 𝐵 ↔ 𝐺 : 𝐴 –onto→ 𝐵 ) )
26 13 25 sylibd ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → ( ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐴 ) –onto→ 𝐵 → 𝐺 : 𝐴 –onto→ 𝐵 ) )
27 simpr ⊢ ( ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → 𝐺 : 𝐴 –onto→ 𝐵 )
28 simpl1 ⊢ ( ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → Fun 𝐹 )
29 simpl3 ⊢ ( ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → 𝐴 ⊆ ran 𝐹 )
30 focofo ⊢ ( ( 𝐺 : 𝐴 –onto→ 𝐵 ∧ Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ) → ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐴 ) –onto→ 𝐵 )
31 27 28 29 30 syl3anc ⊢ ( ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐴 ) –onto→ 𝐵 )
32 31 ex ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → ( 𝐺 : 𝐴 –onto→ 𝐵 → ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐴 ) –onto→ 𝐵 ) )
33 26 32 impbid ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → ( ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐴 ) –onto→ 𝐵 ↔ 𝐺 : 𝐴 –onto→ 𝐵 ) )