# Metamath Proof Explorer

## Theorem bnj966

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 bnj966.3 ${⊢}{\chi }↔\left({n}\in {D}\wedge {f}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
bnj966.10 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
bnj966.12 ${⊢}{C}=\bigcup _{{y}\in {f}\left({m}\right)}pred\left({y},{A},{R}\right)$
bnj966.13 ${⊢}{G}={f}\cup \left\{⟨{n},{C}⟩\right\}$
bnj966.44 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\right)\to {C}\in \mathrm{V}$
bnj966.53 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\right)\to {G}Fn{p}$
Assertion bnj966 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$

### Proof

Step Hyp Ref Expression
1 bnj966.3 ${⊢}{\chi }↔\left({n}\in {D}\wedge {f}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
2 bnj966.10 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
3 bnj966.12 ${⊢}{C}=\bigcup _{{y}\in {f}\left({m}\right)}pred\left({y},{A},{R}\right)$
4 bnj966.13 ${⊢}{G}={f}\cup \left\{⟨{n},{C}⟩\right\}$
5 bnj966.44 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\right)\to {C}\in \mathrm{V}$
6 bnj966.53 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\right)\to {G}Fn{p}$
7 6 bnj930 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\right)\to \mathrm{Fun}{G}$
8 7 3adant3 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to \mathrm{Fun}{G}$
9 opex ${⊢}⟨{n},{C}⟩\in \mathrm{V}$
10 9 snid ${⊢}⟨{n},{C}⟩\in \left\{⟨{n},{C}⟩\right\}$
11 elun2 ${⊢}⟨{n},{C}⟩\in \left\{⟨{n},{C}⟩\right\}\to ⟨{n},{C}⟩\in \left({f}\cup \left\{⟨{n},{C}⟩\right\}\right)$
12 10 11 ax-mp ${⊢}⟨{n},{C}⟩\in \left({f}\cup \left\{⟨{n},{C}⟩\right\}\right)$
13 12 4 eleqtrri ${⊢}⟨{n},{C}⟩\in {G}$
14 funopfv ${⊢}\mathrm{Fun}{G}\to \left(⟨{n},{C}⟩\in {G}\to {G}\left({n}\right)={C}\right)$
15 8 13 14 mpisyl ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {G}\left({n}\right)={C}$
16 simp22 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {n}=\mathrm{suc}{m}$
17 simp33 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {n}=\mathrm{suc}{i}$
18 bnj551 ${⊢}\left({n}=\mathrm{suc}{m}\wedge {n}=\mathrm{suc}{i}\right)\to {m}={i}$
19 16 17 18 syl2anc ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {m}={i}$
20 suceq ${⊢}{m}={i}\to \mathrm{suc}{m}=\mathrm{suc}{i}$
21 20 eqeq2d ${⊢}{m}={i}\to \left({n}=\mathrm{suc}{m}↔{n}=\mathrm{suc}{i}\right)$
22 21 biimpac ${⊢}\left({n}=\mathrm{suc}{m}\wedge {m}={i}\right)\to {n}=\mathrm{suc}{i}$
23 22 fveq2d ${⊢}\left({n}=\mathrm{suc}{m}\wedge {m}={i}\right)\to {G}\left({n}\right)={G}\left(\mathrm{suc}{i}\right)$
24 fveq2 ${⊢}{m}={i}\to {f}\left({m}\right)={f}\left({i}\right)$
25 24 bnj1113 ${⊢}{m}={i}\to \bigcup _{{y}\in {f}\left({m}\right)}pred\left({y},{A},{R}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)$
26 3 25 syl5eq ${⊢}{m}={i}\to {C}=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)$
27 26 adantl ${⊢}\left({n}=\mathrm{suc}{m}\wedge {m}={i}\right)\to {C}=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)$
28 23 27 eqeq12d ${⊢}\left({n}=\mathrm{suc}{m}\wedge {m}={i}\right)\to \left({G}\left({n}\right)={C}↔{G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
29 16 19 28 syl2anc ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to \left({G}\left({n}\right)={C}↔{G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
30 15 29 mpbid ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)$
31 5 3adant3 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {C}\in \mathrm{V}$
32 1 bnj1235 ${⊢}{\chi }\to {f}Fn{n}$
33 32 3ad2ant1 ${⊢}\left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\to {f}Fn{n}$
34 33 3ad2ant2 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {f}Fn{n}$
35 simp23 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {p}=\mathrm{suc}{n}$
36 31 34 35 17 bnj951 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to \left({C}\in \mathrm{V}\wedge {f}Fn{n}\wedge {p}=\mathrm{suc}{n}\wedge {n}=\mathrm{suc}{i}\right)$
37 2 bnj923 ${⊢}{n}\in {D}\to {n}\in \mathrm{\omega }$
38 1 37 bnj769 ${⊢}{\chi }\to {n}\in \mathrm{\omega }$
39 38 3ad2ant1 ${⊢}\left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\to {n}\in \mathrm{\omega }$
40 simp3 ${⊢}\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\to {n}=\mathrm{suc}{i}$
41 39 40 bnj240 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to \left({n}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{i}\right)$
42 vex ${⊢}{i}\in \mathrm{V}$
43 42 bnj216 ${⊢}{n}=\mathrm{suc}{i}\to {i}\in {n}$
44 43 adantl ${⊢}\left({n}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{i}\right)\to {i}\in {n}$
45 41 44 syl ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {i}\in {n}$
46 bnj658 ${⊢}\left({C}\in \mathrm{V}\wedge {f}Fn{n}\wedge {p}=\mathrm{suc}{n}\wedge {n}=\mathrm{suc}{i}\right)\to \left({C}\in \mathrm{V}\wedge {f}Fn{n}\wedge {p}=\mathrm{suc}{n}\right)$
47 46 anim1i ${⊢}\left(\left({C}\in \mathrm{V}\wedge {f}Fn{n}\wedge {p}=\mathrm{suc}{n}\wedge {n}=\mathrm{suc}{i}\right)\wedge {i}\in {n}\right)\to \left(\left({C}\in \mathrm{V}\wedge {f}Fn{n}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in {n}\right)$
48 df-bnj17 ${⊢}\left({C}\in \mathrm{V}\wedge {f}Fn{n}\wedge {p}=\mathrm{suc}{n}\wedge {i}\in {n}\right)↔\left(\left({C}\in \mathrm{V}\wedge {f}Fn{n}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in {n}\right)$
49 47 48 sylibr ${⊢}\left(\left({C}\in \mathrm{V}\wedge {f}Fn{n}\wedge {p}=\mathrm{suc}{n}\wedge {n}=\mathrm{suc}{i}\right)\wedge {i}\in {n}\right)\to \left({C}\in \mathrm{V}\wedge {f}Fn{n}\wedge {p}=\mathrm{suc}{n}\wedge {i}\in {n}\right)$
50 4 bnj945 ${⊢}\left({C}\in \mathrm{V}\wedge {f}Fn{n}\wedge {p}=\mathrm{suc}{n}\wedge {i}\in {n}\right)\to {G}\left({i}\right)={f}\left({i}\right)$
51 49 50 syl ${⊢}\left(\left({C}\in \mathrm{V}\wedge {f}Fn{n}\wedge {p}=\mathrm{suc}{n}\wedge {n}=\mathrm{suc}{i}\right)\wedge {i}\in {n}\right)\to {G}\left({i}\right)={f}\left({i}\right)$
52 36 45 51 syl2anc ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {G}\left({i}\right)={f}\left({i}\right)$
53 3 4 bnj958 ${⊢}{G}\left({i}\right)={f}\left({i}\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}{G}\left({i}\right)={f}\left({i}\right)$
54 53 bnj956 ${⊢}{G}\left({i}\right)={f}\left({i}\right)\to \bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)$
55 54 eqeq2d ${⊢}{G}\left({i}\right)={f}\left({i}\right)\to \left({G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)↔{G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
56 52 55 syl ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to \left({G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)↔{G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
57 30 56 mpbird ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$