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

Metamath Proof Explorer

Theorem bnj124

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) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypotheses bnj124.1 ⊢ F = ∅ pred x A R
bnj124.2 No typesetting found for |- ( ph" <-> [. F / f ]. ph' ) with typecode |-
bnj124.3 No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
bnj124.4 No typesetting found for |- ( ze" <-> [. F / f ]. ze' ) with typecode |-
bnj124.5 No typesetting found for |- ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
Assertion bnj124 Could not format assertion : No typesetting found for |- ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj124.1 ⊢ F = ∅ pred x A R
2 bnj124.2 Could not format ( ph" <-> [. F / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. F / f ]. ph' ) with typecode |-
3 bnj124.3 Could not format ( ps" <-> [. F / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
4 bnj124.4 Could not format ( ze" <-> [. F / f ]. ze' ) : No typesetting found for |- ( ze" <-> [. F / f ]. ze' ) with typecode |-
5 bnj124.5 Could not format ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
6 5 sbcbii Could not format ( [. F / f ]. ze' <-> [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( [. F / f ]. ze' <-> [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
7 1 bnj95 ⊢ F ∈ V
8 nfv ⊢ Ⅎ f R FrSe A ∧ x ∈ A
9 8 sbc19.21g Could not format ( F e. _V -> ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) ) ) : No typesetting found for |- ( F e. _V -> ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) ) ) with typecode |-
10 7 9 ax-mp Could not format ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
11 fneq1 ⊢ f = z → f Fn 1 𝑜 ↔ z Fn 1 𝑜
12 fneq1 ⊢ z = F → z Fn 1 𝑜 ↔ F Fn 1 𝑜
13 11 12 sbcie2g ⊢ F ∈ V → [˙F / f]˙ f Fn 1 𝑜 ↔ F Fn 1 𝑜
14 7 13 ax-mp ⊢ [˙F / f]˙ f Fn 1 𝑜 ↔ F Fn 1 𝑜
15 14 bicomi ⊢ F Fn 1 𝑜 ↔ [˙F / f]˙ f Fn 1 𝑜
16 15 2 3 7 bnj206 Could not format ( [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) <-> ( F Fn 1o /\ ph" /\ ps" ) ) : No typesetting found for |- ( [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) <-> ( F Fn 1o /\ ph" /\ ps" ) ) with typecode |-
17 16 imbi2i Could not format ( ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) with typecode |-
18 6 10 17 3bitri Could not format ( [. F / f ]. ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( [. F / f ]. ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) with typecode |-
19 4 18 bitri Could not format ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) with typecode |-