Theorem cnvexg 4527

Description: The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26.

Assertion

Ref	Expression
cnvexg	|- (A e. V -> `'A e. _V)

Proof of Theorem cnvexg

Step	Hyp	Ref	Expression
1		relcnv 4419	. . 3 |- Rel `'A
2		relssdmrn 4516	. . 3 |- (Rel `'A -> `'A C_ (dom `' A X. ran `' A))
3	1, 2	ax-mp 7	. 2 |- `'A C_ (dom `' A X. ran `' A)
4		df-rn 4138	. . . 4 |- ran A = dom `' A
5		rnexg 4329	. . . 4 |- (A e. V -> ran A e. _V)
6	4, 5	syl5eqelr 2224	. . 3 |- (A e. V -> dom `' A e. _V)
7		dfdm4 4277	. . . 4 |- dom A = ran `' A
8		dmexg 4328	. . . 4 |- (A e. V -> dom A e. _V)
9	7, 8	syl5eqelr 2224	. . 3 |- (A e. V -> ran `' A e. _V)
10		xpexg 4225	. . 3 |- ((dom `' A e. _V /\ ran `' A e. _V) -> (dom `' A X. ran `' A) e. _V)
11	6, 9, 10	syl11anc 659	. 2 |- (A e. V -> (dom `' A X. ran `' A) e. _V)
12		ssexg 3624	. 2 |- ((`'A C_ (dom `' A X. ran `' A) /\ (dom `' A X. ran `' A) e. _V) -> `'A e. _V)
13	3, 11, 12	sylancr 662	1 |- (A e. V -> `'A e. _V)

Syntax hints:   -> wi 3   e. wcel 1588  _Vcvv 2538   C_ wss 2827   X. cxp 4117  `'ccnv 4118  dom cdm 4119  ran crn 4120  Rel wrel 4124

This theorem is referenced by:  cnvex 4528  relcnvexb 4529  cofunex2g 4601  fodom 6374  tx1cn 11058  tx2cn 11059  cnvhmpha 11075  cncomp 11169  injrec2 15178  dupre1 15323  dupos1 15325  dutos1 15365  supwval 15368  mapdiscnlem 15627  cnvhmphb 15637  cnvhmph 15638  hmphsyma 15639  intopcoaconb 15662  intopcoaconc 15663  prcnt 15686  cnconn 16268  cnres 16713  hmeocnv 16722  xpexb 17259

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-rex 2360  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-uni 3367  df-br 3508  df-opab 3566  df-xp 4133  df-rel 4134  df-cnv 4135  df-dm 4137  df-rn 4138

Copyright terms: Public domain