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

Metamath Proof Explorer

Theorem bnj155

Description: Technical lemma for bnj153 . 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 bnj155.1 No typesetting found for |- ( ps1 <-> [. g / f ]. ps' ) with typecode |-
bnj155.2 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 |-
Assertion bnj155 Could not format assertion : No typesetting found for |- ( ps1 <-> A. i e. _om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj155.1 Could not format ( ps1 <-> [. g / f ]. ps' ) : No typesetting found for |- ( ps1 <-> [. g / f ]. ps' ) with typecode |-
2 bnj155.2 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 |-
3 2 sbcbii Could not format ( [. g / f ]. ps' <-> [. g / f ]. A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( [. g / f ]. ps' <-> [. g / f ]. A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
4 vex ⊢ g ∈ V
5 fveq1 ⊢ f = g → f ⁡ suc ⁡ i = g ⁡ suc ⁡ i
6 fveq1 ⊢ f = g → f ⁡ i = g ⁡ i
7 6 iuneq1d ⊢ f = g → ⋃ y ∈ f ⁡ i pred y A R = ⋃ y ∈ g ⁡ i pred y A R
8 5 7 eqeq12d ⊢ f = g → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ↔ g ⁡ suc ⁡ i = ⋃ y ∈ g ⁡ i pred y A R
9 8 imbi2d ⊢ f = g → suc ⁡ i ∈ 1 𝑜 → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ↔ suc ⁡ i ∈ 1 𝑜 → g ⁡ suc ⁡ i = ⋃ y ∈ g ⁡ i pred y A R
10 9 ralbidv ⊢ f = g → ∀ i ∈ ω suc ⁡ i ∈ 1 𝑜 → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ↔ ∀ i ∈ ω suc ⁡ i ∈ 1 𝑜 → g ⁡ suc ⁡ i = ⋃ y ∈ g ⁡ i pred y A R
11 4 10 sbcie ⊢ [˙g / f]˙ ∀ i ∈ ω suc ⁡ i ∈ 1 𝑜 → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ↔ ∀ i ∈ ω suc ⁡ i ∈ 1 𝑜 → g ⁡ suc ⁡ i = ⋃ y ∈ g ⁡ i pred y A R
12 1 3 11 3bitri Could not format ( ps1 <-> A. i e. _om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps1 <-> A. i e. _om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) with typecode |-