Metamath Proof Explorer

Theorem bnj1110

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 bnj1110.3 
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
bnj1110.7 
|- D = ( _om \ { (/) } )
bnj1110.18 
|- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) )
bnj1110.19 
|- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) )
bnj1110.26 
|- ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) )
Assertion bnj1110 
|- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) )

Proof

Step Hyp Ref Expression
1 bnj1110.3 
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
2 bnj1110.7 
 |-  D = ( _om \ { (/) } )
3 bnj1110.18 
 |-  ( si <-> ( ( j e. n /\ j _E i ) -> et' ) )
4 bnj1110.19 
 |-  ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) )
5 bnj1110.26 
 |-  ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) )
6 2 bnj1098 
 |-  E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. n /\ i = suc j ) )
7 bnj219 
 |-  ( i = suc j -> j _E i )
8 7 adantl 
 |-  ( ( j e. n /\ i = suc j ) -> j _E i )
9 8 ancli 
 |-  ( ( j e. n /\ i = suc j ) -> ( ( j e. n /\ i = suc j ) /\ j _E i ) )
10 df-3an 
 |-  ( ( j e. n /\ i = suc j /\ j _E i ) <-> ( ( j e. n /\ i = suc j ) /\ j _E i ) )
11 9 10 sylibr 
 |-  ( ( j e. n /\ i = suc j ) -> ( j e. n /\ i = suc j /\ j _E i ) )
12 6 11 bnj1023 
 |-  E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. n /\ i = suc j /\ j _E i ) )
13 1 bnj1232 
 |-  ( ch -> n e. D )
14 13 3ad2ant3 
 |-  ( ( th /\ ta /\ ch ) -> n e. D )
15 4 bnj1232 
 |-  ( ph0 -> i e. n )
16 14 15 anim12ci 
 |-  ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( i e. n /\ n e. D ) )
17 16 anim2i 
 |-  ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i =/= (/) /\ ( i e. n /\ n e. D ) ) )
18 3anass 
 |-  ( ( i =/= (/) /\ i e. n /\ n e. D ) <-> ( i =/= (/) /\ ( i e. n /\ n e. D ) ) )
19 17 18 sylibr 
 |-  ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i =/= (/) /\ i e. n /\ n e. D ) )
20 12 19 bnj1101 
 |-  E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ j _E i ) )
21 3simpb 
 |-  ( ( j e. n /\ i = suc j /\ j _E i ) -> ( j e. n /\ j _E i ) )
22 4 bnj1235 
 |-  ( ph0 -> si )
23 22 ad2antll 
 |-  ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> si )
24 23 3 sylib 
 |-  ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ j _E i ) -> et' ) )
25 21 24 syl5 
 |-  ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) -> et' ) )
26 25 a2i 
 |-  ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ j _E i ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> et' ) )
27 pm3.43 
 |-  ( ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ j _E i ) ) /\ ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> et' ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) )
28 26 27 mpdan 
 |-  ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ j _E i ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) )
29 20 28 bnj101 
 |-  E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) )
30 4 bnj1247 
 |-  ( ph0 -> f e. K )
31 30 ad2antll 
 |-  ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> f e. K )
32 pm3.43i 
 |-  ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> f e. K ) -> ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) )
33 31 32 ax-mp 
 |-  ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) )
34 29 33 bnj101 
 |-  E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) )
35 fndm 
 |-  ( f Fn n -> dom f = n )
36 1 35 bnj770 
 |-  ( ch -> dom f = n )
37 36 3ad2ant3 
 |-  ( ( th /\ ta /\ ch ) -> dom f = n )
38 37 ad2antrl 
 |-  ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> dom f = n )
39 38 eleq2d 
 |-  ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. dom f <-> j e. n ) )
40 pm3.43i 
 |-  ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. dom f <-> j e. n ) ) -> ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) ) )
41 39 40 ax-mp 
 |-  ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) )
42 34 41 bnj101 
 |-  E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) )
43 bnj268 
 |-  ( ( ( j e. dom f <-> j e. n ) /\ f e. K /\ ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) <-> ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) )
44 bnj251 
 |-  ( ( ( j e. dom f <-> j e. n ) /\ f e. K /\ ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) <-> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) )
45 43 44 bitr3i 
 |-  ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) <-> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) )
46 45 imbi2i 
 |-  ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) ) <-> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) )
47 46 exbii 
 |-  ( E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) ) <-> E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) )
48 42 47 mpbir 
 |-  E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) )
49 simp1 
 |-  ( ( j e. n /\ i = suc j /\ j _E i ) -> j e. n )
50 49 bnj706 
 |-  ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> j e. n )
51 simp2 
 |-  ( ( j e. n /\ i = suc j /\ j _E i ) -> i = suc j )
52 51 bnj706 
 |-  ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> i = suc j )
53 bnj258 
 |-  ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) <-> ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) /\ f e. K ) )
54 53 simprbi 
 |-  ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> f e. K )
55 bnj642 
 |-  ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> ( j e. dom f <-> j e. n ) )
56 50 55 mpbird 
 |-  ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> j e. dom f )
57 bnj645 
 |-  ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> et' )
58 57 5 sylib 
 |-  ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) )
59 54 56 58 mp2and 
 |-  ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> ( f ` j ) C_ B )
60 50 52 59 3jca 
 |-  ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) )
61 48 60 bnj1023 
 |-  E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) )