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

Theorem cnvexg 7097
 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 5491 . . 3 Rel 𝐴
2 relssdmrn 5644 . . 3 (Rel 𝐴𝐴 ⊆ (dom 𝐴 × ran 𝐴))
31, 2ax-mp 5 . 2 𝐴 ⊆ (dom 𝐴 × ran 𝐴)
4 df-rn 5115 . . . 4 ran 𝐴 = dom 𝐴
5 rnexg 7083 . . . 4 (𝐴𝑉 → ran 𝐴 ∈ V)
64, 5syl5eqelr 2704 . . 3 (𝐴𝑉 → dom 𝐴 ∈ V)
7 dfdm4 5305 . . . 4 dom 𝐴 = ran 𝐴
8 dmexg 7082 . . . 4 (𝐴𝑉 → dom 𝐴 ∈ V)
97, 8syl5eqelr 2704 . . 3 (𝐴𝑉 → ran 𝐴 ∈ V)
10 xpexg 6945 . . 3 ((dom 𝐴 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐴 × ran 𝐴) ∈ V)
116, 9, 10syl2anc 692 . 2 (𝐴𝑉 → (dom 𝐴 × ran 𝐴) ∈ V)
12 ssexg 4795 . 2 ((𝐴 ⊆ (dom 𝐴 × ran 𝐴) ∧ (dom 𝐴 × ran 𝐴) ∈ V) → 𝐴 ∈ V)
133, 11, 12sylancr 694 1 (𝐴𝑉𝐴 ∈ V)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1988  Vcvv 3195   ⊆ wss 3567   × cxp 5102  ◡ccnv 5103  dom cdm 5104  ran crn 5105  Rel wrel 5109 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-xp 5110  df-rel 5111  df-cnv 5112  df-dm 5114  df-rn 5115 This theorem is referenced by:  cnvex  7098  relcnvexb  7099  cofunex2g  7116  tposexg  7351  cnven  8017  cnvct  8018  fopwdom  8053  domssex2  8105  domssex  8106  cnvfi  8233  mapfienlem2  8296  wemapwe  8579  hasheqf1oi  13123  hasheqf1oiOLD  13124  brtrclfvcnv  13726  brcnvtrclfvcnv  13727  relexpcnv  13756  relexpnnrn  13766  relexpaddg  13774  imasle  16164  cnvps  17193  gsumvalx  17251  symginv  17803  tposmap  20244  metustel  22336  metustss  22337  metustfbas  22343  metuel2  22351  psmetutop  22353  restmetu  22356  itg2gt0  23508  nlfnval  28710  ffsrn  29478  eulerpartlemgs2  30416  orvcval  30493  coinfliprv  30518  lkrval  34194  pw2f1o2val  37425  lmhmlnmsplit  37476  cnvcnvintabd  37725  clrellem  37748  relexpaddss  37829  cnvtrclfv  37835  rntrclfvRP  37842  xpexb  38478  sge0f1o  40362  smfco  40772
 Copyright terms: Public domain W3C validator