rtrclexi

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

		Ref	Expression
	Hypothesis	rtrclexi.1	$⊢ A \in V$
	Assertion	rtrclexi	$⊢ ⋂ \{x \| (A \subseteq x \land (x \circ x \subseteq x \land {I ↾}_{(dom x \cup ran x)} \subseteq x))\} \in V$

Proof

Step	Hyp	Ref	Expression
1		rtrclexi.1	$⊢ A \in V$
2		ssun1	$⊢ A \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A))$
3		coundir	$⊢ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) = (A \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))) \cup (((dom A \cup ran A) \times (dom A \cup ran A)) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))$
4		coundi	$⊢ A \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) = (A \circ A) \cup (A \circ ((dom A \cup ran A) \times (dom A \cup ran A)))$
5		cossxp	$⊢ A \circ A \subseteq dom A \times ran A$
6		ssun1	$⊢ dom A \subseteq dom A \cup ran A$
7		ssun2	$⊢ ran A \subseteq dom A \cup ran A$
8		xpss12	$⊢ (dom A \subseteq dom A \cup ran A \land ran A \subseteq dom A \cup ran A) \to dom A \times ran A \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
9	6 7 8	mp2an	$⊢ dom A \times ran A \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
10	5 9	sstri	$⊢ A \circ A \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
11		cossxp	$⊢ A \circ ((dom A \cup ran A) \times (dom A \cup ran A)) \subseteq dom ((dom A \cup ran A) \times (dom A \cup ran A)) \times ran A$
12		dmxpss	$⊢ dom ((dom A \cup ran A) \times (dom A \cup ran A)) \subseteq dom A \cup ran A$
13		xpss12	$⊢ (dom ((dom A \cup ran A) \times (dom A \cup ran A)) \subseteq dom A \cup ran A \land ran A \subseteq dom A \cup ran A) \to dom ((dom A \cup ran A) \times (dom A \cup ran A)) \times ran A \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
14	12 7 13	mp2an	$⊢ dom ((dom A \cup ran A) \times (dom A \cup ran A)) \times ran A \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
15	11 14	sstri	$⊢ A \circ ((dom A \cup ran A) \times (dom A \cup ran A)) \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
16	10 15	unssi	$⊢ (A \circ A) \cup (A \circ ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
17	4 16	eqsstri	$⊢ A \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
18		coundi	$⊢ ((dom A \cup ran A) \times (dom A \cup ran A)) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) = (((dom A \cup ran A) \times (dom A \cup ran A)) \circ A) \cup (((dom A \cup ran A) \times (dom A \cup ran A)) \circ ((dom A \cup ran A) \times (dom A \cup ran A)))$
19		cossxp	$⊢ ((dom A \cup ran A) \times (dom A \cup ran A)) \circ A \subseteq dom A \times ran ((dom A \cup ran A) \times (dom A \cup ran A))$
20		rnxpss	$⊢ ran ((dom A \cup ran A) \times (dom A \cup ran A)) \subseteq dom A \cup ran A$
21		xpss12	$⊢ (dom A \subseteq dom A \cup ran A \land ran ((dom A \cup ran A) \times (dom A \cup ran A)) \subseteq dom A \cup ran A) \to dom A \times ran ((dom A \cup ran A) \times (dom A \cup ran A)) \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
22	6 20 21	mp2an	$⊢ dom A \times ran ((dom A \cup ran A) \times (dom A \cup ran A)) \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
23	19 22	sstri	$⊢ ((dom A \cup ran A) \times (dom A \cup ran A)) \circ A \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
24		xpidtr	$⊢ ((dom A \cup ran A) \times (dom A \cup ran A)) \circ ((dom A \cup ran A) \times (dom A \cup ran A)) \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
25	23 24	unssi	$⊢ (((dom A \cup ran A) \times (dom A \cup ran A)) \circ A) \cup (((dom A \cup ran A) \times (dom A \cup ran A)) \circ ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
26	18 25	eqsstri	$⊢ ((dom A \cup ran A) \times (dom A \cup ran A)) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
27	17 26	unssi	$⊢ (A \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))) \cup (((dom A \cup ran A) \times (dom A \cup ran A)) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))) \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
28	3 27	eqsstri	$⊢ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
29		ssun2	$⊢ (dom A \cup ran A) \times (dom A \cup ran A) \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A))$
30	28 29	sstri	$⊢ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A))$
31		dmun	$⊢ dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) = dom A \cup dom ((dom A \cup ran A) \times (dom A \cup ran A))$
32	6 12	unssi	$⊢ dom A \cup dom ((dom A \cup ran A) \times (dom A \cup ran A)) \subseteq dom A \cup ran A$
33	31 32	eqsstri	$⊢ dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq dom A \cup ran A$
34		rnun	$⊢ ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) = ran A \cup ran ((dom A \cup ran A) \times (dom A \cup ran A))$
35	7 20	unssi	$⊢ ran A \cup ran ((dom A \cup ran A) \times (dom A \cup ran A)) \subseteq dom A \cup ran A$
36	34 35	eqsstri	$⊢ ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq dom A \cup ran A$
37	33 36	unssi	$⊢ dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq dom A \cup ran A$
38		ssres2	$⊢ dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq dom A \cup ran A \to {I ↾}_{(dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))} \subseteq {I ↾}_{(dom A \cup ran A)}$
39	37 38	ax-mp	$⊢ {I ↾}_{(dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))} \subseteq {I ↾}_{(dom A \cup ran A)}$
40		idssxp	$⊢ {I ↾}_{(dom A \cup ran A)} \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
41	39 40	sstri	$⊢ {I ↾}_{(dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))} \subseteq (dom A \cup ran A) \times (dom A \cup ran A)$
42	41 29	sstri	$⊢ {I ↾}_{(dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))} \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A))$
43		id	$⊢ ((A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \land {I ↾}_{(dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))} \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \to ((A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \land {I ↾}_{(dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))} \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))$
44	30 42 43	mp2an	$⊢ ((A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \land {I ↾}_{(dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))} \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))$
45	1	elexi	$⊢ A \in V$
46	45	dmex	$⊢ dom A \in V$
47	45	rnex	$⊢ ran A \in V$
48	46 47	unex	$⊢ dom A \cup ran A \in V$
49	48 48	xpex	$⊢ (dom A \cup ran A) \times (dom A \cup ran A) \in V$
50	45 49	unex	$⊢ A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \in V$
51		id	$⊢ x = A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \to x = A \cup ((dom A \cup ran A) \times (dom A \cup ran A))$
52	51 51	coeq12d	$⊢ x = A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \to x \circ x = (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))$
53	52 51	sseq12d	$⊢ x = A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \to (x \circ x \subseteq x \leftrightarrow (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))$
54		dmeq	$⊢ x = A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \to dom x = dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))$
55		rneq	$⊢ x = A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \to ran x = ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))$
56	54 55	uneq12d	$⊢ x = A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \to dom x \cup ran x = dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))$
57	56	reseq2d	$⊢ x = A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \to {I ↾}_{(dom x \cup ran x)} = {I ↾}_{(dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))}$
58	57 51	sseq12d	$⊢ x = A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \to ({I ↾}_{(dom x \cup ran x)} \subseteq x \leftrightarrow {I ↾}_{(dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))} \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))$
59	53 58	anbi12d	$⊢ x = A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \to ((x \circ x \subseteq x \land {I ↾}_{(dom x \cup ran x)} \subseteq x) \leftrightarrow ((A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \land {I ↾}_{(dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))} \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))$
60	59	cleq2lem	$⊢ x = A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \to ((A \subseteq x \land (x \circ x \subseteq x \land {I ↾}_{(dom x \cup ran x)} \subseteq x)) \leftrightarrow (A \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \land ((A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \land {I ↾}_{(dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))} \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))))$
61	50 60	spcev	$⊢ (A \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \land ((A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \land {I ↾}_{(dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))} \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))) \to \exists x (A \subseteq x \land (x \circ x \subseteq x \land {I ↾}_{(dom x \cup ran x)} \subseteq x))$
62		intexab	$⊢ \exists x (A \subseteq x \land (x \circ x \subseteq x \land {I ↾}_{(dom x \cup ran x)} \subseteq x)) \leftrightarrow ⋂ \{x \| (A \subseteq x \land (x \circ x \subseteq x \land {I ↾}_{(dom x \cup ran x)} \subseteq x))\} \in V$
63	61 62	sylib	$⊢ (A \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \land ((A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \circ (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)) \land {I ↾}_{(dom (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))) \cup ran (A \cup ((dom A \cup ran A) \times (dom A \cup ran A))))} \subseteq A \cup ((dom A \cup ran A) \times (dom A \cup ran A)))) \to ⋂ \{x \| (A \subseteq x \land (x \circ x \subseteq x \land {I ↾}_{(dom x \cup ran x)} \subseteq x))\} \in V$
64	2 44 63	mp2an	$⊢ ⋂ \{x \| (A \subseteq x \land (x \circ x \subseteq x \land {I ↾}_{(dom x \cup ran x)} \subseteq x))\} \in V$

Metamath Proof Explorer

Theorem rtrclexi

Proof