cnvexg - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > cnvexg		GIF version

Theorem cnvexg 5269

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 5109	. . 3 ⊢ Rel ^◡𝐴
2		relssdmrn 5252	. . 3 ⊢ (Rel ^◡𝐴 → ^◡𝐴 ⊆ (dom ^◡𝐴 × ran ^◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ^◡𝐴 ⊆ (dom ^◡𝐴 × ran ^◡𝐴)
4		df-rn 4731	. . . 4 ⊢ ran 𝐴 = dom ^◡𝐴
5		rnexg 4992	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2317	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ^◡𝐴 ∈ V)
7		dfdm4 4918	. . . 4 ⊢ dom 𝐴 = ran ^◡𝐴
8		dmexg 4991	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2317	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ^◡𝐴 ∈ V)
10		xpexg 4835	. . 3 ⊢ ((dom ^◡𝐴 ∈ V ∧ ran ^◡𝐴 ∈ V) → (dom ^◡𝐴 × ran ^◡𝐴) ∈ V)
11	6, 9, 10	syl2anc 411	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ^◡𝐴 × ran ^◡𝐴) ∈ V)
12		ssexg 4223	. 2 ⊢ ((^◡𝐴 ⊆ (dom ^◡𝐴 × ran ^◡𝐴) ∧ (dom ^◡𝐴 × ran ^◡𝐴) ∈ V) → ^◡𝐴 ∈ V)
13	3, 11, 12	sylancr 414	1 ⊢ (𝐴 ∈ 𝑉 → ^◡𝐴 ∈ V)

Colors of variables: wff set class

Syntax hints: → wi 4 ∈ wcel 2200 Vcvv 2799 ⊆ wss 3197 × cxp 4718 ^◡ccnv 4719 dom cdm 4720 ran crn 4721 Rel wrel 4725

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-sep 4202 ax-pow 4259 ax-pr 4294 ax-un 4525

This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ral 2513 df-rex 2514 df-v 2801 df-un 3201 df-in 3203 df-ss 3210 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-br 4084 df-opab 4146 df-xp 4726 df-rel 4727 df-cnv 4728 df-dm 4730 df-rn 4731

This theorem is referenced by: cnvex 5270 relcnvexb 5271 cofunex2g 6264 cnvf1o 6382 brtpos2 6408 tposexg 6415 cnven 6974 cnvct 6975 fopwdom 7010 relcnvfi 7124 ennnfonelemim 13016 xpsval 13406 isunitd 14091 znval 14621 znle 14622 znbaslemnn 14624 znleval 14638 pw1nct 16482