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 36240

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 3599	. 2
2		coundir 5340	. . . . 5
3		coundi 5339	. . . . . . 7
4		cossxp 5361	. . . . . . . . 9
5		ssun1 3599	. . . . . . . . . 10
6		ssun2 3600	. . . . . . . . . 10
7		xpss12 4943	. . . . . . . . . 10 $/\$
8	5, 6, 7	mp2an 679	. . . . . . . . 9
9	4, 8	sstri 3443	. . . . . . . 8
10		cossxp 5361	. . . . . . . . 9
11		dmxpss 5271	. . . . . . . . . 10
12		xpss12 4943	. . . . . . . . . 10 $/\$
13	11, 6, 12	mp2an 679	. . . . . . . . 9
14	10, 13	sstri 3443	. . . . . . . 8
15	9, 14	unssi 3611	. . . . . . 7
16	3, 15	eqsstri 3464	. . . . . 6
17		coundi 5339	. . . . . . 7
18		cossxp 5361	. . . . . . . . 9
19		rnxpss 5272	. . . . . . . . . 10
20		xpss12 4943	. . . . . . . . . 10 $/\$
21	5, 19, 20	mp2an 679	. . . . . . . . 9
22	18, 21	sstri 3443	. . . . . . . 8
23		xpidtr 5225	. . . . . . . 8
24	22, 23	unssi 3611	. . . . . . 7
25	17, 24	eqsstri 3464	. . . . . 6
26	16, 25	unssi 3611	. . . . 5
27	2, 26	eqsstri 3464	. . . 4
28		ssun2 3600	. . . 4
29	27, 28	sstri 3443	. . 3
30		dmun 5044	. . . . . . . 8
31	5, 11	unssi 3611	. . . . . . . 8
32	30, 31	eqsstri 3464	. . . . . . 7
33		rnun 5247	. . . . . . . 8
34	6, 19	unssi 3611	. . . . . . . 8
35	33, 34	eqsstri 3464	. . . . . . 7
36	32, 35	unssi 3611	. . . . . 6
37		ssres2 5134	. . . . . 6
38	36, 37	ax-mp 5	. . . . 5
39		relres 5135	. . . . . . 7
40		relssdmrn 5359	. . . . . . 7
41	39, 40	ax-mp 5	. . . . . 6
42		dmresi 5163	. . . . . . 7
43		rnresi 5184	. . . . . . 7
44	42, 43	xpeq12i 4859	. . . . . 6
45	41, 44	sseqtri 3466	. . . . 5
46	38, 45	sstri 3443	. . . 4
47	46, 28	sstri 3443	. . 3
48		id 22	. . 3 $/\$ $/\$
49	29, 47, 48	mp2an 679	. 2 $/\$
50		rtrclexi.1	. . . . . 6
51	50	elexi 3057	. . . . 5
52	51	dmex 6731	. . . . . . 7
53	51	rnex 6732	. . . . . . 7
54	52, 53	unex 6594	. . . . . 6
55	54, 54	xpex 6600	. . . . 5
56	51, 55	unex 6594	. . . 4
57		id 22	. . . . . . . 8
58	57, 57	coeq12d 5002	. . . . . . 7
59	58, 57	sseq12d 3463	. . . . . 6
60		dmeq 5038	. . . . . . . . 9
61		rneq 5063	. . . . . . . . 9
62	60, 61	uneq12d 3591	. . . . . . . 8
63	62	reseq2d 5108	. . . . . . 7
64	63, 57	sseq12d 3463	. . . . . 6
65	59, 64	anbi12d 718	. . . . 5 $/\$ $/\$
66	65	cleq2lem 36226	. . . 4 $/\$ $/\$ $/\$ $/\$
67	56, 66	spcev 3143	. . 3 $/\$ $/\$ $/\$ $/\$
68		intexab 4564	. . 3 $/\$ $/\$ $/\$ $/\$
69	67, 68	sylib 200	. 2 $/\$ $/\$ $/\$ $/\$
70	1, 49, 69	mp2an 679	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 371

wceq 1446

wex 1665

wcel 1889

cab 2439

cvv 3047

cun 3404

wss 3406

cint 4237

cid 4747

cxp 4835

cdm 4837

crn 4838

cres 4839

ccom 4841

wrel 4842

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-rab 2748 df-v 3049 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-op 3977 df-uni 4202 df-int 4238 df-br 4406 df-opab 4465 df-id 4752 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850

This theorem is referenced by: dfrtrcl5 36248

W3C validator