# Metamath Proof Explorer

## Theorem 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 ${⊢}\bigcap \left\{{x}|\left({A}\subseteq {x}\wedge \left({x}\circ {x}\subseteq {x}\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\subseteq {x}\right)\right)\right\}\in \mathrm{V}$

### Proof

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