Theorem bnj985

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). See bnj985v for a version with more disjoint variable conditions, not requiring ax-13 . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj985.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
	bnj985.6	No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
	bnj985.9	No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
	bnj985.11	$$⊢B=\left\{f|\exists n\in D\left(fFnn\wedge \phi \wedge \psi \right)\right\}$$
	bnj985.13	$$⊢G=f\cup \left\{⟨n,C⟩\right\}$$
Assertion	bnj985	Could not format assertion : No typesetting found for |- ( G e. B <-> E. p ch" ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj985.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
2		bnj985.6	Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
3		bnj985.9	Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
4		bnj985.11	$$⊢B=\left\{f|\exists n\in D\left(fFnn\wedge \phi \wedge \psi \right)\right\}$$
5		bnj985.13	$$⊢G=f\cup \left\{⟨n,C⟩\right\}$$
6	5	bnj918	$$⊢G\in \mathrm{V}$$
7	1 4	bnj984	$$⊢G\in \mathrm{V}\to \left(G\in B\leftrightarrow \underset{\dot{}}{[}G/f\underset{\dot{}}{]}\exists n\chi \right)$$
8	6 7	ax-mp	$$⊢G\in B\leftrightarrow \underset{\dot{}}{[}G/f\underset{\dot{}}{]}\exists n\chi$$
9		sbcex2	Could not format ( [. G / f ]. E. p ch' <-> E. p [. G / f ]. ch' ) : No typesetting found for |- ( [. G / f ]. E. p ch' <-> E. p [. G / f ]. ch' ) with typecode |-
10		nfv	$$⊢Ⅎp\chi$$
11	10	sb8e	$$⊢\exists n\chi \leftrightarrow \exists p\left[p/n\right]\chi$$
12		sbsbc	$$⊢\left[p/n\right]\chi \leftrightarrow \underset{\dot{}}{[}p/n\underset{\dot{}}{]}\chi$$
13	12	exbii	$$⊢\exists p\left[p/n\right]\chi \leftrightarrow \exists p\underset{\dot{}}{[}p/n\underset{\dot{}}{]}\chi$$
14	11 13	bitri	$$⊢\exists n\chi \leftrightarrow \exists p\underset{\dot{}}{[}p/n\underset{\dot{}}{]}\chi$$
15	14 2	bnj133	Could not format ( E. n ch <-> E. p ch' ) : No typesetting found for |- ( E. n ch <-> E. p ch' ) with typecode |-
16	15	sbcbii	Could not format ( [. G / f ]. E. n ch <-> [. G / f ]. E. p ch' ) : No typesetting found for |- ( [. G / f ]. E. n ch <-> [. G / f ]. E. p ch' ) with typecode |-
17	3	exbii	Could not format ( E. p ch" <-> E. p [. G / f ]. ch' ) : No typesetting found for |- ( E. p ch" <-> E. p [. G / f ]. ch' ) with typecode |-
18	9 16 17	3bitr4i	Could not format ( [. G / f ]. E. n ch <-> E. p ch" ) : No typesetting found for |- ( [. G / f ]. E. n ch <-> E. p ch" ) with typecode |-
19	8 18	bitri	Could not format ( G e. B <-> E. p ch" ) : No typesetting found for |- ( G e. B <-> E. p ch" ) with typecode |-