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 ) )