Metamath Proof Explorer

Theorem bnj981

Description: Technical lemma for bnj69 . 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
Hypotheses bnj981.1 ${⊢}{\phi }↔{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
bnj981.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)$
bnj981.3 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
bnj981.4 ${⊢}{B}=\left\{{f}|\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)\right\}$
bnj981.5 ${⊢}{\chi }↔\left({n}\in {D}\wedge {f}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
Assertion bnj981 ${⊢}{Z}\in trCl\left({X},{A},{R}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {n}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {i}\in {n}\wedge {Z}\in {f}\left({i}\right)\right)$

Proof

Step Hyp Ref Expression
1 bnj981.1 ${⊢}{\phi }↔{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
2 bnj981.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 bnj981.3 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
4 bnj981.4 ${⊢}{B}=\left\{{f}|\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)\right\}$
5 bnj981.5 ${⊢}{\chi }↔\left({n}\in {D}\wedge {f}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
6 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{Z}\in trCl\left({X},{A},{R}\right)$
7 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\mathrm{\omega }$
8 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{i}\in {n}$
9 nfiu1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)$
10 9 nfeq2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)$
11 8 10 nfim ${⊢}Ⅎ{y}\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 7 11 nfralw ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\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)$
13 2 12 nfxfr ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
14 13 nf5ri ${⊢}{\psi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$
15 14 5 bnj1096 ${⊢}{\chi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\chi }$
16 15 nf5i ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\chi }$
17 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{i}\in {n}$
18 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{Z}\in {f}\left({i}\right)$
19 16 17 18 nf3an ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {i}\in {n}\wedge {Z}\in {f}\left({i}\right)\right)$
20 19 nfex ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {i}\in {n}\wedge {Z}\in {f}\left({i}\right)\right)$
21 20 nfex ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists {n}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {i}\in {n}\wedge {Z}\in {f}\left({i}\right)\right)$
22 21 nfex ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {n}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {i}\in {n}\wedge {Z}\in {f}\left({i}\right)\right)$
23 6 22 nfim ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({Z}\in trCl\left({X},{A},{R}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {n}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {i}\in {n}\wedge {Z}\in {f}\left({i}\right)\right)\right)$
24 eleq1 ${⊢}{y}={Z}\to \left({y}\in trCl\left({X},{A},{R}\right)↔{Z}\in trCl\left({X},{A},{R}\right)\right)$
25 eleq1 ${⊢}{y}={Z}\to \left({y}\in {f}\left({i}\right)↔{Z}\in {f}\left({i}\right)\right)$
26 25 3anbi3d ${⊢}{y}={Z}\to \left(\left({\chi }\wedge {i}\in {n}\wedge {y}\in {f}\left({i}\right)\right)↔\left({\chi }\wedge {i}\in {n}\wedge {Z}\in {f}\left({i}\right)\right)\right)$
27 26 3exbidv ${⊢}{y}={Z}\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\exists {n}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {i}\in {n}\wedge {y}\in {f}\left({i}\right)\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\exists {n}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {i}\in {n}\wedge {Z}\in {f}\left({i}\right)\right)\right)$
28 24 27 imbi12d ${⊢}{y}={Z}\to \left(\left({y}\in trCl\left({X},{A},{R}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {n}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {i}\in {n}\wedge {y}\in {f}\left({i}\right)\right)\right)↔\left({Z}\in trCl\left({X},{A},{R}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {n}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {i}\in {n}\wedge {Z}\in {f}\left({i}\right)\right)\right)\right)$
29 1 2 3 4 5 bnj917 ${⊢}{y}\in trCl\left({X},{A},{R}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {n}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {i}\in {n}\wedge {y}\in {f}\left({i}\right)\right)$
30 23 28 29 vtoclg1f ${⊢}{Z}\in trCl\left({X},{A},{R}\right)\to \left({Z}\in trCl\left({X},{A},{R}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {n}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {i}\in {n}\wedge {Z}\in {f}\left({i}\right)\right)\right)$
31 30 pm2.43i ${⊢}{Z}\in trCl\left({X},{A},{R}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {n}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {i}\in {n}\wedge {Z}\in {f}\left({i}\right)\right)$