Theorem f1ocnv 3809

Description: The converse of a one-to-one onto function is also one-to-one onto.

Assertion

Ref	Expression
f1ocnv	⊢ (F:A–1-1-onto→B → ◡F:B–1-1-onto→A)

Proof of Theorem f1ocnv

Step	Hyp	Ref	Expression
1		df-rn 3270	. . . . . . . 8 ⊢ ran F = dom ◡ F
2	1	eqeq1i 1525	. . . . . . 7 ⊢ (ran F = B ↔ dom ◡ F = B)
3	2	anbi2i 483	. . . . . 6 ⊢ ((Fun ◡F ⋀ ran F = B) ↔ (Fun ◡F ⋀ dom ◡ F = B))
4		df-fn 3274	. . . . . 6 ⊢ (◡F Fn B ↔ (Fun ◡F ⋀ dom ◡ F = B))
5	3, 4	bitr4i 174	. . . . 5 ⊢ ((Fun ◡F ⋀ ran F = B) ↔ ◡F Fn B)
6	5	biimpi 149	. . . 4 ⊢ ((Fun ◡F ⋀ ran F = B) → ◡F Fn B)
7		fnfun 3691	. . . . . 6 ⊢ (F Fn A → Fun F)
8		funcnvcnv 3660	. . . . . 6 ⊢ (Fun F → Fun ◡◡F)
9	7, 8	syl 10	. . . . 5 ⊢ (F Fn A → Fun ◡◡F)
10		fndm 3693	. . . . . 6 ⊢ (F Fn A → dom F = A)
11		dfdm4 3396	. . . . . 6 ⊢ dom F = ran ◡ F
12	10, 11	syl5eqr 1564	. . . . 5 ⊢ (F Fn A → ran ◡ F = A)
13	9, 12	jca 286	. . . 4 ⊢ (F Fn A → (Fun ◡◡F ⋀ ran ◡ F = A))
14	6, 13	anim12i 331	. . 3 ⊢ (((Fun ◡F ⋀ ran F = B) ⋀ F Fn A) → (◡F Fn B ⋀ (Fun ◡◡F ⋀ ran ◡ F = A)))
15	14	ancoms 438	. 2 ⊢ ((F Fn A ⋀ (Fun ◡F ⋀ ran F = B)) → (◡F Fn B ⋀ (Fun ◡◡F ⋀ ran ◡ F = A)))
16		dff1o2 3801	. . 3 ⊢ (F:A–1-1-onto→B ↔ (F Fn A ⋀ Fun ◡F ⋀ ran F = B))
17		3anass 785	. . 3 ⊢ ((F Fn A ⋀ Fun ◡F ⋀ ran F = B) ↔ (F Fn A ⋀ (Fun ◡F ⋀ ran F = B)))
18	16, 17	bitri 171	. 2 ⊢ (F:A–1-1-onto→B ↔ (F Fn A ⋀ (Fun ◡F ⋀ ran F = B)))
19		dff1o2 3801	. . 3 ⊢ (◡F:B–1-1-onto→A ↔ (◡F Fn B ⋀ Fun ◡◡F ⋀ ran ◡ F = A))
20		3anass 785	. . 3 ⊢ ((◡F Fn B ⋀ Fun ◡◡F ⋀ ran ◡ F = A) ↔ (◡F Fn B ⋀ (Fun ◡◡F ⋀ ran ◡ F = A)))
21	19, 20	bitri 171	. 2 ⊢ (◡F:B–1-1-onto→A ↔ (◡F Fn B ⋀ (Fun ◡◡F ⋀ ran ◡ F = A)))
22	15, 18, 21	3imtr4i 217	1 ⊢ (F:A–1-1-onto→B → ◡F:B–1-1-onto→A)

Syntax hints:   → wi 3   ⋀ wa 221   ⋀ w3a 781   = wceq 992  ^◡ccnv 3250  dom cdm 3251  ran crn 3252  Fun wfun 3257   Fn wfn 3258  –1-1-onto→wf1o 3262

This theorem is referenced by:  f1ocnvb 3810  f1orescnv 3812  f1imacnv 3813  f1ococnv2 3819  f1ococnv1 3820  f1dmex 3821  f1ocnvfv1 3992  f1ocnvfv2 3993  f1ofveu 3996  f1ocnvfv3 3997  f1ocnvdm 3998  isocnv 4010  ener 4551  en0 4564  en1 4567  ac6sfi 4591  mapenlem2 4637  ssenen 4651  fodomfi 4709  weth 4933  uzrdgvali 6666  uzrdgsuci 6668  uzrdgfnuzi 6670  unbenlem 7716  effoi 9017  logrn 9023  logf1o 9027  cnvunop 10122  unopadj 10123  symggrpi 10691  f2imacnv 10758  f1ofi 10778  cnvhmpha 11031  hmphsyma 11034  hmeobc 11048  finsschain 11425  opncldf3 11456  compfipin0lem 11492  compfipin0 11493  comptoppr 11495  conntoppr 11504  fbssint 11626  fcluscomplem 11732  f1ocan1fv 11816  f1ocan2fv 11817  hmeocnv 11959  ismtycnv 12005  ismtyhmeo 12007

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-br 2693  df-opab 2741  df-id 2913  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278

Copyright terms: Public domain