Theorem fimacnv 6490

Description: The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007.)

Assertion

Ref	Expression
fimacnv	⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)

Proof of Theorem fimacnv

Step	Hyp	Ref	Expression
1		imassrn 5618	. . 3 ⊢ (◡𝐹 “ 𝐵) ⊆ ran ◡𝐹
2		dfdm4 5454	. . . 4 ⊢ dom 𝐹 = ran ◡𝐹
3		fdm 6191	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
4		ssid 3773	. . . . 5 ⊢ 𝐴 ⊆ 𝐴
5	3, 4	syl6eqss 3804	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 ⊆ 𝐴)
6	2, 5	syl5eqssr 3799	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ran ◡𝐹 ⊆ 𝐴)
7	1, 6	syl5ss 3763	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) ⊆ 𝐴)
8		imassrn 5618	. . . 4 ⊢ (𝐹 “ 𝐴) ⊆ ran 𝐹
9		frn 6193	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
10	8, 9	syl5ss 3763	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 “ 𝐴) ⊆ 𝐵)
11		ffun 6188	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)
12	4, 3	syl5sseqr 3803	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 ⊆ dom 𝐹)
13		funimass3 6476	. . . 4 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ 𝐵)))
14	11, 12, 13	syl2anc 565	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ 𝐵)))
15	10, 14	mpbid 222	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 ⊆ (◡𝐹 “ 𝐵))
16	7, 15	eqssd 3769	1 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1631   ⊆ wss 3723  ^◡ccnv 5248  dom cdm 5249  ran crn 5250   “ cima 5252  Fun wfun 6025  ⟶wf 6027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-fv 6039

This theorem is referenced by:  fimacnvinrn  6491  fmpt  6523  frnsuppeq  7457  fin1a2lem7  9429  cnclima  21292  iscncl  21293  cnindis  21316  cncmp  21415  ptrescn  21662  qtopuni  21725  qtopcld  21736  qtopcmap  21742  ordthmeolem  21824  rnelfmlem  21975  mbfdm  23613  ismbf  23615  mbfimaicc  23618  ismbf2d  23627  ismbf3d  23640  mbfimaopn2  23643  i1fd  23667  plyeq0  24186  fsumcvg4  30333  zrhunitpreima  30359  imambfm  30661  carsggect  30717  dstrvprob  30870  poimirlem30  33768  dvtan  33788  smfresal  41511