Metamath Proof Explorer


Theorem bnj126

Description: Technical lemma for bnj150 . 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 bnj126.1 ψ i ω suc i n f suc i = y f i pred y A R
bnj126.2 No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
bnj126.3 No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
bnj126.4 F = pred x A R
Assertion bnj126 Could not format assertion : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj126.1 ψ i ω suc i n f suc i = y f i pred y A R
2 bnj126.2 Could not format ( ps' <-> [. 1o / n ]. ps ) : No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
3 bnj126.3 Could not format ( ps" <-> [. F / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
4 bnj126.4 F = pred x A R
5 2 sbcbii Could not format ( [. F / f ]. ps' <-> [. F / f ]. [. 1o / n ]. ps ) : No typesetting found for |- ( [. F / f ]. ps' <-> [. F / f ]. [. 1o / n ]. ps ) with typecode |-
6 4 bnj95 F V
7 1 6 bnj106 [˙F / f]˙ [˙ 1 𝑜 / n]˙ ψ i ω suc i 1 𝑜 F suc i = y F i pred y A R
8 3 5 7 3bitri Could not format ( ps" <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) with typecode |-