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=predxAR
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=predxAR
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 FV
8 nfv fRFrSeAxA
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=zfFn1𝑜zFn1𝑜
12 fneq1 z=FzFn1𝑜FFn1𝑜
13 11 12 sbcie2g FV[˙F/f]˙fFn1𝑜FFn1𝑜
14 7 13 ax-mp [˙F/f]˙fFn1𝑜FFn1𝑜
15 14 bicomi FFn1𝑜[˙F/f]˙fFn1𝑜
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 |-