Theorem bnj1040

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	bnj1040.1	No typesetting found for |- ( ph' <-> [. j / i ]. ph ) with typecode |-
	bnj1040.2	No typesetting found for |- ( ps' <-> [. j / i ]. ps ) with typecode |-
	bnj1040.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
	bnj1040.4	No typesetting found for |- ( ch' <-> [. j / i ]. ch ) with typecode |-
Assertion	bnj1040	Could not format assertion : No typesetting found for |- ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj1040.1	Could not format ( ph' <-> [. j / i ]. ph ) : No typesetting found for |- ( ph' <-> [. j / i ]. ph ) with typecode |-
2		bnj1040.2	Could not format ( ps' <-> [. j / i ]. ps ) : No typesetting found for |- ( ps' <-> [. j / i ]. ps ) with typecode |-
3		bnj1040.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
4		bnj1040.4	Could not format ( ch' <-> [. j / i ]. ch ) : No typesetting found for |- ( ch' <-> [. j / i ]. ch ) with typecode |-
5	3	sbcbii	$$⊢\underset{\dot{}}{[}j/i\underset{\dot{}}{]}\chi \leftrightarrow \underset{\dot{}}{[}j/i\underset{\dot{}}{]}\left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
6		df-bnj17	$$⊢\left(\underset{\dot{}}{[}j/i\underset{\dot{}}{]}n\in D\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}fFnn\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\left(\underset{\dot{}}{[}j/i\underset{\dot{}}{]}n\in D\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}fFnn\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}\phi \right)\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}\psi \right)$$
7		vex	$$⊢j\in \mathrm{V}$$
8	7	bnj525	$$⊢\underset{\dot{}}{[}j/i\underset{\dot{}}{]}n\in D\leftrightarrow n\in D$$
9	8	bicomi	$$⊢n\in D\leftrightarrow \underset{\dot{}}{[}j/i\underset{\dot{}}{]}n\in D$$
10	7	bnj525	$$⊢\underset{\dot{}}{[}j/i\underset{\dot{}}{]}fFnn\leftrightarrow fFnn$$
11	10	bicomi	$$⊢fFnn\leftrightarrow \underset{\dot{}}{[}j/i\underset{\dot{}}{]}fFnn$$
12	9 11 1 2	bnj887	Could not format ( ( n e. D /\ f Fn n /\ ph' /\ ps' ) <-> ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph /\ [. j / i ]. ps ) ) : No typesetting found for |- ( ( n e. D /\ f Fn n /\ ph' /\ ps' ) <-> ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph /\ [. j / i ]. ps ) ) with typecode |-
13		df-bnj17	$$⊢\left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)\leftrightarrow \left(\left(n\in D\wedge fFnn\wedge \phi \right)\wedge \psi \right)$$
14	13	sbcbii	$$⊢\underset{\dot{}}{[}j/i\underset{\dot{}}{]}\left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)\leftrightarrow \underset{\dot{}}{[}j/i\underset{\dot{}}{]}\left(\left(n\in D\wedge fFnn\wedge \phi \right)\wedge \psi \right)$$
15		sbcan	$$⊢\underset{\dot{}}{[}j/i\underset{\dot{}}{]}\left(\left(n\in D\wedge fFnn\wedge \phi \right)\wedge \psi \right)\leftrightarrow \left(\underset{\dot{}}{[}j/i\underset{\dot{}}{]}\left(n\in D\wedge fFnn\wedge \phi \right)\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}\psi \right)$$
16		sbc3an	$$⊢\underset{\dot{}}{[}j/i\underset{\dot{}}{]}\left(n\in D\wedge fFnn\wedge \phi \right)\leftrightarrow \left(\underset{\dot{}}{[}j/i\underset{\dot{}}{]}n\in D\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}fFnn\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}\phi \right)$$
17	16	anbi1i	$$⊢\left(\underset{\dot{}}{[}j/i\underset{\dot{}}{]}\left(n\in D\wedge fFnn\wedge \phi \right)\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\left(\underset{\dot{}}{[}j/i\underset{\dot{}}{]}n\in D\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}fFnn\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}\phi \right)\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}\psi \right)$$
18	14 15 17	3bitri	$$⊢\underset{\dot{}}{[}j/i\underset{\dot{}}{]}\left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)\leftrightarrow \left(\left(\underset{\dot{}}{[}j/i\underset{\dot{}}{]}n\in D\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}fFnn\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}\phi \right)\wedge \underset{\dot{}}{[}j/i\underset{\dot{}}{]}\psi \right)$$
19	6 12 18	3bitr4ri	Could not format ( [. j / i ]. ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) : No typesetting found for |- ( [. j / i ]. ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) with typecode |-
20	4 5 19	3bitri	Could not format ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) : No typesetting found for |- ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) with typecode |-