|   | 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 6121 | . . 3 ⊢ Rel ◡𝐴 | |
| 2 | relssdmrn 6287 | . . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)) | |
| 3 | 1, 2 | ax-mp 5 | . 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) | 
| 4 | df-rn 5695 | . . . 4 ⊢ ran 𝐴 = dom ◡𝐴 | |
| 5 | rnexg 7925 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V) | |
| 6 | 4, 5 | eqeltrrid 2845 | . . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V) | 
| 7 | dfdm4 5905 | . . . 4 ⊢ dom 𝐴 = ran ◡𝐴 | |
| 8 | dmexg 7924 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V) | |
| 9 | 7, 8 | eqeltrrid 2845 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V) | 
| 10 | 6, 9 | xpexd 7772 | . 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V) | 
| 11 | ssexg 5322 | . 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 2107 Vcvv 3479 ⊆ wss 3950 × cxp 5682 ◡ccnv 5683 dom cdm 5684 ran crn 5685 Rel wrel 5689 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ral 3061 df-rex 3070 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-br 5143 df-opab 5205 df-xp 5690 df-rel 5691 df-cnv 5692 df-dm 5694 df-rn 5695 | 
| This theorem is referenced by: cnvex 7948 relcnvexb 7949 cofunex2g 7975 tposexg 8266 cnven 9074 cnvct 9075 fopwdom 9121 domssex2 9178 domssex 9179 cnvfiALT 9380 mapfienlem2 9447 wemapwe 9738 hasheqf1oi 14391 brtrclfvcnv 15044 brcnvtrclfvcnv 15045 relexpcnv 15075 relexpnnrn 15085 relexpaddg 15093 imasle 17569 cnvps 18624 gsumvalx 18690 symginv 19421 tposmap 22464 metustel 24564 metustss 24565 metustfbas 24571 metuel2 24579 psmetutop 24581 restmetu 24584 itg2gt0 25796 nlfnval 31901 fnpreimac 32682 ffsrn 32741 pwrssmgc 32991 tocycfv 33130 elrspunidl 33457 ply1degltdimlem 33674 algextdeglem8 33766 rhmpreimacnlem 33884 eulerpartlemgs2 34383 orvcval 34461 coinfliprv 34486 cossex 38421 cosscnvex 38422 cnvelrels 38497 lkrval 39090 aks6d1c2lem4 42129 aks6d1c6lem2 42173 aks6d1c6lem3 42174 pw2f1o2val 43056 lmhmlnmsplit 43104 cnvcnvintabd 43618 clrellem 43640 relexpaddss 43736 cnvtrclfv 43742 rntrclfvRP 43749 xpexb 44478 sge0f1o 46402 smfco 46822 preimafvelsetpreimafv 47380 fundcmpsurinjlem2 47391 grimcnv 47884 grlicsym 47978 | 
| Copyright terms: Public domain | W3C validator |