Theorem bnj1093

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	bnj1093.1	No typesetting found for |- E. j ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B ) with typecode |-
	bnj1093.2	$$⊢\psi \leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in n\to f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$
	bnj1093.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
Assertion	bnj1093	Could not format assertion : No typesetting found for |- ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj1093.1	Could not format E. j ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B ) : No typesetting found for |- E. j ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B ) with typecode |-
2		bnj1093.2	$$⊢\psi \leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in n\to f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$
3		bnj1093.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
4	2	bnj1095	$$⊢\psi \to \forall i\psi$$
5	4 3	bnj1096	$$⊢\chi \to \forall i\chi$$
6	5	bnj1350	$$⊢\left(\theta \wedge \tau \wedge \chi \right)\to \forall i\left(\theta \wedge \tau \wedge \chi \right)$$
7		impexp	Could not format ( ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B ) <-> ( ( th /\ ta /\ ch ) -> ( ph0 -> ( f ` i ) C_ B ) ) ) : No typesetting found for |- ( ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B ) <-> ( ( th /\ ta /\ ch ) -> ( ph0 -> ( f ` i ) C_ B ) ) ) with typecode |-
8	7	exbii	Could not format ( E. j ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B ) <-> E. j ( ( th /\ ta /\ ch ) -> ( ph0 -> ( f ` i ) C_ B ) ) ) : No typesetting found for |- ( E. j ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B ) <-> E. j ( ( th /\ ta /\ ch ) -> ( ph0 -> ( f ` i ) C_ B ) ) ) with typecode |-
9	1 8	mpbi	Could not format E. j ( ( th /\ ta /\ ch ) -> ( ph0 -> ( f ` i ) C_ B ) ) : No typesetting found for |- E. j ( ( th /\ ta /\ ch ) -> ( ph0 -> ( f ` i ) C_ B ) ) with typecode |-
10	9	19.37iv	Could not format ( ( th /\ ta /\ ch ) -> E. j ( ph0 -> ( f ` i ) C_ B ) ) : No typesetting found for |- ( ( th /\ ta /\ ch ) -> E. j ( ph0 -> ( f ` i ) C_ B ) ) with typecode |-
11	6 10	alrimih	Could not format ( ( th /\ ta /\ ch ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) : No typesetting found for |- ( ( th /\ ta /\ ch ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) with typecode |-
12	11	bnj721	Could not format ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) : No typesetting found for |- ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) with typecode |-