# Metamath Proof Explorer

## Theorem bnj893

Description: Property of _trCl . Under certain conditions, the transitive closure of X in A by R is a set. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj893 ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\right)\to trCl\left({X},{A},{R}\right)\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 biid ${⊢}{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)↔{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
2 biid ${⊢}\forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)↔\forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
3 eqid ${⊢}\mathrm{\omega }\setminus \left\{\varnothing \right\}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
4 eqid ${⊢}\left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}=\left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}$
5 1 2 3 4 bnj882 ${⊢}trCl\left({X},{A},{R}\right)=\bigcup _{{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)$
6 vex ${⊢}{g}\in \mathrm{V}$
7 fveq1 ${⊢}{f}={g}\to {f}\left(\varnothing \right)={g}\left(\varnothing \right)$
8 7 eqeq1d ${⊢}{f}={g}\to \left({f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)↔{g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\right)$
9 6 8 sbcie
10 9 bicomi
11 fveq1 ${⊢}{f}={g}\to {f}\left(\mathrm{suc}{i}\right)={g}\left(\mathrm{suc}{i}\right)$
12 fveq1 ${⊢}{f}={g}\to {f}\left({i}\right)={g}\left({i}\right)$
13 12 iuneq1d ${⊢}{f}={g}\to \bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)$
14 11 13 eqeq12d ${⊢}{f}={g}\to \left({f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)↔{g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
15 14 imbi2d ${⊢}{f}={g}\to \left(\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)↔\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)$
16 15 ralbidv ${⊢}{f}={g}\to \left(\forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)↔\forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)$
17 6 16 sbcie
18 17 bicomi
19 4 10 18 bnj873 ${⊢}\left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}=\left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}$
20 19 eleq2i ${⊢}{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}↔{f}\in \left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}$
21 20 anbi1i ${⊢}\left({f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\wedge {w}\in \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\right)↔\left({f}\in \left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\wedge {w}\in \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\right)$
22 21 rexbii2 ${⊢}\exists {f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{w}\in \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)↔\exists {f}\in \left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{w}\in \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)$
23 22 abbii ${⊢}\left\{{w}|\exists {f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{w}\in \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\right\}=\left\{{w}|\exists {f}\in \left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{w}\in \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\right\}$
24 df-iun ${⊢}\bigcup _{{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)=\left\{{w}|\exists {f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{w}\in \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\right\}$
25 df-iun ${⊢}\bigcup _{{f}\in \left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)=\left\{{w}|\exists {f}\in \left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{w}\in \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\right\}$
26 23 24 25 3eqtr4i ${⊢}\bigcup _{{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)=\bigcup _{{f}\in \left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)$
27 biid ${⊢}{g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)↔{g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
28 biid ${⊢}\forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)↔\forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
29 eqid ${⊢}\left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}=\left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}$
30 biid ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\wedge {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\right)↔\left({R}FrSe{A}\wedge {X}\in {A}\wedge {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\right)$
31 biid ${⊢}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)↔\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)$
32 biid
33 biid
34 biid
35 biid ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\right)↔\left({R}FrSe{A}\wedge {X}\in {A}\right)$
36 27 28 3 29 30 31 32 33 34 35 bnj849 ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\right)\to \left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\in \mathrm{V}$
37 vex ${⊢}{f}\in \mathrm{V}$
38 37 dmex ${⊢}\mathrm{dom}{f}\in \mathrm{V}$
39 fvex ${⊢}{f}\left({i}\right)\in \mathrm{V}$
40 38 39 iunex ${⊢}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\in \mathrm{V}$
41 40 rgenw ${⊢}\forall {f}\in \left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\in \mathrm{V}$
42 iunexg ${⊢}\left(\left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\in \mathrm{V}\wedge \forall {f}\in \left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\in \mathrm{V}\right)\to \bigcup _{{f}\in \left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\in \mathrm{V}$
43 36 41 42 sylancl ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\right)\to \bigcup _{{f}\in \left\{{g}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({g}Fn{n}\wedge {g}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {g}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {g}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\in \mathrm{V}$
44 26 43 eqeltrid ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\right)\to \bigcup _{{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\in \mathrm{V}$
45 5 44 eqeltrid ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\right)\to trCl\left({X},{A},{R}\right)\in \mathrm{V}$