dfrcl2

Description: Reflexive closure of a relation as union with restricted identity relation. (Contributed by RP, 6-Jun-2020)

		Ref	Expression
	Assertion	dfrcl2	$⊢ r* = (x \in V ⟼ ({I ↾}_{(dom x \cup ran x)}) \cup x)$

Proof

Step	Hyp	Ref	Expression
1		df-rcl	$⊢ r* = (x \in V ⟼ ⋂ \{z \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\})$
2		rabab	$⊢ \{z \in V \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\} = \{z \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\}$
3	2	eqcomi	$⊢ \{z \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\} = \{z \in V \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\}$
4	3	inteqi	$⊢ ⋂ \{z \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\} = ⋂ \{z \in V \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\}$
5	4	a1i	$⊢ x \in V \to ⋂ \{z \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\} = ⋂ \{z \in V \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\}$
6		vex	$⊢ x \in V$
7	6	dmex	$⊢ dom x \in V$
8	6	rnex	$⊢ ran x \in V$
9	7 8	unex	$⊢ dom x \cup ran x \in V$
10		resiexg	$⊢ dom x \cup ran x \in V \to {I ↾}_{(dom x \cup ran x)} \in V$
11	9 10	ax-mp	$⊢ {I ↾}_{(dom x \cup ran x)} \in V$
12	11 6	unex	$⊢ ({I ↾}_{(dom x \cup ran x)}) \cup x \in V$
13	12	a1i	$⊢ x \in V \to ({I ↾}_{(dom x \cup ran x)}) \cup x \in V$
14		ssun2	$⊢ x \subseteq ({I ↾}_{(dom x \cup ran x)}) \cup x$
15		dmun	$⊢ dom (({I ↾}_{(dom x \cup ran x)}) \cup x) = dom ({I ↾}_{(dom x \cup ran x)}) \cup dom x$
16		dmresi	$⊢ dom ({I ↾}_{(dom x \cup ran x)}) = dom x \cup ran x$
17	16	uneq1i	$⊢ dom ({I ↾}_{(dom x \cup ran x)}) \cup dom x = (dom x \cup ran x) \cup dom x$
18		un23	$⊢ (dom x \cup ran x) \cup dom x = (dom x \cup dom x) \cup ran x$
19		unidm	$⊢ dom x \cup dom x = dom x$
20	19	uneq1i	$⊢ (dom x \cup dom x) \cup ran x = dom x \cup ran x$
21	18 20	eqtri	$⊢ (dom x \cup ran x) \cup dom x = dom x \cup ran x$
22	15 17 21	3eqtri	$⊢ dom (({I ↾}_{(dom x \cup ran x)}) \cup x) = dom x \cup ran x$
23		rnun	$⊢ ran (({I ↾}_{(dom x \cup ran x)}) \cup x) = ran ({I ↾}_{(dom x \cup ran x)}) \cup ran x$
24		rnresi	$⊢ ran ({I ↾}_{(dom x \cup ran x)}) = dom x \cup ran x$
25	24	uneq1i	$⊢ ran ({I ↾}_{(dom x \cup ran x)}) \cup ran x = (dom x \cup ran x) \cup ran x$
26		unass	$⊢ (dom x \cup ran x) \cup ran x = dom x \cup (ran x \cup ran x)$
27		unidm	$⊢ ran x \cup ran x = ran x$
28	27	uneq2i	$⊢ dom x \cup (ran x \cup ran x) = dom x \cup ran x$
29	26 28	eqtri	$⊢ (dom x \cup ran x) \cup ran x = dom x \cup ran x$
30	23 25 29	3eqtri	$⊢ ran (({I ↾}_{(dom x \cup ran x)}) \cup x) = dom x \cup ran x$
31	22 30	uneq12i	$⊢ dom (({I ↾}_{(dom x \cup ran x)}) \cup x) \cup ran (({I ↾}_{(dom x \cup ran x)}) \cup x) = (dom x \cup ran x) \cup (dom x \cup ran x)$
32		unidm	$⊢ (dom x \cup ran x) \cup (dom x \cup ran x) = dom x \cup ran x$
33	31 32	eqtri	$⊢ dom (({I ↾}_{(dom x \cup ran x)}) \cup x) \cup ran (({I ↾}_{(dom x \cup ran x)}) \cup x) = dom x \cup ran x$
34	33	reseq2i	$⊢ {I ↾}_{(dom (({I ↾}_{(dom x \cup ran x)}) \cup x) \cup ran (({I ↾}_{(dom x \cup ran x)}) \cup x))} = {I ↾}_{(dom x \cup ran x)}$
35		ssun1	$⊢ {I ↾}_{(dom x \cup ran x)} \subseteq ({I ↾}_{(dom x \cup ran x)}) \cup x$
36	34 35	eqsstri	$⊢ {I ↾}_{(dom (({I ↾}_{(dom x \cup ran x)}) \cup x) \cup ran (({I ↾}_{(dom x \cup ran x)}) \cup x))} \subseteq ({I ↾}_{(dom x \cup ran x)}) \cup x$
37	14 36	pm3.2i	$⊢ (x \subseteq ({I ↾}_{(dom x \cup ran x)}) \cup x \land {I ↾}_{(dom (({I ↾}_{(dom x \cup ran x)}) \cup x) \cup ran (({I ↾}_{(dom x \cup ran x)}) \cup x))} \subseteq ({I ↾}_{(dom x \cup ran x)}) \cup x)$
38		dmeq	$⊢ z = ({I ↾}_{(dom x \cup ran x)}) \cup x \to dom z = dom (({I ↾}_{(dom x \cup ran x)}) \cup x)$
39		rneq	$⊢ z = ({I ↾}_{(dom x \cup ran x)}) \cup x \to ran z = ran (({I ↾}_{(dom x \cup ran x)}) \cup x)$
40	38 39	uneq12d	$⊢ z = ({I ↾}_{(dom x \cup ran x)}) \cup x \to dom z \cup ran z = dom (({I ↾}_{(dom x \cup ran x)}) \cup x) \cup ran (({I ↾}_{(dom x \cup ran x)}) \cup x)$
41	40	reseq2d	$⊢ z = ({I ↾}_{(dom x \cup ran x)}) \cup x \to {I ↾}_{(dom z \cup ran z)} = {I ↾}_{(dom (({I ↾}_{(dom x \cup ran x)}) \cup x) \cup ran (({I ↾}_{(dom x \cup ran x)}) \cup x))}$
42		id	$⊢ z = ({I ↾}_{(dom x \cup ran x)}) \cup x \to z = ({I ↾}_{(dom x \cup ran x)}) \cup x$
43	41 42	sseq12d	$⊢ z = ({I ↾}_{(dom x \cup ran x)}) \cup x \to ({I ↾}_{(dom z \cup ran z)} \subseteq z \leftrightarrow {I ↾}_{(dom (({I ↾}_{(dom x \cup ran x)}) \cup x) \cup ran (({I ↾}_{(dom x \cup ran x)}) \cup x))} \subseteq ({I ↾}_{(dom x \cup ran x)}) \cup x)$
44	43	cleq2lem	$⊢ z = ({I ↾}_{(dom x \cup ran x)}) \cup x \to ((x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z) \leftrightarrow (x \subseteq ({I ↾}_{(dom x \cup ran x)}) \cup x \land {I ↾}_{(dom (({I ↾}_{(dom x \cup ran x)}) \cup x) \cup ran (({I ↾}_{(dom x \cup ran x)}) \cup x))} \subseteq ({I ↾}_{(dom x \cup ran x)}) \cup x))$
45	44	intminss	$⊢ (({I ↾}_{(dom x \cup ran x)}) \cup x \in V \land (x \subseteq ({I ↾}_{(dom x \cup ran x)}) \cup x \land {I ↾}_{(dom (({I ↾}_{(dom x \cup ran x)}) \cup x) \cup ran (({I ↾}_{(dom x \cup ran x)}) \cup x))} \subseteq ({I ↾}_{(dom x \cup ran x)}) \cup x)) \to ⋂ \{z \in V \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\} \subseteq ({I ↾}_{(dom x \cup ran x)}) \cup x$
46	13 37 45	sylancl	$⊢ x \in V \to ⋂ \{z \in V \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\} \subseteq ({I ↾}_{(dom x \cup ran x)}) \cup x$
47	5 46	eqsstrd	$⊢ x \in V \to ⋂ \{z \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\} \subseteq ({I ↾}_{(dom x \cup ran x)}) \cup x$
48		dmss	$⊢ x \subseteq z \to dom x \subseteq dom z$
49		rnss	$⊢ x \subseteq z \to ran x \subseteq ran z$
50		unss12	$⊢ (dom x \subseteq dom z \land ran x \subseteq ran z) \to dom x \cup ran x \subseteq dom z \cup ran z$
51	48 49 50	syl2anc	$⊢ x \subseteq z \to dom x \cup ran x \subseteq dom z \cup ran z$
52		dfss	$⊢ dom x \cup ran x \subseteq dom z \cup ran z \leftrightarrow dom x \cup ran x = (dom x \cup ran x) \cap (dom z \cup ran z)$
53	51 52	sylib	$⊢ x \subseteq z \to dom x \cup ran x = (dom x \cup ran x) \cap (dom z \cup ran z)$
54		incom	$⊢ (dom x \cup ran x) \cap (dom z \cup ran z) = (dom z \cup ran z) \cap (dom x \cup ran x)$
55	53 54	eqtrdi	$⊢ x \subseteq z \to dom x \cup ran x = (dom z \cup ran z) \cap (dom x \cup ran x)$
56	55	reseq2d	$⊢ x \subseteq z \to {I ↾}_{(dom x \cup ran x)} = {I ↾}_{((dom z \cup ran z) \cap (dom x \cup ran x))}$
57		resres	$⊢ {({I ↾}_{(dom z \cup ran z)}) ↾}_{(dom x \cup ran x)} = {I ↾}_{((dom z \cup ran z) \cap (dom x \cup ran x))}$
58	56 57	eqtr4di	$⊢ x \subseteq z \to {I ↾}_{(dom x \cup ran x)} = {({I ↾}_{(dom z \cup ran z)}) ↾}_{(dom x \cup ran x)}$
59		resss	$⊢ {({I ↾}_{(dom z \cup ran z)}) ↾}_{(dom x \cup ran x)} \subseteq {I ↾}_{(dom z \cup ran z)}$
60	59	a1i	$⊢ x \subseteq z \to {({I ↾}_{(dom z \cup ran z)}) ↾}_{(dom x \cup ran x)} \subseteq {I ↾}_{(dom z \cup ran z)}$
61	58 60	eqsstrd	$⊢ x \subseteq z \to {I ↾}_{(dom x \cup ran x)} \subseteq {I ↾}_{(dom z \cup ran z)}$
62	61	adantr	$⊢ (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z) \to {I ↾}_{(dom x \cup ran x)} \subseteq {I ↾}_{(dom z \cup ran z)}$
63		simpr	$⊢ (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z) \to {I ↾}_{(dom z \cup ran z)} \subseteq z$
64	62 63	sstrd	$⊢ (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z) \to {I ↾}_{(dom x \cup ran x)} \subseteq z$
65		simpl	$⊢ (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z) \to x \subseteq z$
66	64 65	unssd	$⊢ (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z) \to ({I ↾}_{(dom x \cup ran x)}) \cup x \subseteq z$
67	66	ax-gen	$⊢ \forall z ((x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z) \to ({I ↾}_{(dom x \cup ran x)}) \cup x \subseteq z)$
68	67	a1i	$⊢ x \in V \to \forall z ((x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z) \to ({I ↾}_{(dom x \cup ran x)}) \cup x \subseteq z)$
69		ssintab	$⊢ ({I ↾}_{(dom x \cup ran x)}) \cup x \subseteq ⋂ \{z \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\} \leftrightarrow \forall z ((x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z) \to ({I ↾}_{(dom x \cup ran x)}) \cup x \subseteq z)$
70	68 69	sylibr	$⊢ x \in V \to ({I ↾}_{(dom x \cup ran x)}) \cup x \subseteq ⋂ \{z \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\}$
71	47 70	eqssd	$⊢ x \in V \to ⋂ \{z \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\} = ({I ↾}_{(dom x \cup ran x)}) \cup x$
72	71	mpteq2ia	$⊢ (x \in V ⟼ ⋂ \{z \| (x \subseteq z \land {I ↾}_{(dom z \cup ran z)} \subseteq z)\}) = (x \in V ⟼ ({I ↾}_{(dom x \cup ran x)}) \cup x)$
73	1 72	eqtri	$⊢ r* = (x \in V ⟼ ({I ↾}_{(dom x \cup ran x)}) \cup x)$

Metamath Proof Explorer

Theorem dfrcl2

Proof