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	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	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 = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
	bnj985.13	$⊢ G = f \cup \{⟨n, C⟩\}$
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	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
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 = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
5		bnj985.13	$⊢ G = f \cup \{⟨n, C⟩\}$
6	5	bnj918	$⊢ G \in V$
7	1 4	bnj984	$⊢ G \in V \to (G \in B \leftrightarrow \underset{˙}{[} G / f \underset{˙}{]} \exists n χ)$
8	6 7	ax-mp	$⊢ G \in B \leftrightarrow \underset{˙}{[} G / f \underset{˙}{]} \exists n χ$
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 χ$
11	10	sb8e	$⊢ \exists n χ \leftrightarrow \exists p [p/ n] χ$
12		sbsbc	$⊢ [p/ n] χ \leftrightarrow \underset{˙}{[} p / n \underset{˙}{]} χ$
13	12	exbii	$⊢ \exists p [p/ n] χ \leftrightarrow \exists p \underset{˙}{[} p / n \underset{˙}{]} χ$
14	11 13	bitri	$⊢ \exists n χ \leftrightarrow \exists p \underset{˙}{[} p / n \underset{˙}{]} χ$
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 \|-

Metamath Proof Explorer

Theorem bnj985

Proof