Theorem bnj1090 31047

Description: Technical lemma for bnj69 31078. 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.)

Hypotheses

Ref	Expression
bnj1090.9	|- ( et <-> ( ( f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) )
bnj1090.10	|- ( rh <-> A. j e. n ( j _E i -> [. j / i ]. et ) )
bnj1090.17	|- ( et' <-> [. j / i ]. et )
bnj1090.18	|- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) )
bnj1090.19	|- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) )
bnj1090.28	|- ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) )

Assertion

Ref	Expression
bnj1090	|- ( ( th /\ ta /\ ch /\ ze ) -> A. i e. n ( rh -> et ) )

Distinct variable groups:   et, j   i, j   j, n

Allowed substitution hints:   ch( f, i, j, n)   th( f, i, j, n)   ta( f, i, j, n)   et( f, i, n)   ze( f, i, j, n)   si( f, i, j, n)   rh( f, i, j, n)   B( f, i, j, n)   K( f, i, j, n)   et'( f, i, j, n)   ph0( f, i, j, n)

Proof of Theorem bnj1090

Step	Hyp	Ref	Expression
1		bnj1090.28	. 2 |- ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) )
2		impexp 462	. . . . . . 7 |- ( ( ( i e. n /\ si ) -> et ) <-> ( i e. n -> ( si -> et ) ) )
3	2	exbii 1774	. . . . . 6 |- ( E. j ( ( i e. n /\ si ) -> et ) <-> E. j ( i e. n -> ( si -> et ) ) )
4		bnj1090.18	. . . . . . . . . 10 |- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) )
5	4	imbi1i 339	. . . . . . . . 9 |- ( ( si -> et ) <-> ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) )
6	5	exbii 1774	. . . . . . . 8 |- ( E. j ( si -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) )
7	6	imbi2i 326	. . . . . . 7 |- ( ( i e. n -> E. j ( si -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) )
8		19.37v 1910	. . . . . . 7 |- ( E. j ( i e. n -> ( si -> et ) ) <-> ( i e. n -> E. j ( si -> et ) ) )
9		bnj1090.10	. . . . . . . . . . . 12 |- ( rh <-> A. j e. n ( j _E i -> [. j / i ]. et ) )
10	9	bnj115 30791	. . . . . . . . . . 11 |- ( rh <-> A. j ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) )
11		bnj1090.17	. . . . . . . . . . . . 13 |- ( et' <-> [. j / i ]. et )
12	11	imbi2i 326	. . . . . . . . . . . 12 |- ( ( ( j e. n /\ j _E i ) -> et' ) <-> ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) )
13	12	albii 1747	. . . . . . . . . . 11 |- ( A. j ( ( j e. n /\ j _E i ) -> et' ) <-> A. j ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) )
14	10, 13	bitr4i 267	. . . . . . . . . 10 |- ( rh <-> A. j ( ( j e. n /\ j _E i ) -> et' ) )
15	14	imbi1i 339	. . . . . . . . 9 |- ( ( rh -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) )
16		19.36v 1904	. . . . . . . . 9 |- ( E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) )
17	15, 16	bitr4i 267	. . . . . . . 8 |- ( ( rh -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) )
18	17	imbi2i 326	. . . . . . 7 |- ( ( i e. n -> ( rh -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) )
19	7, 8, 18	3bitr4i 292	. . . . . 6 |- ( E. j ( i e. n -> ( si -> et ) ) <-> ( i e. n -> ( rh -> et ) ) )
20	3, 19	bitr2i 265	. . . . 5 |- ( ( i e. n -> ( rh -> et ) ) <-> E. j ( ( i e. n /\ si ) -> et ) )
21		impexp 462	. . . . . 6 |- ( ( ( ( i e. n /\ si ) /\ ( f e. K /\ i e. dom f ) ) -> ( f ` i ) C_ B ) <-> ( ( i e. n /\ si ) -> ( ( f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) )
22		bnj256 30772	. . . . . . 7 |- ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) <-> ( ( i e. n /\ si ) /\ ( f e. K /\ i e. dom f ) ) )
23	22	imbi1i 339	. . . . . 6 |- ( ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) <-> ( ( ( i e. n /\ si ) /\ ( f e. K /\ i e. dom f ) ) -> ( f ` i ) C_ B ) )
24		bnj1090.9	. . . . . . 7 |- ( et <-> ( ( f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) )
25	24	imbi2i 326	. . . . . 6 |- ( ( ( i e. n /\ si ) -> et ) <-> ( ( i e. n /\ si ) -> ( ( f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) )
26	21, 23, 25	3bitr4i 292	. . . . 5 |- ( ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) <-> ( ( i e. n /\ si ) -> et ) )
27	20, 26	bnj133 30793	. . . 4 |- ( ( i e. n -> ( rh -> et ) ) <-> E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) )
28	27	albii 1747	. . 3 |- ( A. i ( i e. n -> ( rh -> et ) ) <-> A. i E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) )
29		df-ral 2917	. . 3 |- ( A. i e. n ( rh -> et ) <-> A. i ( i e. n -> ( rh -> et ) ) )
30		bnj1090.19	. . . . . 6 |- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) )
31	30	imbi1i 339	. . . . 5 |- ( ( ph0 -> ( f ` i ) C_ B ) <-> ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) )
32	31	exbii 1774	. . . 4 |- ( E. j ( ph0 -> ( f ` i ) C_ B ) <-> E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) )
33	32	albii 1747	. . 3 |- ( 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 ) )
34	28, 29, 33	3bitr4i 292	. 2 |- ( A. i e. n ( rh -> et ) <-> A. i E. j ( ph0 -> ( f ` i ) C_ B ) )
35	1, 34	sylibr 224	1 |- ( ( th /\ ta /\ ch /\ ze ) -> A. i e. n ( rh -> et ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704   e. wcel 1990   A.wral 2912   [.wsbc 3435   C_ wss 3574   class class class wbr 4653   _E cep 5028   dom cdm 5114   ` cfv 5888   /\ w-bnj17 30752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039  df-ex 1705  df-ral 2917  df-bnj17 30753

This theorem is referenced by:  bnj1030  31055