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

Metamath Proof Explorer

Theorem bnj156

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj156.1 No typesetting found for |- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
bnj156.2 No typesetting found for |- ( ze1 <-> [. g / f ]. ze0 ) with typecode |-
bnj156.3 No typesetting found for |- ( ph1 <-> [. g / f ]. ph' ) with typecode |-
bnj156.4 No typesetting found for |- ( ps1 <-> [. g / f ]. ps' ) with typecode |-
Assertion bnj156 Could not format assertion : No typesetting found for |- ( ze1 <-> ( g Fn 1o /\ ph1 /\ ps1 ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj156.1 Could not format ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) : No typesetting found for |- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
2 bnj156.2 Could not format ( ze1 <-> [. g / f ]. ze0 ) : No typesetting found for |- ( ze1 <-> [. g / f ]. ze0 ) with typecode |-
3 bnj156.3 Could not format ( ph1 <-> [. g / f ]. ph' ) : No typesetting found for |- ( ph1 <-> [. g / f ]. ph' ) with typecode |-
4 bnj156.4 Could not format ( ps1 <-> [. g / f ]. ps' ) : No typesetting found for |- ( ps1 <-> [. g / f ]. ps' ) with typecode |-
5 1 sbcbii Could not format ( [. g / f ]. ze0 <-> [. g / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) : No typesetting found for |- ( [. g / f ]. ze0 <-> [. g / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
6 sbc3an Could not format ( [. g / f ]. ( f Fn 1o /\ ph' /\ ps' ) <-> ( [. g / f ]. f Fn 1o /\ [. g / f ]. ph' /\ [. g / f ]. ps' ) ) : No typesetting found for |- ( [. g / f ]. ( f Fn 1o /\ ph' /\ ps' ) <-> ( [. g / f ]. f Fn 1o /\ [. g / f ]. ph' /\ [. g / f ]. ps' ) ) with typecode |-
7 bnj62 ⊢ [˙g / f]˙ f Fn 1 𝑜 ↔ g Fn 1 𝑜
8 3 bicomi Could not format ( [. g / f ]. ph' <-> ph1 ) : No typesetting found for |- ( [. g / f ]. ph' <-> ph1 ) with typecode |-
9 4 bicomi Could not format ( [. g / f ]. ps' <-> ps1 ) : No typesetting found for |- ( [. g / f ]. ps' <-> ps1 ) with typecode |-
10 7 8 9 3anbi123i Could not format ( ( [. g / f ]. f Fn 1o /\ [. g / f ]. ph' /\ [. g / f ]. ps' ) <-> ( g Fn 1o /\ ph1 /\ ps1 ) ) : No typesetting found for |- ( ( [. g / f ]. f Fn 1o /\ [. g / f ]. ph' /\ [. g / f ]. ps' ) <-> ( g Fn 1o /\ ph1 /\ ps1 ) ) with typecode |-
11 6 10 bitri Could not format ( [. g / f ]. ( f Fn 1o /\ ph' /\ ps' ) <-> ( g Fn 1o /\ ph1 /\ ps1 ) ) : No typesetting found for |- ( [. g / f ]. ( f Fn 1o /\ ph' /\ ps' ) <-> ( g Fn 1o /\ ph1 /\ ps1 ) ) with typecode |-
12 5 11 bitri Could not format ( [. g / f ]. ze0 <-> ( g Fn 1o /\ ph1 /\ ps1 ) ) : No typesetting found for |- ( [. g / f ]. ze0 <-> ( g Fn 1o /\ ph1 /\ ps1 ) ) with typecode |-
13 2 12 bitri Could not format ( ze1 <-> ( g Fn 1o /\ ph1 /\ ps1 ) ) : No typesetting found for |- ( ze1 <-> ( g Fn 1o /\ ph1 /\ ps1 ) ) with typecode |-