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	$$⊢\underset{\dot{}}{[}g/f\underset{\dot{}}{]}fFn{1}_{𝑜}\leftrightarrow gFn{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 |-