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

Metamath Proof Explorer

Theorem bnj934

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 bnj934.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
bnj934.4 No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
bnj934.7 No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
bnj934.50 ⊢ G ∈ V
Assertion bnj934 Could not format assertion : No typesetting found for |- ( ( ph /\ ( G ` (/) ) = ( f ` (/) ) ) -> ph" ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj934.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
2 bnj934.4 Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
3 bnj934.7 Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
4 bnj934.50 ⊢ G ∈ V
5 eqtr ⊢ G ⁡ ∅ = f ⁡ ∅ ∧ f ⁡ ∅ = pred X A R → G ⁡ ∅ = pred X A R
6 1 5 sylan2b ⊢ G ⁡ ∅ = f ⁡ ∅ ∧ φ → G ⁡ ∅ = pred X A R
7 vex ⊢ p ∈ V
8 1 2 7 bnj523 Could not format ( ph' <-> ( f ` (/) ) = _pred ( X , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( X , A , R ) ) with typecode |-
9 8 1 bitr4i Could not format ( ph' <-> ph ) : No typesetting found for |- ( ph' <-> ph ) with typecode |-
10 9 sbcbii Could not format ( [. G / f ]. ph' <-> [. G / f ]. ph ) : No typesetting found for |- ( [. G / f ]. ph' <-> [. G / f ]. ph ) with typecode |-
11 3 10 bitri Could not format ( ph" <-> [. G / f ]. ph ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph ) with typecode |-
12 1 11 4 bnj609 Could not format ( ph" <-> ( G ` (/) ) = _pred ( X , A , R ) ) : No typesetting found for |- ( ph" <-> ( G ` (/) ) = _pred ( X , A , R ) ) with typecode |-
13 6 12 sylibr Could not format ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph ) -> ph" ) : No typesetting found for |- ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph ) -> ph" ) with typecode |-
14 13 ancoms Could not format ( ( ph /\ ( G ` (/) ) = ( f ` (/) ) ) -> ph" ) : No typesetting found for |- ( ( ph /\ ( G ` (/) ) = ( f ` (/) ) ) -> ph" ) with typecode |-