# Metamath Proof Explorer

## Theorem dfrtrcl5

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

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

### Proof

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