![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnvexg | Structured version Visualization version GIF version |
Description: The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 17-Mar-1998.) |
Ref | Expression |
---|---|
cnvexg | ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcnv 6054 | . . 3 ⊢ Rel ◡𝐴 | |
2 | relssdmrn 6218 | . . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) |
4 | df-rn 5642 | . . . 4 ⊢ ran 𝐴 = dom ◡𝐴 | |
5 | rnexg 7837 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V) | |
6 | 4, 5 | eqeltrrid 2843 | . . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V) |
7 | dfdm4 5849 | . . . 4 ⊢ dom 𝐴 = ran ◡𝐴 | |
8 | dmexg 7836 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V) | |
9 | 7, 8 | eqeltrrid 2843 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V) |
10 | 6, 9 | xpexd 7681 | . 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V) |
11 | ssexg 5278 | . 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V) | |
12 | 3, 10, 11 | sylancr 587 | 1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 Vcvv 3443 ⊆ wss 3908 × cxp 5629 ◡ccnv 5630 dom cdm 5631 ran crn 5632 Rel wrel 5636 |
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 2707 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 ax-un 7668 |
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 2714 df-cleq 2728 df-clel 2814 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-xp 5637 df-rel 5638 df-cnv 5639 df-dm 5641 df-rn 5642 |
This theorem is referenced by: cnvex 7858 relcnvexb 7859 cofunex2g 7878 tposexg 8167 cnven 8973 cnvct 8974 fopwdom 9020 domssex2 9077 domssex 9078 cnvfiALT 9274 mapfienlem2 9338 wemapwe 9629 hasheqf1oi 14243 brtrclfvcnv 14881 brcnvtrclfvcnv 14882 relexpcnv 14912 relexpnnrn 14922 relexpaddg 14930 imasle 17397 cnvps 18459 gsumvalx 18523 symginv 19175 tposmap 21790 metustel 23890 metustss 23891 metustfbas 23897 metuel2 23905 psmetutop 23907 restmetu 23910 itg2gt0 25109 nlfnval 30709 fnpreimac 31473 ffsrn 31529 pwrssmgc 31743 tocycfv 31841 elrspunidl 32082 rhmpreimacnlem 32334 eulerpartlemgs2 32849 orvcval 32926 coinfliprv 32951 cossex 36848 cosscnvex 36849 cnvelrels 36924 lkrval 37517 pw2f1o2val 41301 lmhmlnmsplit 41352 cnvcnvintabd 41814 clrellem 41836 relexpaddss 41932 cnvtrclfv 41938 rntrclfvRP 41945 xpexb 42676 sge0f1o 44555 smfco 44975 preimafvelsetpreimafv 45512 fundcmpsurinjlem2 45523 |
Copyright terms: Public domain | W3C validator |