Theorem cnvexg 7866

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 6061	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6225	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5649	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7846	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2837	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5856	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7845	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2837	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7690	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5285	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 587	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3446   ⊆ wss 3913   × cxp 5636  ^◡ccnv 5637  dom cdm 5638  ran crn 5639  Rel wrel 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-xp 5644  df-rel 5645  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  cnvex  7867  relcnvexb  7868  cofunex2g  7887  tposexg  8176  cnven  8984  cnvct  8985  fopwdom  9031  domssex2  9088  domssex  9089  cnvfiALT  9285  mapfienlem2  9351  wemapwe  9642  hasheqf1oi  14261  brtrclfvcnv  14901  brcnvtrclfvcnv  14902  relexpcnv  14932  relexpnnrn  14942  relexpaddg  14950  imasle  17419  cnvps  18481  gsumvalx  18545  symginv  19198  tposmap  21843  metustel  23943  metustss  23944  metustfbas  23950  metuel2  23958  psmetutop  23960  restmetu  23963  itg2gt0  25162  nlfnval  30886  fnpreimac  31654  ffsrn  31714  pwrssmgc  31930  tocycfv  32028  elrspunidl  32279  ply1degltdimlem  32404  rhmpreimacnlem  32554  eulerpartlemgs2  33069  orvcval  33146  coinfliprv  33171  cossex  36954  cosscnvex  36955  cnvelrels  37030  lkrval  37623  pw2f1o2val  41421  lmhmlnmsplit  41472  cnvcnvintabd  41994  clrellem  42016  relexpaddss  42112  cnvtrclfv  42118  rntrclfvRP  42125  xpexb  42856  sge0f1o  44743  smfco  45163  preimafvelsetpreimafv  45700  fundcmpsurinjlem2  45711