bnj873

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	bnj873.4	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
	bnj873.7	No typesetting found for \|- ( ph' <-> [. g / f ]. ph ) with typecode \|-
	bnj873.8	No typesetting found for \|- ( ps' <-> [. g / f ]. ps ) with typecode \|-
Assertion	bnj873	Could not format assertion : No typesetting found for \|- B = { g \| E. n e. D ( g Fn n /\ ph' /\ ps' ) } with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bnj873.4	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
2		bnj873.7	Could not format ( ph' <-> [. g / f ]. ph ) : No typesetting found for \|- ( ph' <-> [. g / f ]. ph ) with typecode \|-
3		bnj873.8	Could not format ( ps' <-> [. g / f ]. ps ) : No typesetting found for \|- ( ps' <-> [. g / f ]. ps ) with typecode \|-
4		nfv	$⊢ Ⅎ g \exists n \in D (f Fn n \land φ \land ψ)$
5		nfcv	$⊢ \underline{Ⅎ} f D$
6		nfv	$⊢ Ⅎ f g Fn n$
7		nfsbc1v	$⊢ Ⅎ f \underset{˙}{[} g / f \underset{˙}{]} φ$
8	2 7	nfxfr	Could not format F/ f ph' : No typesetting found for \|- F/ f ph' with typecode \|-
9		nfsbc1v	$⊢ Ⅎ f \underset{˙}{[} g / f \underset{˙}{]} ψ$
10	3 9	nfxfr	Could not format F/ f ps' : No typesetting found for \|- F/ f ps' with typecode \|-
11	6 8 10	nf3an	Could not format F/ f ( g Fn n /\ ph' /\ ps' ) : No typesetting found for \|- F/ f ( g Fn n /\ ph' /\ ps' ) with typecode \|-
12	5 11	nfrexw	Could not format F/ f E. n e. D ( g Fn n /\ ph' /\ ps' ) : No typesetting found for \|- F/ f E. n e. D ( g Fn n /\ ph' /\ ps' ) with typecode \|-
13		fneq1	$⊢ f = g \to (f Fn n \leftrightarrow g Fn n)$
14		sbceq1a	$⊢ f = g \to (φ \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} φ)$
15	14 2	bitr4di	Could not format ( f = g -> ( ph <-> ph' ) ) : No typesetting found for \|- ( f = g -> ( ph <-> ph' ) ) with typecode \|-
16		sbceq1a	$⊢ f = g \to (ψ \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} ψ)$
17	16 3	bitr4di	Could not format ( f = g -> ( ps <-> ps' ) ) : No typesetting found for \|- ( f = g -> ( ps <-> ps' ) ) with typecode \|-
18	13 15 17	3anbi123d	Could not format ( f = g -> ( ( f Fn n /\ ph /\ ps ) <-> ( g Fn n /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( f = g -> ( ( f Fn n /\ ph /\ ps ) <-> ( g Fn n /\ ph' /\ ps' ) ) ) with typecode \|-
19	18	rexbidv	Could not format ( f = g -> ( E. n e. D ( f Fn n /\ ph /\ ps ) <-> E. n e. D ( g Fn n /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( f = g -> ( E. n e. D ( f Fn n /\ ph /\ ps ) <-> E. n e. D ( g Fn n /\ ph' /\ ps' ) ) ) with typecode \|-
20	4 12 19	cbvabw	Could not format { f \| E. n e. D ( f Fn n /\ ph /\ ps ) } = { g \| E. n e. D ( g Fn n /\ ph' /\ ps' ) } : No typesetting found for \|- { f \| E. n e. D ( f Fn n /\ ph /\ ps ) } = { g \| E. n e. D ( g Fn n /\ ph' /\ ps' ) } with typecode \|-
21	1 20	eqtri	Could not format B = { g \| E. n e. D ( g Fn n /\ ph' /\ ps' ) } : No typesetting found for \|- B = { g \| E. n e. D ( g Fn n /\ ph' /\ ps' ) } with typecode \|-

Metamath Proof Explorer

Theorem bnj873

Proof