# Metamath Proof Explorer

## Theorem brtrclfv2

Description: Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020)

Ref Expression
Assertion brtrclfv2 ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \left({X}\mathrm{t+}\left({R}\right){Y}↔{Y}\in \bigcap \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 df-br ${⊢}{X}\bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}{Y}↔⟨{X},{Y}⟩\in \bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}$
2 1 a1i ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \left({X}\bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}{Y}↔⟨{X},{Y}⟩\in \bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\right)$
3 trclfv ${⊢}{R}\in {W}\to \mathrm{t+}\left({R}\right)=\bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}$
4 3 breqd ${⊢}{R}\in {W}\to \left({X}\mathrm{t+}\left({R}\right){Y}↔{X}\bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}{Y}\right)$
5 4 3ad2ant3 ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \left({X}\mathrm{t+}\left({R}\right){Y}↔{X}\bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}{Y}\right)$
6 elimasng ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\right)\to \left({Y}\in \bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\left[\left\{{X}\right\}\right]↔⟨{X},{Y}⟩\in \bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\right)$
7 6 3adant3 ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \left({Y}\in \bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\left[\left\{{X}\right\}\right]↔⟨{X},{Y}⟩\in \bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\right)$
8 2 5 7 3bitr4d ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \left({X}\mathrm{t+}\left({R}\right){Y}↔{Y}\in \bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\left[\left\{{X}\right\}\right]\right)$
9 intimasn ${⊢}{X}\in {U}\to \bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\left[\left\{{X}\right\}\right]=\bigcap \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}$
10 9 3ad2ant1 ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\left[\left\{{X}\right\}\right]=\bigcap \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}$
11 simpl3 ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to {R}\in {W}$
12 snex ${⊢}\left\{{X}\right\}\in \mathrm{V}$
13 vex ${⊢}{f}\in \mathrm{V}$
14 12 13 xpex ${⊢}\left\{{X}\right\}×{f}\in \mathrm{V}$
15 unexg ${⊢}\left({R}\in {W}\wedge \left\{{X}\right\}×{f}\in \mathrm{V}\right)\to {R}\cup \left(\left\{{X}\right\}×{f}\right)\in \mathrm{V}$
16 11 14 15 sylancl ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to {R}\cup \left(\left\{{X}\right\}×{f}\right)\in \mathrm{V}$
17 trclfvlb ${⊢}{R}\cup \left(\left\{{X}\right\}×{f}\right)\in \mathrm{V}\to {R}\cup \left(\left\{{X}\right\}×{f}\right)\subseteq \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)$
18 17 unssad ${⊢}{R}\cup \left(\left\{{X}\right\}×{f}\right)\in \mathrm{V}\to {R}\subseteq \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)$
19 16 18 syl ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to {R}\subseteq \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)$
20 trclfvcotrg ${⊢}\mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\circ \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\subseteq \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)$
21 20 a1i ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\circ \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\subseteq \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)$
22 simpl1 ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to {X}\in {U}$
23 snidg ${⊢}{X}\in {U}\to {X}\in \left\{{X}\right\}$
24 22 23 syl ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to {X}\in \left\{{X}\right\}$
25 inelcm ${⊢}\left({X}\in \left\{{X}\right\}\wedge {X}\in \left\{{X}\right\}\right)\to \left\{{X}\right\}\cap \left\{{X}\right\}\ne \varnothing$
26 24 24 25 syl2anc ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to \left\{{X}\right\}\cap \left\{{X}\right\}\ne \varnothing$
27 xpima2 ${⊢}\left\{{X}\right\}\cap \left\{{X}\right\}\ne \varnothing \to \left(\left\{{X}\right\}×{f}\right)\left[\left\{{X}\right\}\right]={f}$
28 26 27 syl ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to \left(\left\{{X}\right\}×{f}\right)\left[\left\{{X}\right\}\right]={f}$
29 16 17 syl ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to {R}\cup \left(\left\{{X}\right\}×{f}\right)\subseteq \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)$
30 29 unssbd ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to \left\{{X}\right\}×{f}\subseteq \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)$
31 imass1 ${⊢}\left\{{X}\right\}×{f}\subseteq \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\to \left(\left\{{X}\right\}×{f}\right)\left[\left\{{X}\right\}\right]\subseteq \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\left[\left\{{X}\right\}\right]$
32 30 31 syl ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to \left(\left\{{X}\right\}×{f}\right)\left[\left\{{X}\right\}\right]\subseteq \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\left[\left\{{X}\right\}\right]$
33 28 32 eqsstrrd ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to {f}\subseteq \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\left[\left\{{X}\right\}\right]$
34 imaundir ${⊢}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\left[\left\{{X}\right\}\cup {f}\right]={R}\left[\left\{{X}\right\}\cup {f}\right]\cup \left(\left\{{X}\right\}×{f}\right)\left[\left\{{X}\right\}\cup {f}\right]$
35 simpr ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}$
36 imassrn ${⊢}\left(\left\{{X}\right\}×{f}\right)\left[\left\{{X}\right\}\cup {f}\right]\subseteq \mathrm{ran}\left(\left\{{X}\right\}×{f}\right)$
37 rnxpss ${⊢}\mathrm{ran}\left(\left\{{X}\right\}×{f}\right)\subseteq {f}$
38 36 37 sstri ${⊢}\left(\left\{{X}\right\}×{f}\right)\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}$
39 38 a1i ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to \left(\left\{{X}\right\}×{f}\right)\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}$
40 35 39 unssd ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to {R}\left[\left\{{X}\right\}\cup {f}\right]\cup \left(\left\{{X}\right\}×{f}\right)\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}$
41 34 40 eqsstrid ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to \left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}$
42 trclimalb2 ${⊢}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\in \mathrm{V}\wedge \left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\left[\left\{{X}\right\}\right]\subseteq {f}$
43 16 41 42 syl2anc ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to \mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\left[\left\{{X}\right\}\right]\subseteq {f}$
44 33 43 eqssd ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to {f}=\mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\left[\left\{{X}\right\}\right]$
45 sbcan
46 sbcan
47 fvex ${⊢}\mathrm{t+}\left({R}\cup \left(\left\{{X}\right\}×{f}\right)\right)\in \mathrm{V}$
48 sbcssg
49 47 48 ax-mp
50 csbconstg
51 47 50 ax-mp
52 47 csbvargi
53 51 52 sseq12i
54 49 53 bitri
55 sbcssg
56 47 55 ax-mp
57 csbcog
58 47 57 ax-mp
59 52 52 coeq12i
60 58 59 eqtri
61 60 52 sseq12i
62 56 61 bitri
63 54 62 anbi12i
64 46 63 bitri
65 sbceq2g
66 47 65 ax-mp
67 csbima12
68 52 imaeq1i
69 csbconstg
70 47 69 ax-mp
71 70 imaeq2i
72 67 68 71 3eqtri
73 72 eqeq2i
74 66 73 bitri
75 64 74 anbi12i
76 45 75 sylbbr
77 19 21 44 76 syl21anc
78 77 spesbcd ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\wedge {R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right)\to \exists {r}\phantom{\rule{.4em}{0ex}}\left(\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\wedge {f}={r}\left[\left\{{X}\right\}\right]\right)$
79 78 ex ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \left({R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\to \exists {r}\phantom{\rule{.4em}{0ex}}\left(\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\wedge {f}={r}\left[\left\{{X}\right\}\right]\right)\right)$
80 eqeq1 ${⊢}{g}={f}\to \left({g}={s}\left[\left\{{X}\right\}\right]↔{f}={s}\left[\left\{{X}\right\}\right]\right)$
81 80 rexbidv ${⊢}{g}={f}\to \left(\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]↔\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{f}={s}\left[\left\{{X}\right\}\right]\right)$
82 imaeq1 ${⊢}{s}={r}\to {s}\left[\left\{{X}\right\}\right]={r}\left[\left\{{X}\right\}\right]$
83 82 eqeq2d ${⊢}{s}={r}\to \left({f}={s}\left[\left\{{X}\right\}\right]↔{f}={r}\left[\left\{{X}\right\}\right]\right)$
84 83 rexab2 ${⊢}\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{f}={s}\left[\left\{{X}\right\}\right]↔\exists {r}\phantom{\rule{.4em}{0ex}}\left(\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\wedge {f}={r}\left[\left\{{X}\right\}\right]\right)$
85 81 84 syl6bb ${⊢}{g}={f}\to \left(\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]↔\exists {r}\phantom{\rule{.4em}{0ex}}\left(\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\wedge {f}={r}\left[\left\{{X}\right\}\right]\right)\right)$
86 13 85 elab ${⊢}{f}\in \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}↔\exists {r}\phantom{\rule{.4em}{0ex}}\left(\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\wedge {f}={r}\left[\left\{{X}\right\}\right]\right)$
87 79 86 syl6ibr ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \left({R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\to {f}\in \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}\right)$
88 intss1 ${⊢}{f}\in \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}\to \bigcap \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}\subseteq {f}$
89 87 88 syl6 ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \left({R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\to \bigcap \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}\subseteq {f}\right)$
90 89 alrimiv ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \forall {f}\phantom{\rule{.4em}{0ex}}\left({R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\to \bigcap \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}\subseteq {f}\right)$
91 ssintab ${⊢}\bigcap \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}\subseteq \bigcap \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}↔\forall {f}\phantom{\rule{.4em}{0ex}}\left({R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\to \bigcap \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}\subseteq {f}\right)$
92 90 91 sylibr ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \bigcap \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}\subseteq \bigcap \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}$
93 ssintab ${⊢}\bigcap \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}\subseteq \bigcap \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}↔\forall {g}\phantom{\rule{.4em}{0ex}}\left(\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\to \bigcap \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}\subseteq {g}\right)$
94 82 eqeq2d ${⊢}{s}={r}\to \left({g}={s}\left[\left\{{X}\right\}\right]↔{g}={r}\left[\left\{{X}\right\}\right]\right)$
95 94 rexab2 ${⊢}\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]↔\exists {r}\phantom{\rule{.4em}{0ex}}\left(\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\wedge {g}={r}\left[\left\{{X}\right\}\right]\right)$
96 simpr ${⊢}\left(\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\wedge {g}={r}\left[\left\{{X}\right\}\right]\right)\to {g}={r}\left[\left\{{X}\right\}\right]$
97 imass1 ${⊢}{R}\subseteq {r}\to {R}\left[\left\{{X}\right\}\right]\subseteq {r}\left[\left\{{X}\right\}\right]$
98 97 adantr ${⊢}\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\to {R}\left[\left\{{X}\right\}\right]\subseteq {r}\left[\left\{{X}\right\}\right]$
99 imass1 ${⊢}{R}\subseteq {r}\to {R}\left[{r}\left[\left\{{X}\right\}\right]\right]\subseteq {r}\left[{r}\left[\left\{{X}\right\}\right]\right]$
100 imaco ${⊢}\left({r}\circ {r}\right)\left[\left\{{X}\right\}\right]={r}\left[{r}\left[\left\{{X}\right\}\right]\right]$
101 imass1 ${⊢}{r}\circ {r}\subseteq {r}\to \left({r}\circ {r}\right)\left[\left\{{X}\right\}\right]\subseteq {r}\left[\left\{{X}\right\}\right]$
102 100 101 eqsstrrid ${⊢}{r}\circ {r}\subseteq {r}\to {r}\left[{r}\left[\left\{{X}\right\}\right]\right]\subseteq {r}\left[\left\{{X}\right\}\right]$
103 99 102 sylan9ss ${⊢}\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\to {R}\left[{r}\left[\left\{{X}\right\}\right]\right]\subseteq {r}\left[\left\{{X}\right\}\right]$
104 98 103 jca ${⊢}\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\to \left({R}\left[\left\{{X}\right\}\right]\subseteq {r}\left[\left\{{X}\right\}\right]\wedge {R}\left[{r}\left[\left\{{X}\right\}\right]\right]\subseteq {r}\left[\left\{{X}\right\}\right]\right)$
105 104 adantr ${⊢}\left(\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\wedge {g}={r}\left[\left\{{X}\right\}\right]\right)\to \left({R}\left[\left\{{X}\right\}\right]\subseteq {r}\left[\left\{{X}\right\}\right]\wedge {R}\left[{r}\left[\left\{{X}\right\}\right]\right]\subseteq {r}\left[\left\{{X}\right\}\right]\right)$
106 vex ${⊢}{r}\in \mathrm{V}$
107 106 imaex ${⊢}{r}\left[\left\{{X}\right\}\right]\in \mathrm{V}$
108 imaundi ${⊢}{R}\left[\left\{{X}\right\}\cup {f}\right]={R}\left[\left\{{X}\right\}\right]\cup {R}\left[{f}\right]$
109 108 sseq1i ${⊢}{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}↔{R}\left[\left\{{X}\right\}\right]\cup {R}\left[{f}\right]\subseteq {f}$
110 unss ${⊢}\left({R}\left[\left\{{X}\right\}\right]\subseteq {f}\wedge {R}\left[{f}\right]\subseteq {f}\right)↔{R}\left[\left\{{X}\right\}\right]\cup {R}\left[{f}\right]\subseteq {f}$
111 109 110 bitr4i ${⊢}{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}↔\left({R}\left[\left\{{X}\right\}\right]\subseteq {f}\wedge {R}\left[{f}\right]\subseteq {f}\right)$
112 imaeq2 ${⊢}{f}={r}\left[\left\{{X}\right\}\right]\to {R}\left[{f}\right]={R}\left[{r}\left[\left\{{X}\right\}\right]\right]$
113 id ${⊢}{f}={r}\left[\left\{{X}\right\}\right]\to {f}={r}\left[\left\{{X}\right\}\right]$
114 112 113 sseq12d ${⊢}{f}={r}\left[\left\{{X}\right\}\right]\to \left({R}\left[{f}\right]\subseteq {f}↔{R}\left[{r}\left[\left\{{X}\right\}\right]\right]\subseteq {r}\left[\left\{{X}\right\}\right]\right)$
115 114 cleq2lem ${⊢}{f}={r}\left[\left\{{X}\right\}\right]\to \left(\left({R}\left[\left\{{X}\right\}\right]\subseteq {f}\wedge {R}\left[{f}\right]\subseteq {f}\right)↔\left({R}\left[\left\{{X}\right\}\right]\subseteq {r}\left[\left\{{X}\right\}\right]\wedge {R}\left[{r}\left[\left\{{X}\right\}\right]\right]\subseteq {r}\left[\left\{{X}\right\}\right]\right)\right)$
116 111 115 syl5bb ${⊢}{f}={r}\left[\left\{{X}\right\}\right]\to \left({R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}↔\left({R}\left[\left\{{X}\right\}\right]\subseteq {r}\left[\left\{{X}\right\}\right]\wedge {R}\left[{r}\left[\left\{{X}\right\}\right]\right]\subseteq {r}\left[\left\{{X}\right\}\right]\right)\right)$
117 107 116 elab ${⊢}{r}\left[\left\{{X}\right\}\right]\in \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}↔\left({R}\left[\left\{{X}\right\}\right]\subseteq {r}\left[\left\{{X}\right\}\right]\wedge {R}\left[{r}\left[\left\{{X}\right\}\right]\right]\subseteq {r}\left[\left\{{X}\right\}\right]\right)$
118 105 117 sylibr ${⊢}\left(\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\wedge {g}={r}\left[\left\{{X}\right\}\right]\right)\to {r}\left[\left\{{X}\right\}\right]\in \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}$
119 96 118 eqeltrd ${⊢}\left(\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\wedge {g}={r}\left[\left\{{X}\right\}\right]\right)\to {g}\in \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}$
120 119 exlimiv ${⊢}\exists {r}\phantom{\rule{.4em}{0ex}}\left(\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\wedge {g}={r}\left[\left\{{X}\right\}\right]\right)\to {g}\in \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}$
121 95 120 sylbi ${⊢}\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\to {g}\in \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}$
122 intss1 ${⊢}{g}\in \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}\to \bigcap \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}\subseteq {g}$
123 121 122 syl ${⊢}\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\to \bigcap \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}\subseteq {g}$
124 93 123 mpgbir ${⊢}\bigcap \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}\subseteq \bigcap \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}$
125 124 a1i ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \bigcap \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}\subseteq \bigcap \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}$
126 92 125 eqssd ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \bigcap \left\{{g}|\exists {s}\in \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\phantom{\rule{.4em}{0ex}}{g}={s}\left[\left\{{X}\right\}\right]\right\}=\bigcap \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}$
127 10 126 eqtrd ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\left[\left\{{X}\right\}\right]=\bigcap \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}$
128 127 eleq2d ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \left({Y}\in \bigcap \left\{{r}|\left({R}\subseteq {r}\wedge {r}\circ {r}\subseteq {r}\right)\right\}\left[\left\{{X}\right\}\right]↔{Y}\in \bigcap \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}\right)$
129 8 128 bitrd ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {R}\in {W}\right)\to \left({X}\mathrm{t+}\left({R}\right){Y}↔{Y}\in \bigcap \left\{{f}|{R}\left[\left\{{X}\right\}\cup {f}\right]\subseteq {f}\right\}\right)$