dfrtrcl5

Description: Definition of reflexive-transitive closure as a standard closure. (Contributed by RP, 1-Nov-2020)

		Ref	Expression
	Assertion	dfrtrcl5	$⊢ t* = (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land ({I ↾}_{(dom y \cup ran y)} \subseteq y \land y \circ y \subseteq y))\})$

Proof

Step	Hyp	Ref	Expression
1		df-rtrcl	$⊢ t* = (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\})$
2		ancom	$⊢ ({I ↾}_{(dom y \cup ran y)} \subseteq y \land y \circ y \subseteq y) \leftrightarrow (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y)$
3	2	anbi2i	$⊢ (x \subseteq y \land ({I ↾}_{(dom y \cup ran y)} \subseteq y \land y \circ y \subseteq y)) \leftrightarrow (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))$
4	3	abbii	$⊢ \{y \| (x \subseteq y \land ({I ↾}_{(dom y \cup ran y)} \subseteq y \land y \circ y \subseteq y))\} = \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\}$
5	4	inteqi	$⊢ ⋂ \{y \| (x \subseteq y \land ({I ↾}_{(dom y \cup ran y)} \subseteq y \land y \circ y \subseteq y))\} = ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\}$
6	5	mpteq2i	$⊢ (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land ({I ↾}_{(dom y \cup ran y)} \subseteq y \land y \circ y \subseteq y))\}) = (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\})$
7		vex	$⊢ x \in V$
8	7	rtrclexi	$⊢ ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \in V$
9	8	a1i	$⊢ x \in V \to ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \in V$
10		dmexg	$⊢ x \in V \to dom x \in V$
11		rnexg	$⊢ x \in V \to ran x \in V$
12		unexg	$⊢ (dom x \in V \land ran x \in V) \to dom x \cup ran x \in V$
13	10 11 12	syl2anc	$⊢ x \in V \to dom x \cup ran x \in V$
14		resiexg	$⊢ dom x \cup ran x \in V \to {I ↾}_{(dom x \cup ran x)} \in V$
15	7 13 14	mp2b	$⊢ {I ↾}_{(dom x \cup ran x)} \in V$
16	7 15	unex	$⊢ x \cup ({I ↾}_{(dom x \cup ran x)}) \in V$
17	16	trclexi	$⊢ ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \in V$
18	17	a1i	$⊢ x \in V \to ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \in V$
19		simpr	$⊢ (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z) \to z \circ z \subseteq z$
20	19	cotrintab	$⊢ ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \circ ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \subseteq ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\}$
21	20	a1i	$⊢ x \in V \to ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \circ ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \subseteq ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\}$
22	7	dmex	$⊢ dom x \in V$
23	7	rnex	$⊢ ran x \in V$
24	12	resiexd	$⊢ (dom x \in V \land ran x \in V) \to {I ↾}_{(dom x \cup ran x)} \in V$
25	22 23 24	mp2an	$⊢ {I ↾}_{(dom x \cup ran x)} \in V$
26	7 25	unex	$⊢ x \cup ({I ↾}_{(dom x \cup ran x)}) \in V$
27		dmtrcl	$⊢ x \cup ({I ↾}_{(dom x \cup ran x)}) \in V \to dom ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} = dom (x \cup ({I ↾}_{(dom x \cup ran x)}))$
28	26 27	ax-mp	$⊢ dom ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} = dom (x \cup ({I ↾}_{(dom x \cup ran x)}))$
29		dmun	$⊢ dom (x \cup ({I ↾}_{(dom x \cup ran x)})) = dom x \cup dom ({I ↾}_{(dom x \cup ran x)})$
30		dmresi	$⊢ dom ({I ↾}_{(dom x \cup ran x)}) = dom x \cup ran x$
31	30	uneq2i	$⊢ dom x \cup dom ({I ↾}_{(dom x \cup ran x)}) = dom x \cup (dom x \cup ran x)$
32		ssun1	$⊢ dom x \subseteq dom x \cup ran x$
33		ssequn1	$⊢ dom x \subseteq dom x \cup ran x \leftrightarrow dom x \cup (dom x \cup ran x) = dom x \cup ran x$
34	32 33	mpbi	$⊢ dom x \cup (dom x \cup ran x) = dom x \cup ran x$
35	29 31 34	3eqtri	$⊢ dom (x \cup ({I ↾}_{(dom x \cup ran x)})) = dom x \cup ran x$
36	28 35	eqtri	$⊢ dom ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} = dom x \cup ran x$
37		rntrcl	$⊢ x \cup ({I ↾}_{(dom x \cup ran x)}) \in V \to ran ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} = ran (x \cup ({I ↾}_{(dom x \cup ran x)}))$
38	26 37	ax-mp	$⊢ ran ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} = ran (x \cup ({I ↾}_{(dom x \cup ran x)}))$
39		rnun	$⊢ ran (x \cup ({I ↾}_{(dom x \cup ran x)})) = ran x \cup ran ({I ↾}_{(dom x \cup ran x)})$
40		rnresi	$⊢ ran ({I ↾}_{(dom x \cup ran x)}) = dom x \cup ran x$
41	40	uneq2i	$⊢ ran x \cup ran ({I ↾}_{(dom x \cup ran x)}) = ran x \cup (dom x \cup ran x)$
42		ssun2	$⊢ ran x \subseteq dom x \cup ran x$
43		ssequn1	$⊢ ran x \subseteq dom x \cup ran x \leftrightarrow ran x \cup (dom x \cup ran x) = dom x \cup ran x$
44	42 43	mpbi	$⊢ ran x \cup (dom x \cup ran x) = dom x \cup ran x$
45	39 41 44	3eqtri	$⊢ ran (x \cup ({I ↾}_{(dom x \cup ran x)})) = dom x \cup ran x$
46	38 45	eqtri	$⊢ ran ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} = dom x \cup ran x$
47	36 46	uneq12i	$⊢ dom ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \cup ran ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} = (dom x \cup ran x) \cup (dom x \cup ran x)$
48		unidm	$⊢ (dom x \cup ran x) \cup (dom x \cup ran x) = dom x \cup ran x$
49	47 48	eqtri	$⊢ dom ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \cup ran ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} = dom x \cup ran x$
50	49	reseq2i	$⊢ {I ↾}_{(dom ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \cup ran ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\})} = {I ↾}_{(dom x \cup ran x)}$
51		ssun2	$⊢ {I ↾}_{(dom x \cup ran x)} \subseteq x \cup ({I ↾}_{(dom x \cup ran x)})$
52		ssmin	$⊢ x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\}$
53	51 52	sstri	$⊢ {I ↾}_{(dom x \cup ran x)} \subseteq ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\}$
54	50 53	eqsstri	$⊢ {I ↾}_{(dom ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \cup ran ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\})} \subseteq ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\}$
55	54	a1i	$⊢ x \in V \to {I ↾}_{(dom ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \cup ran ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\})} \subseteq ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\}$
56		simprl	$⊢ (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y)) \to y \circ y \subseteq y$
57	56	cotrintab	$⊢ ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \circ ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \subseteq ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\}$
58	57	a1i	$⊢ x \in V \to ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \circ ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \subseteq ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\}$
59		id	$⊢ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \to y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\}$
60	59 59	coeq12d	$⊢ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \to y \circ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \circ ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\}$
61	60 59	sseq12d	$⊢ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \to (y \circ y \subseteq y \leftrightarrow ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \circ ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \subseteq ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\})$
62		dmeq	$⊢ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \to dom y = dom ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\}$
63		rneq	$⊢ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \to ran y = ran ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\}$
64	62 63	uneq12d	$⊢ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \to dom y \cup ran y = dom ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \cup ran ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\}$
65	64	reseq2d	$⊢ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \to {I ↾}_{(dom y \cup ran y)} = {I ↾}_{(dom ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \cup ran ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\})}$
66	65 59	sseq12d	$⊢ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \to ({I ↾}_{(dom y \cup ran y)} \subseteq y \leftrightarrow {I ↾}_{(dom ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} \cup ran ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\})} \subseteq ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\})$
67		id	$⊢ z = ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \to z = ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\}$
68	67 67	coeq12d	$⊢ z = ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \to z \circ z = ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \circ ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\}$
69	68 67	sseq12d	$⊢ z = ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \to (z \circ z \subseteq z \leftrightarrow ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \circ ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \subseteq ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\})$
70	9 18 21 55 58 61 66 69	mptrcllem	$⊢ (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land (y \circ y \subseteq y \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\}) = (x \in V ⟼ ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\})$
71		df-3an	$⊢ ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z) \leftrightarrow (({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z) \land z \circ z \subseteq z)$
72		ancom	$⊢ ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z) \leftrightarrow (x \subseteq z \land {I ↾}_{(dom x \cup ran x)} \subseteq z)$
73		unss	$⊢ (x \subseteq z \land {I ↾}_{(dom x \cup ran x)} \subseteq z) \leftrightarrow x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z$
74	72 73	bitri	$⊢ ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z) \leftrightarrow x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z$
75	74	anbi1i	$⊢ (({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z) \land z \circ z \subseteq z) \leftrightarrow (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)$
76	71 75	bitr2i	$⊢ (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z) \leftrightarrow ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)$
77	76	abbii	$⊢ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} = \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}$
78	77	inteqi	$⊢ ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\} = ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}$
79	78	mpteq2i	$⊢ (x \in V ⟼ ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land z \circ z \subseteq z)\}) = (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\})$
80	6 70 79	3eqtri	$⊢ (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land ({I ↾}_{(dom y \cup ran y)} \subseteq y \land y \circ y \subseteq y))\}) = (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\})$
81	1 80	eqtr4i	$⊢ t* = (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land ({I ↾}_{(dom y \cup ran y)} \subseteq y \land y \circ y \subseteq y))\})$

Metamath Proof Explorer

Theorem dfrtrcl5

Proof