cnvexg - Metamath Proof Explorer

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

Theorem cnvexg 7485

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**
Step	Hyp	Ref	Expression
1		relcnv 5843	. . 3 ⊢ Rel ^◡𝐴
2		relssdmrn 5996	. . 3 ⊢ (Rel ^◡𝐴 → ^◡𝐴 ⊆ (dom ^◡𝐴 × ran ^◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ^◡𝐴 ⊆ (dom ^◡𝐴 × ran ^◡𝐴)
4		df-rn 5454	. . . 4 ⊢ ran 𝐴 = dom ^◡𝐴
5		rnexg 7470	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	syl5eqelr 2888	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ^◡𝐴 ∈ V)
7		dfdm4 5650	. . . 4 ⊢ dom 𝐴 = ran ^◡𝐴
8		dmexg 7469	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	syl5eqelr 2888	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ^◡𝐴 ∈ V)
10	6, 9	xpexd 7331	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ^◡𝐴 × ran ^◡𝐴) ∈ V)
11		ssexg 5118	. 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 2081 Vcvv 3437 ⊆ wss 3859 × cxp 5441 ^◡ccnv 5442 dom cdm 5443 ran crn 5444 Rel wrel 5448

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-xp 5449 df-rel 5450 df-cnv 5451 df-dm 5453 df-rn 5454

This theorem is referenced by: cnvex 7486 relcnvexb 7487 cofunex2g 7507 tposexg 7757 cnven 8433 cnvct 8434 fopwdom 8472 domssex2 8524 domssex 8525 cnvfi 8652 mapfienlem2 8715 wemapwe 9006 hasheqf1oi 13562 brtrclfvcnv 14198 brcnvtrclfvcnv 14199 relexpcnv 14228 relexpnnrn 14238 relexpaddg 14246 imasle 16625 cnvps 17651 gsumvalx 17709 symginv 18261 tposmap 20750 metustel 22843 metustss 22844 metustfbas 22850 metuel2 22858 psmetutop 22860 restmetu 22863 itg2gt0 24044 nlfnval 29349 fnpreimac 30106 ffsrn 30153 tocycfv 30398 eulerpartlemgs2 31255 orvcval 31332 coinfliprv 31357 cossex 35195 cosscnvex 35196 cnvelrels 35266 lkrval 35755 pw2f1o2val 39121 lmhmlnmsplit 39172 cnvcnvintabd 39445 clrellem 39467 relexpaddss 39548 cnvtrclfv 39554 rntrclfvRP 39561 xpexb 40325 sge0f1o 42206 smfco 42619