Theorem focdmex 7898

Description: If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.)

Assertion

Ref	Expression
focdmex	⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V))

Proof of Theorem focdmex

Step	Hyp	Ref	Expression
1		fofun 6740	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹)
2		funrnex 7896	. . . 4 ⊢ (dom 𝐹 ∈ 𝐶 → (Fun 𝐹 → ran 𝐹 ∈ V))
3	1, 2	syl5com 31	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → (dom 𝐹 ∈ 𝐶 → ran 𝐹 ∈ V))
4		fof 6739	. . . . 5 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
5	4	fdmd 6665	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴)
6	5	eleq1d 2824	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → (dom 𝐹 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7		forn 6742	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
8	7	eleq1d 2824	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → (ran 𝐹 ∈ V ↔ 𝐵 ∈ V))
9	3, 6, 8	3imtr3d 294	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐴 ∈ 𝐶 → 𝐵 ∈ V))
10	9	com12 32	1 ⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V))

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3431  dom cdm 5618  ran crn 5619  Fun wfun 6479  –onto→wfo 6483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493

This theorem is referenced by:  f1dmex  7899  f1ovv  7900  fsetprcnex  8799  f1oeng  8907  fodomnum  9970  ttukeylem1  10422  fodomb  10439  cnexALT  12927  hasheqf1oi  14304  imasbas  17467  imasds  17468  elqtop  23680  qtoprest  23700  indishmph  23781  imasf1oxmet  24358  noprc  27766  foresf1o  32592  sge0f1o  46825  sge0fodjrnlem  46859