rtrclexi - Mathbox for Richard Penner

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

Theorem rtrclexi 36299

Description: The reflexive-transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.)

**Hypothesis**
Ref	Expression
rtrclexi.1

**Assertion**
Ref	Expression
rtrclexi	$/\$ $/\$

Distinct variable group:

Allowed substitution hint:

(

)

**Proof of Theorem rtrclexi**
Step	Hyp	Ref	Expression
1		ssun1 3588	. 2
2		coundir 5344	. . . . 5
3		coundi 5343	. . . . . . 7
4		cossxp 5365	. . . . . . . . 9
5		ssun1 3588	. . . . . . . . . 10
6		ssun2 3589	. . . . . . . . . 10
7		xpss12 4945	. . . . . . . . . 10 $/\$
8	5, 6, 7	mp2an 686	. . . . . . . . 9
9	4, 8	sstri 3427	. . . . . . . 8
10		cossxp 5365	. . . . . . . . 9
11		dmxpss 5274	. . . . . . . . . 10
12		xpss12 4945	. . . . . . . . . 10 $/\$
13	11, 6, 12	mp2an 686	. . . . . . . . 9
14	10, 13	sstri 3427	. . . . . . . 8
15	9, 14	unssi 3600	. . . . . . 7
16	3, 15	eqsstri 3448	. . . . . 6
17		coundi 5343	. . . . . . 7
18		cossxp 5365	. . . . . . . . 9
19		rnxpss 5275	. . . . . . . . . 10
20		xpss12 4945	. . . . . . . . . 10 $/\$
21	5, 19, 20	mp2an 686	. . . . . . . . 9
22	18, 21	sstri 3427	. . . . . . . 8
23		xpidtr 5228	. . . . . . . 8
24	22, 23	unssi 3600	. . . . . . 7
25	17, 24	eqsstri 3448	. . . . . 6
26	16, 25	unssi 3600	. . . . 5
27	2, 26	eqsstri 3448	. . . 4
28		ssun2 3589	. . . 4
29	27, 28	sstri 3427	. . 3
30		dmun 5047	. . . . . . . 8
31	5, 11	unssi 3600	. . . . . . . 8
32	30, 31	eqsstri 3448	. . . . . . 7
33		rnun 5250	. . . . . . . 8
34	6, 19	unssi 3600	. . . . . . . 8
35	33, 34	eqsstri 3448	. . . . . . 7
36	32, 35	unssi 3600	. . . . . 6
37		ssres2 5137	. . . . . 6
38	36, 37	ax-mp 5	. . . . 5
39		relres 5138	. . . . . . 7
40		relssdmrn 5363	. . . . . . 7
41	39, 40	ax-mp 5	. . . . . 6
42		dmresi 5166	. . . . . . 7
43		rnresi 5187	. . . . . . 7
44	42, 43	xpeq12i 4861	. . . . . 6
45	41, 44	sseqtri 3450	. . . . 5
46	38, 45	sstri 3427	. . . 4
47	46, 28	sstri 3427	. . 3
48		id 22	. . 3 $/\$ $/\$
49	29, 47, 48	mp2an 686	. 2 $/\$
50		rtrclexi.1	. . . . . 6
51	50	elexi 3041	. . . . 5
52	51	dmex 6745	. . . . . . 7
53	51	rnex 6746	. . . . . . 7
54	52, 53	unex 6608	. . . . . 6
55	54, 54	xpex 6614	. . . . 5
56	51, 55	unex 6608	. . . 4
57		id 22	. . . . . . . 8
58	57, 57	coeq12d 5004	. . . . . . 7
59	58, 57	sseq12d 3447	. . . . . 6
60		dmeq 5040	. . . . . . . . 9
61		rneq 5066	. . . . . . . . 9
62	60, 61	uneq12d 3580	. . . . . . . 8
63	62	reseq2d 5111	. . . . . . 7
64	63, 57	sseq12d 3447	. . . . . 6
65	59, 64	anbi12d 725	. . . . 5 $/\$ $/\$
66	65	cleq2lem 36285	. . . 4 $/\$ $/\$ $/\$ $/\$
67	56, 66	spcev 3127	. . 3 $/\$ $/\$ $/\$ $/\$
68		intexab 4559	. . 3 $/\$ $/\$ $/\$ $/\$
69	67, 68	sylib 201	. 2 $/\$ $/\$ $/\$ $/\$
70	1, 49, 69	mp2an 686	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 376

wceq 1452

wex 1671

wcel 1904

cab 2457

cvv 3031

cun 3388

wss 3390

cint 4226

cid 4749

cxp 4837

cdm 4839

crn 4840

cres 4841

ccom 4843

wrel 4844

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-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-rab 2765 df-v 3033 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-br 4396 df-opab 4455 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

This theorem is referenced by: dfrtrcl5 36307

W3C validator