# Metamath Proof Explorer

## Theorem bnj1000

Description: Technical lemma for bnj852 . 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 bnj1000.1 ${⊢}{\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)$
bnj1000.2 No typesetting found for |- ( ps" <-> [. G / f ]. ps ) with typecode |-
bnj1000.3 ${⊢}{G}\in \mathrm{V}$
bnj1000.15 ${⊢}{C}=\bigcup _{{y}\in {f}\left({m}\right)}pred\left({y},{A},{R}\right)$
bnj1000.16 ${⊢}{G}={f}\cup \left\{⟨{n},{C}⟩\right\}$
Assertion bnj1000 Could not format assertion : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. N -> ( G  suc i ) = U_ y e. ( G  i ) _pred ( y , A , R ) ) ) with typecode |-

### Proof

Step Hyp Ref Expression
1 bnj1000.1 ${⊢}{\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)$
2 bnj1000.2 Could not format ( ps" <-> [. G / f ]. ps ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps ) with typecode |-
3 bnj1000.3 ${⊢}{G}\in \mathrm{V}$
4 bnj1000.15 ${⊢}{C}=\bigcup _{{y}\in {f}\left({m}\right)}pred\left({y},{A},{R}\right)$
5 bnj1000.16 ${⊢}{G}={f}\cup \left\{⟨{n},{C}⟩\right\}$
6 df-ral ${⊢}\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}\phantom{\rule{.4em}{0ex}}\left({i}\in \mathrm{\omega }\to \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)$
7 6 bicomi ${⊢}\forall {i}\phantom{\rule{.4em}{0ex}}\left({i}\in \mathrm{\omega }\to \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)↔\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)$
8 7 sbcbii
9 nfv ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}{i}\in \mathrm{\omega }$
10 9 sbc19.21g
11 3 10 ax-mp
12 nfv ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{i}\in {N}$
13 12 sbc19.21g
14 3 13 ax-mp
15 fveq1 ${⊢}{f}={G}\to {f}\left(\mathrm{suc}{i}\right)={G}\left(\mathrm{suc}{i}\right)$
16 fveq1 ${⊢}{f}={G}\to {f}\left({i}\right)={G}\left({i}\right)$
17 ax-5 ${⊢}{w}\in {f}\left({i}\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}{w}\in {f}\left({i}\right)$
18 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{f}$
19 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{n}$
20 nfiu1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\bigcup _{{y}\in {f}\left({m}\right)}pred\left({y},{A},{R}\right)$
21 4 20 nfcxfr ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{C}$
22 19 21 nfop ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}⟨{n},{C}⟩$
23 22 nfsn ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{⟨{n},{C}⟩\right\}$
24 18 23 nfun ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({f}\cup \left\{⟨{n},{C}⟩\right\}\right)$
25 5 24 nfcxfr ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{G}$
26 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{i}$
27 25 26 nffv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{G}\left({i}\right)$
28 27 nfcrii ${⊢}{w}\in {G}\left({i}\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}{w}\in {G}\left({i}\right)$
29 17 28 bnj1316 ${⊢}{f}\left({i}\right)={G}\left({i}\right)\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)$
30 16 29 syl ${⊢}{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)$
31 15 30 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)$
32 fveq1 ${⊢}{f}={e}\to {f}\left(\mathrm{suc}{i}\right)={e}\left(\mathrm{suc}{i}\right)$
33 fveq1 ${⊢}{f}={e}\to {f}\left({i}\right)={e}\left({i}\right)$
34 ax-5 ${⊢}{f}\left({i}\right)={e}\left({i}\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}{f}\left({i}\right)={e}\left({i}\right)$
35 34 bnj956 ${⊢}{f}\left({i}\right)={e}\left({i}\right)\to \bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)=\bigcup _{{y}\in {e}\left({i}\right)}pred\left({y},{A},{R}\right)$
36 33 35 syl ${⊢}{f}={e}\to \bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)=\bigcup _{{y}\in {e}\left({i}\right)}pred\left({y},{A},{R}\right)$
37 32 36 eqeq12d ${⊢}{f}={e}\to \left({f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)↔{e}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {e}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
38 fveq1 ${⊢}{e}={G}\to {e}\left(\mathrm{suc}{i}\right)={G}\left(\mathrm{suc}{i}\right)$
39 fveq1 ${⊢}{e}={G}\to {e}\left({i}\right)={G}\left({i}\right)$
40 ax-5 ${⊢}{w}\in {e}\left({i}\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}{w}\in {e}\left({i}\right)$
41 40 28 bnj1316 ${⊢}{e}\left({i}\right)={G}\left({i}\right)\to \bigcup _{{y}\in {e}\left({i}\right)}pred\left({y},{A},{R}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
42 39 41 syl ${⊢}{e}={G}\to \bigcup _{{y}\in {e}\left({i}\right)}pred\left({y},{A},{R}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
43 38 42 eqeq12d ${⊢}{e}={G}\to \left({e}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {e}\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)$
44 3 31 37 43 bnj610
45 44 imbi2i
46 14 45 bitri
47 46 imbi2i
48 11 47 bitri
49 48 albii
50 sbcal
51 df-ral ${⊢}\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}\phantom{\rule{.4em}{0ex}}\left({i}\in \mathrm{\omega }\to \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)$
52 49 50 51 3bitr4ri
53 1 sbcbii
54 8 52 53 3bitr4ri
55 2 54 bitri Could not format ( ps" <-> A. i e. _om ( suc i e. N -> ( G  suc i ) = U_ y e. ( G  i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. N -> ( G  suc i ) = U_ y e. ( G  i ) _pred ( y , A , R ) ) ) with typecode |-