MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnvexg Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 relcnv 6061 . . 3 Rel 𝐴
2 relssdmrn 6225 . . 3 (Rel 𝐴𝐴 ⊆ (dom 𝐴 × ran 𝐴))
31, 2ax-mp 5 . 2 𝐴 ⊆ (dom 𝐴 × ran 𝐴)
4 df-rn 5649 . . . 4 ran 𝐴 = dom 𝐴
5 rnexg 7846 . . . 4 (𝐴𝑉 → ran 𝐴 ∈ V)
64, 5eqeltrrid 2843 . . 3 (𝐴𝑉 → dom 𝐴 ∈ V)
7 dfdm4 5856 . . . 4 dom 𝐴 = ran 𝐴
8 dmexg 7845 . . . 4 (𝐴𝑉 → dom 𝐴 ∈ V)
97, 8eqeltrrid 2843 . . 3 (𝐴𝑉 → ran 𝐴 ∈ V)
106, 9xpexd 7690 . 2 (𝐴𝑉 → (dom 𝐴 × ran 𝐴) ∈ V)
11 ssexg 5285 . 2 ((𝐴 ⊆ (dom 𝐴 × ran 𝐴) ∧ (dom 𝐴 × ran 𝐴) ∈ V) → 𝐴 ∈ V)
123, 10, 11sylancr 588 1 (𝐴𝑉𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3448  wss 3915   × 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  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 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  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  9349  wemapwe  9640  hasheqf1oi  14258  brtrclfvcnv  14896  brcnvtrclfvcnv  14897  relexpcnv  14927  relexpnnrn  14937  relexpaddg  14945  imasle  17412  cnvps  18474  gsumvalx  18538  symginv  19191  tposmap  21822  metustel  23922  metustss  23923  metustfbas  23929  metuel2  23937  psmetutop  23939  restmetu  23942  itg2gt0  25141  nlfnval  30865  fnpreimac  31629  ffsrn  31688  pwrssmgc  31902  tocycfv  32000  elrspunidl  32243  rhmpreimacnlem  32505  eulerpartlemgs2  33020  orvcval  33097  coinfliprv  33122  cossex  36910  cosscnvex  36911  cnvelrels  36986  lkrval  37579  pw2f1o2val  41392  lmhmlnmsplit  41443  cnvcnvintabd  41946  clrellem  41968  relexpaddss  42064  cnvtrclfv  42070  rntrclfvRP  42077  xpexb  42808  sge0f1o  44697  smfco  45117  preimafvelsetpreimafv  45654  fundcmpsurinjlem2  45665
  Copyright terms: Public domain W3C validator