This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 |-