Theorem rtrclex

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

	Ref	Expression
Assertion	rtrclex	|- ( A e. _V <-> |^| { x | ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) } e. _V )

Proof

Step	Hyp	Ref	Expression
1		ssun1	|- A C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
2		coundir	|- ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) = ( ( A o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) u. ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) )
3		coundi	|- ( A o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) = ( ( A o. A ) u. ( A o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) )
4		cossxp	|- ( A o. A ) C_ ( dom A X. ran A )
5		ssun1	|- dom A C_ ( dom A u. ran A )
6		ssun2	|- ran A C_ ( dom A u. ran A )
7		xpss12	|- ( ( dom A C_ ( dom A u. ran A ) /\ ran A C_ ( dom A u. ran A ) ) -> ( dom A X. ran A ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
8	5 6 7	mp2an	|- ( dom A X. ran A ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
9	4 8	sstri	|- ( A o. A ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
10		cossxp	|- ( A o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) X. ran A )
11		dmxpss	|- dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) C_ ( dom A u. ran A )
12		xpss12	|- ( ( dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) C_ ( dom A u. ran A ) /\ ran A C_ ( dom A u. ran A ) ) -> ( dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) X. ran A ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
13	11 6 12	mp2an	|- ( dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) X. ran A ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
14	10 13	sstri	|- ( A o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
15	9 14	unssi	|- ( ( A o. A ) u. ( A o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
16	3 15	eqsstri	|- ( A o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
17		coundi	|- ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) = ( ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. A ) u. ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) )
18		cossxp	|- ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. A ) C_ ( dom A X. ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
19		rnxpss	|- ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) C_ ( dom A u. ran A )
20		xpss12	|- ( ( dom A C_ ( dom A u. ran A ) /\ ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) C_ ( dom A u. ran A ) ) -> ( dom A X. ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
21	5 19 20	mp2an	|- ( dom A X. ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
22	18 21	sstri	|- ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. A ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
23		xpidtr	|- ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
24	22 23	unssi	|- ( ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. A ) u. ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
25	17 24	eqsstri	|- ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
26	16 25	unssi	|- ( ( A o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) u. ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
27	2 26	eqsstri	|- ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
28		ssun2	|- ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
29	27 28	sstri	|- ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
30		dmun	|- dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) = ( dom A u. dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
31		dmxpid	|- dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) = ( dom A u. ran A )
32	31	uneq2i	|- ( dom A u. dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) = ( dom A u. ( dom A u. ran A ) )
33		ssequn1	|- ( dom A C_ ( dom A u. ran A ) <-> ( dom A u. ( dom A u. ran A ) ) = ( dom A u. ran A ) )
34	5 33	mpbi	|- ( dom A u. ( dom A u. ran A ) ) = ( dom A u. ran A )
35	30 32 34	3eqtri	|- dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) = ( dom A u. ran A )
36		rnun	|- ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) = ( ran A u. ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
37		rnxpid	|- ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) = ( dom A u. ran A )
38	37	uneq2i	|- ( ran A u. ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) = ( ran A u. ( dom A u. ran A ) )
39		ssequn1	|- ( ran A C_ ( dom A u. ran A ) <-> ( ran A u. ( dom A u. ran A ) ) = ( dom A u. ran A ) )
40	6 39	mpbi	|- ( ran A u. ( dom A u. ran A ) ) = ( dom A u. ran A )
41	36 38 40	3eqtri	|- ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) = ( dom A u. ran A )
42	35 41	uneq12i	|- ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) = ( ( dom A u. ran A ) u. ( dom A u. ran A ) )
43		unidm	|- ( ( dom A u. ran A ) u. ( dom A u. ran A ) ) = ( dom A u. ran A )
44	42 43	eqtri	|- ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) = ( dom A u. ran A )
45	44	reseq2i	|- ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) = ( _I |` ( dom A u. ran A ) )
46		idssxp	|- ( _I |` ( dom A u. ran A ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
47	45 46	eqsstri	|- ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
48	47 28	sstri	|- ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
49	29 48	pm3.2i	|- ( ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) )
50		rtrclexlem	|- ( A e. _V -> ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) e. _V )
51		id	|- ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) )
52	51 51	coeq12d	|- ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( x o. x ) = ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) )
53	52 51	sseq12d	|- ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( ( x o. x ) C_ x <-> ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) )
54		dmeq	|- ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> dom x = dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) )
55		rneq	|- ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ran x = ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) )
56	54 55	uneq12d	|- ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( dom x u. ran x ) = ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) )
57	56	reseq2d	|- ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( _I |` ( dom x u. ran x ) ) = ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) )
58	57 51	sseq12d	|- ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( ( _I |` ( dom x u. ran x ) ) C_ x <-> ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) )
59	53 58	anbi12d	|- ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) <-> ( ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) )
60	59	cleq2lem	|- ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) <-> ( A C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) ) )
61	60	biimprd	|- ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( ( A C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) -> ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) ) )
62	61	adantl	|- ( ( A e. _V /\ x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) -> ( ( A C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) -> ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) ) )
63	50 62	spcimedv	|- ( A e. _V -> ( ( A C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) -> E. x ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) ) )
64	1 49 63	mp2ani	|- ( A e. _V -> E. x ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) )
65		exsimpl	|- ( E. x ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) -> E. x A C_ x )
66		vex	|- x e. _V
67	66	ssex	|- ( A C_ x -> A e. _V )
68	67	exlimiv	|- ( E. x A C_ x -> A e. _V )
69	65 68	syl	|- ( E. x ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) -> A e. _V )
70	64 69	impbii	|- ( A e. _V <-> E. x ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) )
71		intexab	|- ( E. x ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) <-> |^| { x | ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) } e. _V )
72	70 71	bitri	|- ( A e. _V <-> |^| { x | ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) } e. _V )