Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1118.2 |
|
2 |
|
bnj1118.3 |
|
3 |
|
bnj1118.5 |
|
4 |
|
bnj1118.7 |
|
5 |
|
bnj1118.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 |- |
6 |
|
bnj1118.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 |- |
7 |
|
bnj1118.26 |
Could not format ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) : No typesetting found for |- ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) with typecode |- |
8 |
2 4 5 6 7
|
bnj1110 |
Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) with typecode |- |
9 |
|
ancl |
Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) ) ) with typecode |- |
10 |
8 9
|
bnj101 |
Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) ) with typecode |- |
11 |
|
simpr2 |
Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> i = suc j ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> i = suc j ) with typecode |- |
12 |
2
|
bnj1254 |
|
13 |
12
|
3ad2ant3 |
|
14 |
13
|
ad2antrl |
Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ps ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ps ) with typecode |- |
15 |
14
|
adantr |
Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ps ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ps ) with typecode |- |
16 |
2
|
bnj1232 |
|
17 |
16
|
3ad2ant3 |
|
18 |
17
|
ad2antrl |
Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> n e. D ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> n e. D ) with typecode |- |
19 |
18
|
adantr |
Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> n e. D ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> n e. D ) with typecode |- |
20 |
|
simpr1 |
Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> j e. n ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> j e. n ) with typecode |- |
21 |
4
|
bnj923 |
|
22 |
21
|
anim1i |
|
23 |
22
|
ancomd |
|
24 |
19 20 23
|
syl2anc |
Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( j e. n /\ n e. _om ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( j e. n /\ n e. _om ) ) with typecode |- |
25 |
|
elnn |
|
26 |
24 25
|
syl |
Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> j e. _om ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> j e. _om ) with typecode |- |
27 |
6
|
bnj1232 |
Could not format ( ph0 -> i e. n ) : No typesetting found for |- ( ph0 -> i e. n ) with typecode |- |
28 |
27
|
adantl |
Could not format ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> i e. n ) : No typesetting found for |- ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> i e. n ) with typecode |- |
29 |
28
|
ad2antlr |
Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> i e. n ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> i e. n ) with typecode |- |
30 |
11 15 26 29
|
bnj951 |
Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( i = suc j /\ ps /\ j e. _om /\ i e. n ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( i = suc j /\ ps /\ j e. _om /\ i e. n ) ) with typecode |- |
31 |
3
|
simp2bi |
|
32 |
31
|
3ad2ant2 |
|
33 |
32
|
ad2antrl |
Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> _TrFo ( B , A , R ) ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> _TrFo ( B , A , R ) ) with typecode |- |
34 |
|
simp3 |
|
35 |
33 34
|
anim12i |
Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( _TrFo ( B , A , R ) /\ ( f ` j ) C_ B ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( _TrFo ( B , A , R ) /\ ( f ` j ) C_ B ) ) with typecode |- |
36 |
|
bnj256 |
|
37 |
1
|
bnj1112 |
|
38 |
37
|
biimpi |
|
39 |
38
|
19.21bi |
|
40 |
|
eleq1 |
|
41 |
40
|
anbi2d |
|
42 |
|
fveqeq2 |
|
43 |
41 42
|
imbi12d |
|
44 |
39 43
|
syl5ibr |
|
45 |
44
|
imp31 |
|
46 |
36 45
|
sylbi |
|
47 |
|
df-bnj19 |
|
48 |
|
ssralv |
|
49 |
47 48
|
syl5bi |
|
50 |
49
|
impcom |
|
51 |
|
iunss |
|
52 |
50 51
|
sylibr |
|
53 |
|
sseq1 |
|
54 |
53
|
biimpar |
|
55 |
46 52 54
|
syl2an |
|
56 |
30 35 55
|
syl2anc |
Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( f ` i ) C_ B ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( f ` i ) C_ B ) with typecode |- |
57 |
10 56
|
bnj1023 |
Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) with typecode |- |