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