cnvrcl0 - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cnvrcl0		Structured version Visualization version Unicode version

Theorem cnvrcl0 36303

Description: The converse of the reflexive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)

**Assertion**
Ref	Expression
cnvrcl0	$/\$ $/\$

Distinct variable groups:

**Proof of Theorem cnvrcl0**
Step	Hyp	Ref	Expression
1		cnvresid 5663	. . . . . . 7
2		cnvnonrel 36265	. . . . . . . . . . . . . . . 16 $\$
3		cnv0 5245	. . . . . . . . . . . . . . . 16
4	2, 3	eqtr4i 2496	. . . . . . . . . . . . . . 15 $\$
5	4	dmeqi 5041	. . . . . . . . . . . . . 14 $\$
6		df-rn 4850	. . . . . . . . . . . . . 14 $\$ $\$
7		df-rn 4850	. . . . . . . . . . . . . 14
8	5, 6, 7	3eqtr4i 2503	. . . . . . . . . . . . 13 $\$
9		0ss 3766	. . . . . . . . . . . . . 14
10		rnss 5069	. . . . . . . . . . . . . 14
11	9, 10	ax-mp 5	. . . . . . . . . . . . 13
12	8, 11	eqsstri 3448	. . . . . . . . . . . 12 $\$
13		ssequn2 3598	. . . . . . . . . . . 12 $\$ $\$
14	12, 13	mpbi 213	. . . . . . . . . . 11 $\$
15		rnun 5250	. . . . . . . . . . 11 $\$ $\$
16		dfdm4 5032	. . . . . . . . . . 11
17	14, 15, 16	3eqtr4ri 2504	. . . . . . . . . 10 $\$
18	4	rneqi 5067	. . . . . . . . . . . . . 14 $\$
19		dfdm4 5032	. . . . . . . . . . . . . 14 $\$ $\$
20		dfdm4 5032	. . . . . . . . . . . . . 14
21	18, 19, 20	3eqtr4i 2503	. . . . . . . . . . . . 13 $\$
22		dmss 5039	. . . . . . . . . . . . . 14
23	9, 22	ax-mp 5	. . . . . . . . . . . . 13
24	21, 23	eqsstri 3448	. . . . . . . . . . . 12 $\$
25		ssequn2 3598	. . . . . . . . . . . 12 $\$ $\$
26	24, 25	mpbi 213	. . . . . . . . . . 11 $\$
27		dmun 5047	. . . . . . . . . . 11 $\$ $\$
28		df-rn 4850	. . . . . . . . . . 11
29	26, 27, 28	3eqtr4ri 2504	. . . . . . . . . 10 $\$
30	17, 29	uneq12i 3577	. . . . . . . . 9 $\$ $\$
31	30	equncomi 3571	. . . . . . . 8 $\$ $\$
32	31	reseq2i 5108	. . . . . . 7 $\$ $\$
33	1, 32	eqtr2i 2494	. . . . . 6 $\$ $\$
34		cnvss 5012	. . . . . 6
35	33, 34	syl5eqss 3462	. . . . 5 $\$ $\$
36		ssun1 3588	. . . . 5 $\$
37	35, 36	syl6ss 3430	. . . 4 $\$ $\$ $\$
38		dmeq 5040	. . . . . . 7 $\$ $\$
39		rneq 5066	. . . . . . 7 $\$ $\$
40	38, 39	uneq12d 3580	. . . . . 6 $\$ $\$ $\$
41	40	reseq2d 5111	. . . . 5 $\$ $\$ $\$
42		id 22	. . . . 5 $\$ $\$
43	41, 42	sseq12d 3447	. . . 4 $\$ $\$ $\$ $\$
44	37, 43	syl5ibr 229	. . 3 $\$
45	44	adantl 473	. 2 $/\$ $\$
46		cnvresid 5663	. . . . . 6
47		dfdm4 5032	. . . . . . . . 9
48		df-rn 4850	. . . . . . . . 9
49	47, 48	uneq12i 3577	. . . . . . . 8
50	49	equncomi 3571	. . . . . . 7
51	50	reseq2i 5108	. . . . . 6
52	46, 51	eqtr2i 2494	. . . . 5
53		cnvss 5012	. . . . 5
54	52, 53	syl5eqss 3462	. . . 4
55		dmeq 5040	. . . . . . 7
56		rneq 5066	. . . . . . 7
57	55, 56	uneq12d 3580	. . . . . 6
58	57	reseq2d 5111	. . . . 5
59		id 22	. . . . 5
60	58, 59	sseq12d 3447	. . . 4
61	54, 60	syl5ibr 229	. . 3
62	61	adantl 473	. 2 $/\$
63		dmeq 5040	. . . . 5
64		rneq 5066	. . . . 5
65	63, 64	uneq12d 3580	. . . 4
66	65	reseq2d 5111	. . 3
67		id 22	. . 3
68	66, 67	sseq12d 3447	. 2
69		ssun1 3588	. . 3
70	69	a1i 11	. 2
71		dmexg 6743	. . . . 5
72		rnexg 6744	. . . . 5
73		unexg 6611	. . . . 5 $/\$
74	71, 72, 73	syl2anc 673	. . . 4
75	74	resiexd 6147	. . 3
76		unexg 6611	. . 3 $/\$
77	75, 76	mpdan 681	. 2
78		dmun 5047	. . . . . 6
79		ssun1 3588	. . . . . . 7
80		dmresi 5166	. . . . . . . 8
81	80	eqimssi 3472	. . . . . . 7
82	79, 81	unssi 3600	. . . . . 6
83	78, 82	eqsstri 3448	. . . . 5
84		rnun 5250	. . . . . 6
85		ssun2 3589	. . . . . . 7
86		rnresi 5187	. . . . . . . 8
87	86	eqimssi 3472	. . . . . . 7
88	85, 87	unssi 3600	. . . . . 6
89	84, 88	eqsstri 3448	. . . . 5
90	83, 89	pm3.2i 462	. . . 4 $/\$
91		unss 3599	. . . . 5 $/\$
92		ssres2 5137	. . . . 5
93	91, 92	sylbi 200	. . . 4 $/\$
94		ssun4 3591	. . . 4
95	90, 93, 94	mp2b 10	. . 3
96	95	a1i 11	. 2
97	45, 62, 68, 70, 77, 96	clcnvlem 36301	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 376

wceq 1452

wcel 1904

cab 2457

cvv 3031 $\$ cdif 3387

cun 3388

wss 3390

c0 3722

cint 4226

cid 4749

ccnv 4838

cdm 4839

crn 4840

cres 4841

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-reu 2763 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-id 4754 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-1st 6812 df-2nd 6813

This theorem is referenced by: (None)

W3C validator