![]() |
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 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 2843 | . . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V) |
7 | dfdm4 5856 | . . . 4 ⊢ dom 𝐴 = ran ◡𝐴 | |
8 | dmexg 7845 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V) | |
9 | 7, 8 | eqeltrrid 2843 | . . 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 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 |