Theorem bnj207

Description: Technical lemma for bnj852 . 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	bnj207.1	$$⊢\chi \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \exists !f\left(fFnn\wedge \phi \wedge \psi \right)\right)$$
	bnj207.2	No typesetting found for |- ( ph' <-> [. M / n ]. ph ) with typecode |-
	bnj207.3	No typesetting found for |- ( ps' <-> [. M / n ]. ps ) with typecode |-
	bnj207.4	No typesetting found for |- ( ch' <-> [. M / n ]. ch ) with typecode |-
	bnj207.5	$$⊢M\in \mathrm{V}$$
Assertion	bnj207	Could not format assertion : No typesetting found for |- ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj207.1	$$⊢\chi \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \exists !f\left(fFnn\wedge \phi \wedge \psi \right)\right)$$
2		bnj207.2	Could not format ( ph' <-> [. M / n ]. ph ) : No typesetting found for |- ( ph' <-> [. M / n ]. ph ) with typecode |-
3		bnj207.3	Could not format ( ps' <-> [. M / n ]. ps ) : No typesetting found for |- ( ps' <-> [. M / n ]. ps ) with typecode |-
4		bnj207.4	Could not format ( ch' <-> [. M / n ]. ch ) : No typesetting found for |- ( ch' <-> [. M / n ]. ch ) with typecode |-
5		bnj207.5	$$⊢M\in \mathrm{V}$$
6	1	sbcbii	$$⊢\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\chi \leftrightarrow \underset{\dot{}}{[}M/n\underset{\dot{}}{]}\left(\left(RFrSeA\wedge x\in A\right)\to \exists !f\left(fFnn\wedge \phi \wedge \psi \right)\right)$$
7		nfv	$$⊢Ⅎn\left(RFrSeA\wedge x\in A\right)$$
8	7	sbc19.21g	$$⊢M\in \mathrm{V}\to \left(\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\left(\left(RFrSeA\wedge x\in A\right)\to \exists !f\left(fFnn\wedge \phi \wedge \psi \right)\right)\leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \underset{\dot{}}{[}M/n\underset{\dot{}}{]}\exists !f\left(fFnn\wedge \phi \wedge \psi \right)\right)\right)$$
9	5 8	ax-mp	$$⊢\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\left(\left(RFrSeA\wedge x\in A\right)\to \exists !f\left(fFnn\wedge \phi \wedge \psi \right)\right)\leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \underset{\dot{}}{[}M/n\underset{\dot{}}{]}\exists !f\left(fFnn\wedge \phi \wedge \psi \right)\right)$$
10	5	bnj89	$$⊢\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\exists !f\left(fFnn\wedge \phi \wedge \psi \right)\leftrightarrow \exists !f\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\left(fFnn\wedge \phi \wedge \psi \right)$$
11	5	bnj90	$$⊢\underset{\dot{}}{[}M/n\underset{\dot{}}{]}fFnn\leftrightarrow fFnM$$
12	11	bicomi	$$⊢fFnM\leftrightarrow \underset{\dot{}}{[}M/n\underset{\dot{}}{]}fFnn$$
13	12 2 3 5	bnj206	Could not format ( [. M / n ]. ( f Fn n /\ ph /\ ps ) <-> ( f Fn M /\ ph' /\ ps' ) ) : No typesetting found for |- ( [. M / n ]. ( f Fn n /\ ph /\ ps ) <-> ( f Fn M /\ ph' /\ ps' ) ) with typecode |-
14	13	eubii	Could not format ( E! f [. M / n ]. ( f Fn n /\ ph /\ ps ) <-> E! f ( f Fn M /\ ph' /\ ps' ) ) : No typesetting found for |- ( E! f [. M / n ]. ( f Fn n /\ ph /\ ps ) <-> E! f ( f Fn M /\ ph' /\ ps' ) ) with typecode |-
15	10 14	bitri	Could not format ( [. M / n ]. E! f ( f Fn n /\ ph /\ ps ) <-> E! f ( f Fn M /\ ph' /\ ps' ) ) : No typesetting found for |- ( [. M / n ]. E! f ( f Fn n /\ ph /\ ps ) <-> E! f ( f Fn M /\ ph' /\ ps' ) ) with typecode |-
16	15	imbi2i	Could not format ( ( ( R _FrSe A /\ x e. A ) -> [. M / n ]. E! f ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) -> [. M / n ]. E! f ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) ) with typecode |-
17	9 16	bitri	Could not format ( [. M / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( [. M / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) ) with typecode |-
18	6 17	bitri	Could not format ( [. M / n ]. ch <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( [. M / n ]. ch <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) ) with typecode |-
19	4 18	bitri	Could not format ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) ) with typecode |-