Theorem focofo 6828

Description: Composition of onto functions. Generalisation of foco 6829. (Contributed by AV, 29-Sep-2024.)

Assertion

Ref	Expression
focofo	⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐴)–onto→𝐵)

Proof of Theorem focofo

Step	Hyp	Ref	Expression
1		fof 6815	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
2		fcof 6751	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐴)⟶𝐵)
3	1, 2	sylan 578	. . 3 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐴)⟶𝐵)
4	3	3adant3 1129	. 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐴)⟶𝐵)
5		rnco 6263	. . 3 ⊢ ran (𝐹 ∘ 𝐺) = ran (𝐹 ↾ ran 𝐺)
6	1	freld 6734	. . . . . 6 ⊢ (𝐹:𝐴–onto→𝐵 → Rel 𝐹)
7	6	3ad2ant1 1130	. . . . 5 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺) → Rel 𝐹)
8		fdm 6737	. . . . . . . . 9 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
9	8	eqcomd 2732	. . . . . . . 8 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = dom 𝐹)
10	1, 9	syl 17	. . . . . . 7 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐴 = dom 𝐹)
11	10	sseq1d 4011	. . . . . 6 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐴 ⊆ ran 𝐺 ↔ dom 𝐹 ⊆ ran 𝐺))
12	11	biimpa 475	. . . . 5 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐴 ⊆ ran 𝐺) → dom 𝐹 ⊆ ran 𝐺)
13		relssres 6031	. . . . . 6 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ ran 𝐺) → (𝐹 ↾ ran 𝐺) = 𝐹)
14	13	rneqd 5944	. . . . 5 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ ran 𝐺) → ran (𝐹 ↾ ran 𝐺) = ran 𝐹)
15	7, 12, 14	3imp3i2an 1342	. . . 4 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺) → ran (𝐹 ↾ ran 𝐺) = ran 𝐹)
16		forn 6818	. . . . 5 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
17	16	3ad2ant1 1130	. . . 4 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺) → ran 𝐹 = 𝐵)
18	15, 17	eqtrd 2766	. . 3 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺) → ran (𝐹 ↾ ran 𝐺) = 𝐵)
19	5, 18	eqtrid 2778	. 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺) → ran (𝐹 ∘ 𝐺) = 𝐵)
20		dffo2 6819	. 2 ⊢ ((𝐹 ∘ 𝐺):(◡𝐺 “ 𝐴)–onto→𝐵 ↔ ((𝐹 ∘ 𝐺):(◡𝐺 “ 𝐴)⟶𝐵 ∧ ran (𝐹 ∘ 𝐺) = 𝐵))
21	4, 19, 20	sylanbrc 581	1 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐴)–onto→𝐵)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084   = wceq 1534   ⊆ wss 3947  ^◡ccnv 5681  dom cdm 5682  ran crn 5683   ↾ cres 5684   “ cima 5685   ∘ ccom 5686  Rel wrel 5687  Fun wfun 6548  ⟶wf 6550  –onto→wfo 6552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-br 5154  df-opab 5216  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-fun 6556  df-fn 6557  df-f 6558  df-fo 6560

This theorem is referenced by:  foco  6829  funfocofob  46691