bnj1090

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	bnj1090.9	$⊢ η \leftrightarrow ((f \in K \land i \in dom f) \to f (i) \subseteq B)$
	bnj1090.10	$⊢ ρ \leftrightarrow \forall j \in n (j E i \to \underset{˙}{[} j / i \underset{˙}{]} η)$
	bnj1090.17	No typesetting found for \|- ( et' <-> [. j / i ]. et ) with typecode \|-
	bnj1090.18	No typesetting found for \|- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) with typecode \|-
	bnj1090.19	No typesetting found for \|- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) with typecode \|-
	bnj1090.28	No typesetting found for \|- ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) with typecode \|-
Assertion	bnj1090	$⊢ (θ \land τ \land χ \land ζ) \to \forall i \in n (ρ \to η)$

Proof

Step	Hyp	Ref	Expression
1		bnj1090.9	$⊢ η \leftrightarrow ((f \in K \land i \in dom f) \to f (i) \subseteq B)$
2		bnj1090.10	$⊢ ρ \leftrightarrow \forall j \in n (j E i \to \underset{˙}{[} j / i \underset{˙}{]} η)$
3		bnj1090.17	Could not format ( et' <-> [. j / i ]. et ) : No typesetting found for \|- ( et' <-> [. j / i ]. et ) with typecode \|-
4		bnj1090.18	Could not format ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) : No typesetting found for \|- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) with typecode \|-
5		bnj1090.19	Could not format ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) : No typesetting found for \|- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) with typecode \|-
6		bnj1090.28	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 \|-
7		impexp	$⊢ ((i \in n \land σ) \to η) \leftrightarrow (i \in n \to (σ \to η))$
8	7	exbii	$⊢ \exists j ((i \in n \land σ) \to η) \leftrightarrow \exists j (i \in n \to (σ \to η))$
9	4	imbi1i	Could not format ( ( si -> et ) <-> ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for \|- ( ( si -> et ) <-> ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode \|-
10	9	exbii	Could not format ( E. j ( si -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for \|- ( E. j ( si -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode \|-
11	10	imbi2i	Could not format ( ( i e. n -> E. j ( si -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) ) : No typesetting found for \|- ( ( i e. n -> E. j ( si -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) ) with typecode \|-
12		19.37v	$⊢ \exists j (i \in n \to (σ \to η)) \leftrightarrow (i \in n \to \exists j (σ \to η))$
13	2	bnj115	$⊢ ρ \leftrightarrow \forall j ((j \in n \land j E i) \to \underset{˙}{[} j / i \underset{˙}{]} η)$
14	3	imbi2i	Could not format ( ( ( j e. n /\ j _E i ) -> et' ) <-> ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) ) : No typesetting found for \|- ( ( ( j e. n /\ j _E i ) -> et' ) <-> ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) ) with typecode \|-
15	14	albii	Could not format ( A. j ( ( j e. n /\ j _E i ) -> et' ) <-> A. j ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) ) : No typesetting found for \|- ( A. j ( ( j e. n /\ j _E i ) -> et' ) <-> A. j ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) ) with typecode \|-
16	13 15	bitr4i	Could not format ( rh <-> A. j ( ( j e. n /\ j _E i ) -> et' ) ) : No typesetting found for \|- ( rh <-> A. j ( ( j e. n /\ j _E i ) -> et' ) ) with typecode \|-
17	16	imbi1i	Could not format ( ( rh -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for \|- ( ( rh -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode \|-
18		19.36v	Could not format ( E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for \|- ( E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode \|-
19	17 18	bitr4i	Could not format ( ( rh -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for \|- ( ( rh -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode \|-
20	19	imbi2i	Could not format ( ( i e. n -> ( rh -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) ) : No typesetting found for \|- ( ( i e. n -> ( rh -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) ) with typecode \|-
21	11 12 20	3bitr4i	$⊢ \exists j (i \in n \to (σ \to η)) \leftrightarrow (i \in n \to (ρ \to η))$
22	8 21	bitr2i	$⊢ (i \in n \to (ρ \to η)) \leftrightarrow \exists j ((i \in n \land σ) \to η)$
23		impexp	$⊢ (((i \in n \land σ) \land (f \in K \land i \in dom f)) \to f (i) \subseteq B) \leftrightarrow ((i \in n \land σ) \to ((f \in K \land i \in dom f) \to f (i) \subseteq B))$
24		bnj256	$⊢ (i \in n \land σ \land f \in K \land i \in dom f) \leftrightarrow ((i \in n \land σ) \land (f \in K \land i \in dom f))$
25	24	imbi1i	$⊢ ((i \in n \land σ \land f \in K \land i \in dom f) \to f (i) \subseteq B) \leftrightarrow (((i \in n \land σ) \land (f \in K \land i \in dom f)) \to f (i) \subseteq B)$
26	1	imbi2i	$⊢ ((i \in n \land σ) \to η) \leftrightarrow ((i \in n \land σ) \to ((f \in K \land i \in dom f) \to f (i) \subseteq B))$
27	23 25 26	3bitr4i	$⊢ ((i \in n \land σ \land f \in K \land i \in dom f) \to f (i) \subseteq B) \leftrightarrow ((i \in n \land σ) \to η)$
28	22 27	bnj133	$⊢ (i \in n \to (ρ \to η)) \leftrightarrow \exists j ((i \in n \land σ \land f \in K \land i \in dom f) \to f (i) \subseteq B)$
29	28	albii	$⊢ \forall i (i \in n \to (ρ \to η)) \leftrightarrow \forall i \exists j ((i \in n \land σ \land f \in K \land i \in dom f) \to f (i) \subseteq B)$
30		df-ral	$⊢ \forall i \in n (ρ \to η) \leftrightarrow \forall i (i \in n \to (ρ \to η))$
31	5	imbi1i	Could not format ( ( ph0 -> ( f ` i ) C_ B ) <-> ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) : No typesetting found for \|- ( ( ph0 -> ( f ` i ) C_ B ) <-> ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) with typecode \|-
32	31	exbii	Could not format ( E. j ( ph0 -> ( f ` i ) C_ B ) <-> E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) : No typesetting found for \|- ( E. j ( ph0 -> ( f ` i ) C_ B ) <-> E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) with typecode \|-
33	32	albii	Could not format ( A. i E. j ( ph0 -> ( f ` i ) C_ B ) <-> A. i E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) : No typesetting found for \|- ( A. i E. j ( ph0 -> ( f ` i ) C_ B ) <-> A. i E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) with typecode \|-
34	29 30 33	3bitr4i	Could not format ( A. i e. n ( rh -> et ) <-> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) : No typesetting found for \|- ( A. i e. n ( rh -> et ) <-> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) with typecode \|-
35	6 34	sylibr	$⊢ (θ \land τ \land χ \land ζ) \to \forall i \in n (ρ \to η)$

Metamath Proof Explorer

Theorem bnj1090

Proof