# Metamath Proof Explorer

## Theorem bnj546

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 bnj546.1 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
bnj546.2 No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
bnj546.3 ${⊢}{\sigma }↔\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in {m}\right)$
bnj546.4 No typesetting found for |- ( ph' <-> ( f  (/) ) = _pred ( x , A , R ) ) with typecode |-
bnj546.5 No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f  suc i ) = U_ y e. ( f  i ) _pred ( y , A , R ) ) ) with typecode |-
Assertion bnj546 ${⊢}\left({R}FrSe{A}\wedge {\tau }\wedge {\sigma }\right)\to \bigcup _{{y}\in {f}\left({p}\right)}pred\left({y},{A},{R}\right)\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 bnj546.1 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
2 bnj546.2 Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
3 bnj546.3 ${⊢}{\sigma }↔\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in {m}\right)$
4 bnj546.4 Could not format ( ph' <-> ( f  (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f  (/) ) = _pred ( x , A , R ) ) with typecode |-
5 bnj546.5 Could not format ( ps' <-> A. i e. _om ( suc i e. m -> ( f  suc i ) = U_ y e. ( f  i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f  suc i ) = U_ y e. ( f  i ) _pred ( y , A , R ) ) ) with typecode |-
6 3simpc Could not format ( ( f Fn m /\ ph' /\ ps' ) -> ( ph' /\ ps' ) ) : No typesetting found for |- ( ( f Fn m /\ ph' /\ ps' ) -> ( ph' /\ ps' ) ) with typecode |-
7 2 6 sylbi Could not format ( ta -> ( ph' /\ ps' ) ) : No typesetting found for |- ( ta -> ( ph' /\ ps' ) ) with typecode |-
8 1 bnj923 ${⊢}{m}\in {D}\to {m}\in \mathrm{\omega }$
9 8 3ad2ant1 ${⊢}\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in {m}\right)\to {m}\in \mathrm{\omega }$
10 simp3 ${⊢}\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in {m}\right)\to {p}\in {m}$
11 9 10 jca ${⊢}\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in {m}\right)\to \left({m}\in \mathrm{\omega }\wedge {p}\in {m}\right)$
12 3 11 sylbi ${⊢}{\sigma }\to \left({m}\in \mathrm{\omega }\wedge {p}\in {m}\right)$
13 7 12 anim12i Could not format ( ( ta /\ si ) -> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) ) : No typesetting found for |- ( ( ta /\ si ) -> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) ) with typecode |-
14 bnj256 Could not format ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) ) : No typesetting found for |- ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) ) with typecode |-
15 13 14 sylibr Could not format ( ( ta /\ si ) -> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) : No typesetting found for |- ( ( ta /\ si ) -> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) with typecode |-
16 15 anim2i Could not format ( ( R _FrSe A /\ ( ta /\ si ) ) -> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) ) : No typesetting found for |- ( ( R _FrSe A /\ ( ta /\ si ) ) -> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) ) with typecode |-
17 16 3impb Could not format ( ( R _FrSe A /\ ta /\ si ) -> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ si ) -> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) ) with typecode |-
18 biid Could not format ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) : No typesetting found for |- ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) with typecode |-
19 4 5 18 bnj518 Could not format ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) -> A. y e. ( f  p ) _pred ( y , A , R ) e. _V ) : No typesetting found for |- ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) -> A. y e. ( f ` p ) _pred ( y , A , R ) e. _V ) with typecode |-
20 fvex ${⊢}{f}\left({p}\right)\in \mathrm{V}$
21 iunexg ${⊢}\left({f}\left({p}\right)\in \mathrm{V}\wedge \forall {y}\in {f}\left({p}\right)\phantom{\rule{.4em}{0ex}}pred\left({y},{A},{R}\right)\in \mathrm{V}\right)\to \bigcup _{{y}\in {f}\left({p}\right)}pred\left({y},{A},{R}\right)\in \mathrm{V}$
22 20 21 mpan ${⊢}\forall {y}\in {f}\left({p}\right)\phantom{\rule{.4em}{0ex}}pred\left({y},{A},{R}\right)\in \mathrm{V}\to \bigcup _{{y}\in {f}\left({p}\right)}pred\left({y},{A},{R}\right)\in \mathrm{V}$
23 17 19 22 3syl ${⊢}\left({R}FrSe{A}\wedge {\tau }\wedge {\sigma }\right)\to \bigcup _{{y}\in {f}\left({p}\right)}pred\left({y},{A},{R}\right)\in \mathrm{V}$