Theorem cnvexg 7925

Description: The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 17-Mar-1998.)

Assertion

Ref	Expression
cnvexg	⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Proof of Theorem cnvexg

Step	Hyp	Ref	Expression
1		relcnv 6096	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6262	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5670	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7903	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2840	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5880	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7902	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2840	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7750	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5298	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 587	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3464   ⊆ wss 3931   × cxp 5657  ^◡ccnv 5658  dom cdm 5659  ran crn 5660  Rel wrel 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-xp 5665  df-rel 5666  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  cnvex  7926  relcnvexb  7927  cofunex2g  7953  tposexg  8244  cnven  9052  cnvct  9053  fopwdom  9099  domssex2  9156  domssex  9157  cnvfiALT  9356  mapfienlem2  9423  wemapwe  9716  hasheqf1oi  14374  brtrclfvcnv  15028  brcnvtrclfvcnv  15029  relexpcnv  15059  relexpnnrn  15069  relexpaddg  15077  imasle  17542  cnvps  18593  gsumvalx  18659  symginv  19388  tposmap  22400  metustel  24494  metustss  24495  metustfbas  24501  metuel2  24509  psmetutop  24511  restmetu  24514  itg2gt0  25718  nlfnval  31867  fnpreimac  32654  ffsrn  32711  pwrssmgc  32985  tocycfv  33125  elrspunidl  33448  ply1degltdimlem  33667  algextdeglem8  33763  rhmpreimacnlem  33920  eulerpartlemgs2  34417  orvcval  34495  coinfliprv  34520  cossex  38442  cosscnvex  38443  cnvelrels  38518  lkrval  39111  aks6d1c2lem4  42145  aks6d1c6lem2  42189  aks6d1c6lem3  42190  pw2f1o2val  43030  lmhmlnmsplit  43078  cnvcnvintabd  43591  clrellem  43613  relexpaddss  43709  cnvtrclfv  43715  rntrclfvRP  43722  xpexb  44445  sge0f1o  46378  smfco  46798  preimafvelsetpreimafv  47369  fundcmpsurinjlem2  47380  grimcnv  47868  grlicsym  47985  imasubclem1  49030