Theorem f1ocnv 3777

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 3244	. . . . . . . 8 |- ran F = dom `' F
2	1	eqeq1i 1519	. . . . . . 7 |- (ran F = B <-> dom `' F = B)
3	2	anbi2i 482	. . . . . 6 |- ((Fun `'F /\ ran F = B) <-> (Fun `'F /\ dom `' F = B))
4		df-fn 3248	. . . . . 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 3660	. . . . . 6 |- (F Fn A -> Fun F)
8		funcnvcnv 3630	. . . . . 6 |- (Fun F -> Fun `'`'F)
9	7, 8	syl 10	. . . . 5 |- (F Fn A -> Fun `'`'F)
10		fndm 3662	. . . . . 6 |- (F Fn A -> dom F = A)
11		dfdm4 3369	. . . . . 6 |- dom F = ran `' F
12	10, 11	syl5eqr 1558	. . . . 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 3769	. . 3 |- (F:A-1-1-onto->B <-> (F Fn A /\ Fun `'F /\ ran F = B))
17		3anass 782	. . 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 3769	. . 3 |- (`'F:B-1-1-onto->A <-> (`'F Fn B /\ Fun `'`'F /\ ran `' F = A))
20		3anass 782	. . 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 778   = wceq 988  `'ccnv 3224  dom cdm 3225  ran crn 3226  Fun wfun 3231   Fn wfn 3232  -1-1-onto->wf1o 3236

This theorem is referenced by:  f1ocnvb 3778  f1orescnv 3780  f1imacnv 3781  f1ococnv2 3784  f1ococnv1 3785  f1dmex 3786  f1ocnvfv1 3954  f1ocnvfv2 3955  f1ofveu 3958  f1ocnvfv3 3959  f1ocnvdm 3960  isocnv 3972  ener 4497  en0 4510  en1 4513  mapenlem2 4579  ssenen 4593  fodomfi 4650  weth 4873  uzrdgvali 6595  uzrdgsuci 6597  uzrdgfnuzi 6599  unbenlem 7629  effoi 8864  logrn 8870  logf1o 8874  cnvunop 9960  unopadj 9961  symggrpi 10527  f2imacnv 10592  cnvhmpha 10661  hmphsyma 10664  hmeobc 10678

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3an 780  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-br 2670  df-opab 2718  df-id 2889  df-xp 3239  df-rel 3240  df-cnv 3241  df-co 3242  df-dm 3243  df-rn 3244  df-fun 3247  df-fn 3248  df-f 3249  df-f1 3250  df-fo 3251  df-f1o 3252

Copyright terms: Public domain