# Metamath Proof Explorer

## Theorem bnj1318

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj1318 ${⊢}{X}={Y}\to trCl\left({X},{A},{R}\right)=trCl\left({Y},{A},{R}\right)$

### Proof

Step Hyp Ref Expression
1 bnj602 ${⊢}{X}={Y}\to pred\left({X},{A},{R}\right)=pred\left({Y},{A},{R}\right)$
2 1 eqeq2d ${⊢}{X}={Y}\to \left({f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)↔{f}\left(\varnothing \right)=pred\left({Y},{A},{R}\right)\right)$
3 2 3anbi2d ${⊢}{X}={Y}\to \left(\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 {f}\left(\varnothing \right)=pred\left({Y},{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)$
4 3 rexbidv ${⊢}{X}={Y}\to \left(\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)↔\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({Y},{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 4 abbidv ${⊢}{X}={Y}\to \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({Y},{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\}$
6 hbab1 ${⊢}{z}\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\}\to \forall {f}\phantom{\rule{.4em}{0ex}}{z}\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\}$
7 hbab1 ${⊢}{z}\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({Y},{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\}\to \forall {f}\phantom{\rule{.4em}{0ex}}{z}\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({Y},{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\}$
8 6 7 bnj1316 ${⊢}\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({Y},{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\}\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)=\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({Y},{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)$
9 5 8 syl ${⊢}{X}={Y}\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)=\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({Y},{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)$
10 biid ${⊢}{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)↔{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
11 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)$
12 eqid ${⊢}\mathrm{\omega }\setminus \left\{\varnothing \right\}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
13 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\}$
14 10 11 12 13 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)$
15 biid ${⊢}{f}\left(\varnothing \right)=pred\left({Y},{A},{R}\right)↔{f}\left(\varnothing \right)=pred\left({Y},{A},{R}\right)$
16 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({Y},{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({Y},{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 15 11 12 16 bnj882 ${⊢}trCl\left({Y},{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({Y},{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)$
18 9 14 17 3eqtr4g ${⊢}{X}={Y}\to trCl\left({X},{A},{R}\right)=trCl\left({Y},{A},{R}\right)$