# Metamath Proof Explorer

## Theorem bnj882

Description: Definition (using hypotheses for readability) of the function giving the transitive closure of X in A by R . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj882.1 ${⊢}{\phi }↔{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
bnj882.2 ${⊢}{\psi }↔\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)$
bnj882.3 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
bnj882.4 ${⊢}{B}=\left\{{f}|\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)\right\}$
Assertion bnj882 ${⊢}trCl\left({X},{A},{R}\right)=\bigcup _{{f}\in {B}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)$

### Proof

Step Hyp Ref Expression
1 bnj882.1 ${⊢}{\phi }↔{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
2 bnj882.2 ${⊢}{\psi }↔\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 bnj882.3 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
4 bnj882.4 ${⊢}{B}=\left\{{f}|\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)\right\}$
5 df-bnj18 ${⊢}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 df-iun ${⊢}\bigcup _{{f}\in {B}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)=\left\{{w}|\exists {f}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\right\}$
7 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\}$
8 1 2 anbi12i ${⊢}\left({\phi }\wedge {\psi }\right)↔\left({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)$
9 8 anbi2i ${⊢}\left({f}Fn{n}\wedge \left({\phi }\wedge {\psi }\right)\right)↔\left({f}Fn{n}\wedge \left({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)$
10 3anass ${⊢}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)↔\left({f}Fn{n}\wedge \left({\phi }\wedge {\psi }\right)\right)$
11 3anass ${⊢}\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)↔\left({f}Fn{n}\wedge \left({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)$
12 9 10 11 3bitr4i ${⊢}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)↔\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)$
13 3 12 rexeqbii ${⊢}\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)↔\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)$
14 13 abbii ${⊢}\left\{{f}|\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\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\}$
15 4 14 eqtri ${⊢}{B}=\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\}$
16 15 eleq2i ${⊢}{f}\in {B}↔{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\}$
17 16 anbi1i ${⊢}\left({f}\in {B}\wedge {w}\in \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\right)↔\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)$
18 17 rexbii2 ${⊢}\exists {f}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)↔\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)$
19 18 abbii ${⊢}\left\{{w}|\exists {f}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\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\}$
20 7 19 eqtr4i ${⊢}\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 {B}\phantom{\rule{.4em}{0ex}}{w}\in \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\right\}$
21 6 20 eqtr4i ${⊢}\bigcup _{{f}\in {B}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\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)$
22 5 21 eqtr4i ${⊢}trCl\left({X},{A},{R}\right)=\bigcup _{{f}\in {B}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)$