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 36226

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 5651	. . . . . . 7
2		cnvnonrel 36188	. . . . . . . . . . . . . . . 16 $\$
3		cnv0 5238	. . . . . . . . . . . . . . . 16
4	2, 3	eqtr4i 2475	. . . . . . . . . . . . . . 15 $\$
5	4	dmeqi 5035	. . . . . . . . . . . . . 14 $\$
6		df-rn 4844	. . . . . . . . . . . . . 14 $\$ $\$
7		df-rn 4844	. . . . . . . . . . . . . 14
8	5, 6, 7	3eqtr4i 2482	. . . . . . . . . . . . 13 $\$
9		0ss 3762	. . . . . . . . . . . . . 14
10		rnss 5062	. . . . . . . . . . . . . 14
11	9, 10	ax-mp 5	. . . . . . . . . . . . 13
12	8, 11	eqsstri 3461	. . . . . . . . . . . 12 $\$
13		ssequn2 3606	. . . . . . . . . . . 12 $\$ $\$
14	12, 13	mpbi 212	. . . . . . . . . . 11 $\$
15		rnun 5243	. . . . . . . . . . 11 $\$ $\$
16		dfdm4 5026	. . . . . . . . . . 11
17	14, 15, 16	3eqtr4ri 2483	. . . . . . . . . 10 $\$
18	4	rneqi 5060	. . . . . . . . . . . . . 14 $\$
19		dfdm4 5026	. . . . . . . . . . . . . 14 $\$ $\$
20		dfdm4 5026	. . . . . . . . . . . . . 14
21	18, 19, 20	3eqtr4i 2482	. . . . . . . . . . . . 13 $\$
22		dmss 5033	. . . . . . . . . . . . . 14
23	9, 22	ax-mp 5	. . . . . . . . . . . . 13
24	21, 23	eqsstri 3461	. . . . . . . . . . . 12 $\$
25		ssequn2 3606	. . . . . . . . . . . 12 $\$ $\$
26	24, 25	mpbi 212	. . . . . . . . . . 11 $\$
27		dmun 5040	. . . . . . . . . . 11 $\$ $\$
28		df-rn 4844	. . . . . . . . . . 11
29	26, 27, 28	3eqtr4ri 2483	. . . . . . . . . 10 $\$
30	17, 29	uneq12i 3585	. . . . . . . . 9 $\$ $\$
31	30	equncomi 3579	. . . . . . . 8 $\$ $\$
32	31	reseq2i 5101	. . . . . . 7 $\$ $\$
33	1, 32	eqtr2i 2473	. . . . . 6 $\$ $\$
34		cnvss 5006	. . . . . 6
35	33, 34	syl5eqss 3475	. . . . 5 $\$ $\$
36		ssun1 3596	. . . . 5 $\$
37	35, 36	syl6ss 3443	. . . 4 $\$ $\$ $\$
38		dmeq 5034	. . . . . . 7 $\$ $\$
39		rneq 5059	. . . . . . 7 $\$ $\$
40	38, 39	uneq12d 3588	. . . . . 6 $\$ $\$ $\$
41	40	reseq2d 5104	. . . . 5 $\$ $\$ $\$
42		id 22	. . . . 5 $\$ $\$
43	41, 42	sseq12d 3460	. . . 4 $\$ $\$ $\$ $\$
44	37, 43	syl5ibr 225	. . 3 $\$
45	44	adantl 468	. 2 $/\$ $\$
46		cnvresid 5651	. . . . . 6
47		dfdm4 5026	. . . . . . . . 9
48		df-rn 4844	. . . . . . . . 9
49	47, 48	uneq12i 3585	. . . . . . . 8
50	49	equncomi 3579	. . . . . . 7
51	50	reseq2i 5101	. . . . . 6
52	46, 51	eqtr2i 2473	. . . . 5
53		cnvss 5006	. . . . 5
54	52, 53	syl5eqss 3475	. . . 4
55		dmeq 5034	. . . . . . 7
56		rneq 5059	. . . . . . 7
57	55, 56	uneq12d 3588	. . . . . 6
58	57	reseq2d 5104	. . . . 5
59		id 22	. . . . 5
60	58, 59	sseq12d 3460	. . . 4
61	54, 60	syl5ibr 225	. . 3
62	61	adantl 468	. 2 $/\$
63		dmeq 5034	. . . . 5
64		rneq 5059	. . . . 5
65	63, 64	uneq12d 3588	. . . 4
66	65	reseq2d 5104	. . 3
67		id 22	. . 3
68	66, 67	sseq12d 3460	. 2
69		ssun1 3596	. . 3
70	69	a1i 11	. 2
71		dmexg 6721	. . . . 5
72		rnexg 6722	. . . . 5
73		unexg 6589	. . . . 5 $/\$
74	71, 72, 73	syl2anc 666	. . . 4
75	74	resiexd 6129	. . 3
76		unexg 6589	. . 3 $/\$
77	75, 76	mpdan 673	. 2
78		dmun 5040	. . . . . 6
79		ssun1 3596	. . . . . . 7
80		dmresi 5159	. . . . . . . 8
81	80	eqimssi 3485	. . . . . . 7
82	79, 81	unssi 3608	. . . . . 6
83	78, 82	eqsstri 3461	. . . . 5
84		rnun 5243	. . . . . 6
85		ssun2 3597	. . . . . . 7
86		rnresi 5180	. . . . . . . 8
87	86	eqimssi 3485	. . . . . . 7
88	85, 87	unssi 3608	. . . . . 6
89	84, 88	eqsstri 3461	. . . . 5
90	83, 89	pm3.2i 457	. . . 4 $/\$
91		unss 3607	. . . . 5 $/\$
92		ssres2 5130	. . . . 5
93	91, 92	sylbi 199	. . . 4 $/\$
94		ssun4 3599	. . . 4
95	90, 93, 94	mp2b 10	. . 3
96	95	a1i 11	. 2
97	45, 62, 68, 70, 77, 96	clcnvlem 36224	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 371

wceq 1443

wcel 1886

cab 2436

cvv 3044 $\$ cdif 3400

cun 3401

wss 3403

c0 3730

cint 4233

cid 4743

ccnv 4832

cdm 4833

crn 4834

cres 4835

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-ral 2741 df-rex 2742 df-reu 2743 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-id 4748 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-1st 6790 df-2nd 6791

This theorem is referenced by: (None)

W3C validator