Metamath Proof Explorer

Theorem dfrcl2

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

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

Proof

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