Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1128.1 |
|
2 |
|
bnj1128.2 |
|
3 |
|
bnj1128.3 |
|
4 |
|
bnj1128.4 |
|
5 |
|
bnj1128.5 |
|
6 |
|
bnj1128.6 |
|
7 |
|
bnj1128.7 |
|
8 |
|
bnj1128.8 |
Could not format ( ph' <-> [. j / i ]. ph ) : No typesetting found for |- ( ph' <-> [. j / i ]. ph ) with typecode |- |
9 |
|
bnj1128.9 |
Could not format ( ps' <-> [. j / i ]. ps ) : No typesetting found for |- ( ps' <-> [. j / i ]. ps ) with typecode |- |
10 |
|
bnj1128.10 |
Could not format ( ch' <-> [. j / i ]. ch ) : No typesetting found for |- ( ch' <-> [. j / i ]. ch ) with typecode |- |
11 |
|
bnj1128.11 |
Could not format ( th' <-> [. j / i ]. th ) : No typesetting found for |- ( th' <-> [. j / i ]. th ) with typecode |- |
12 |
1 2 3 4 5
|
bnj981 |
|
13 |
|
simp1 |
|
14 |
|
simp2 |
|
15 |
|
nfv |
|
16 |
|
nfra1 |
|
17 |
7 16
|
nfxfr |
|
18 |
|
nfv |
|
19 |
15 17 18
|
nf3an |
|
20 |
|
nfv |
|
21 |
19 20
|
nfim |
|
22 |
21
|
nf5ri |
|
23 |
3
|
bnj1098 |
|
24 |
|
simpl |
|
25 |
|
simpr1 |
|
26 |
5
|
bnj1232 |
|
27 |
26
|
3ad2ant3 |
|
28 |
27
|
adantl |
|
29 |
24 25 28
|
3jca |
|
30 |
23 29
|
bnj1101 |
|
31 |
|
ancl |
|
32 |
30 31
|
bnj101 |
|
33 |
|
df-3an |
|
34 |
33
|
imbi2i |
|
35 |
34
|
exbii |
|
36 |
32 35
|
mpbir |
|
37 |
|
bnj213 |
|
38 |
37
|
bnj226 |
|
39 |
|
simp21 |
|
40 |
|
simp3r |
|
41 |
|
biid |
|
42 |
|
biid |
|
43 |
|
vex |
|
44 |
|
sbcg |
|
45 |
43 44
|
ax-mp |
|
46 |
8 45
|
bitr2i |
Could not format ( ph <-> ph' ) : No typesetting found for |- ( ph <-> ph' ) with typecode |- |
47 |
2 9
|
bnj1039 |
Could not format ( ps' <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |- |
48 |
2 47
|
bitr4i |
Could not format ( ps <-> ps' ) : No typesetting found for |- ( ps <-> ps' ) with typecode |- |
49 |
41 42 46 48
|
bnj887 |
Could not format ( ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) : No typesetting found for |- ( ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) with typecode |- |
50 |
8 9 5 10
|
bnj1040 |
Could not format ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) : No typesetting found for |- ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) with typecode |- |
51 |
49 5 50
|
3bitr4i |
Could not format ( ch <-> ch' ) : No typesetting found for |- ( ch <-> ch' ) with typecode |- |
52 |
50
|
bnj1254 |
Could not format ( ch' -> ps' ) : No typesetting found for |- ( ch' -> ps' ) with typecode |- |
53 |
51 52
|
sylbi |
Could not format ( ch -> ps' ) : No typesetting found for |- ( ch -> ps' ) with typecode |- |
54 |
53
|
3ad2ant3 |
Could not format ( ( i e. n /\ ta /\ ch ) -> ps' ) : No typesetting found for |- ( ( i e. n /\ ta /\ ch ) -> ps' ) with typecode |- |
55 |
54
|
3ad2ant2 |
Could not format ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> ps' ) : No typesetting found for |- ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> ps' ) with typecode |- |
56 |
|
simp3l |
|
57 |
27
|
3ad2ant2 |
|
58 |
3
|
bnj923 |
|
59 |
|
elnn |
|
60 |
58 59
|
sylan2 |
|
61 |
56 57 60
|
syl2anc |
|
62 |
47
|
bnj589 |
Could not format ( ps' <-> A. j e. _om ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. j e. _om ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) with typecode |- |
63 |
|
rsp |
|
64 |
62 63
|
sylbi |
Could not format ( ps' -> ( j e. _om -> ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) ) : No typesetting found for |- ( ps' -> ( j e. _om -> ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) ) with typecode |- |
65 |
|
eleq1 |
|
66 |
|
fveqeq2 |
|
67 |
65 66
|
imbi12d |
|
68 |
67
|
imbi2d |
|
69 |
64 68
|
syl5ibr |
Could not format ( i = suc j -> ( ps' -> ( j e. _om -> ( i e. n -> ( f ` i ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) ) ) : No typesetting found for |- ( i = suc j -> ( ps' -> ( j e. _om -> ( i e. n -> ( f ` i ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) ) ) with typecode |- |
70 |
40 55 61 69
|
syl3c |
|
71 |
39 70
|
mpd |
|
72 |
38 71
|
bnj1262 |
|
73 |
36 72
|
bnj1023 |
|
74 |
5
|
bnj1247 |
|
75 |
74
|
3ad2ant3 |
|
76 |
|
bnj213 |
|
77 |
|
fveq2 |
|
78 |
1
|
biimpi |
|
79 |
77 78
|
sylan9eq |
|
80 |
76 79
|
bnj1262 |
|
81 |
75 80
|
sylan2 |
|
82 |
73 81
|
bnj1109 |
|
83 |
22 82
|
bnj1131 |
|
84 |
83
|
3expia |
|
85 |
84 6
|
sylibr |
|
86 |
3 5 7 85
|
bnj1133 |
|
87 |
6
|
ralbii |
|
88 |
86 87
|
sylib |
|
89 |
|
rsp |
|
90 |
88 89
|
syl |
|
91 |
13 14 13 90
|
syl3c |
|
92 |
|
simp3 |
|
93 |
91 92
|
sseldd |
|
94 |
93
|
2eximi |
|
95 |
12 94
|
bnj593 |
|
96 |
|
19.9v |
|
97 |
|
19.9v |
|
98 |
|
19.9v |
|
99 |
96 97 98
|
3bitri |
|
100 |
95 99
|
sylib |
|