Step | Hyp | Ref
| Expression |
1 | | simpll 519 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![F F](_cf.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) |
2 | | simplr 520 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![F F](_cf.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![) )](rp.gif) |
3 | | simprr 522 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![F F](_cf.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif)
![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) |
4 | 1, 2, 3 | 3jca 1162 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![F F](_cf.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | 4 | reximi 2532 |
. 2
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![F F](_cf.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
6 | | fveq2 5429 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![) )](rp.gif) ![)
)](rp.gif) |
7 | 6 | sseq2d 3132 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | 6 | raleqdv 2635 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) DECID ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
9 | | seqeq1 10252 |
. . . . . 6
![( (](lp.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif) ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![) )](rp.gif) ![) )](rp.gif) |
10 | 9 | breq1d 3947 |
. . . . 5
![( (](lp.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif)
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
11 | 7, 8, 10 | 3anbi123d 1291 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif) ![x x](_x.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | 11 | cbvrexvw 2662 |
. . 3
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) DECID
![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif) ![x x](_x.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | | reeanv 2603 |
. . . . 5
![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
14 | | simprl3 1029 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) |
15 | | simprl1 1027 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) ![)
)](rp.gif) ![) )](rp.gif) |
16 | | uzssz 9369 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) ![ZZ ZZ](bbz.gif) |
17 | 15, 16 | sstrdi 3114 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
18 | | 1zzd 9105 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
19 | | simplrr 526 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif)
![NN NN](bbn.gif) ![) )](rp.gif) |
20 | 19 | nnzd 9196 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
21 | 18, 20 | fzfigd 10235 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![Fin Fin](_fin.gif) ![) )](rp.gif) |
22 | | simprr 522 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![f
f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) |
23 | | f1oeng 6659 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![A A](_ca.gif) ![) )](rp.gif) |
24 | 21, 22, 23 | syl2anc 409 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif)
![A A](_ca.gif) ![) )](rp.gif) |
25 | 24 | ensymd 6685 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | | enfii 6776 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif)
![Fin Fin](_fin.gif) ![) )](rp.gif) |
27 | 21, 25, 26 | syl2anc 409 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif)
![Fin Fin](_fin.gif) ![) )](rp.gif) |
28 | | zfz1iso 10616 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![Fin Fin](_fin.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | 17, 27, 28 | syl2anc 409 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
30 | | prodmo.1 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | | prodmo.2 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
32 | 31 | ad4ant14 506 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif)
![A A](_ca.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
33 | | prodmodc.3 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![j j](_j.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
34 | | eqid 2140 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif)
♯![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![g
g](_g.gif) ![`
`](backtick.gif) ![j j](_j.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ♯![`
`](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![j j](_j.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | | simpll2 1022 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID ![A A](_ca.gif) ![) )](rp.gif) |
36 | 35 | adantl 275 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID ![A A](_ca.gif) ![) )](rp.gif) |
37 | | eleq1w 2201 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 37 | dcbid 824 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) DECID
DECID
![A A](_ca.gif) ![) )](rp.gif) ![)
)](rp.gif) |
39 | 38 | rspcv 2789 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID DECID ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
40 | 36, 39 | mpan9 279 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) ![) )](rp.gif) DECID ![A A](_ca.gif) ![) )](rp.gif) |
41 | | simplrr 526 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif)
![NN NN](bbn.gif) ![) )](rp.gif) |
42 | | simplrl 525 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
43 | 15 | adantrr 471 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) ![)
)](rp.gif) ![) )](rp.gif) |
44 | | simprlr 528 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![f
f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) |
45 | | simprr 522 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
46 | 30, 32, 33, 34, 40, 41, 42, 43, 44, 45 | prodmodclem2a 11377 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) |
47 | 46 | expr 373 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![A A](_ca.gif)
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![)
)](rp.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
48 | 47 | exlimdv 1792 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
49 | 29, 48 | mpd 13 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) |
50 | | climuni 11094 |
. . . . . . . . . . . 12
![( (](lp.gif) ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![)
)](rp.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![)
)](rp.gif) |
51 | 14, 49, 50 | syl2anc 409 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) |
52 | | eqeq2 2150 |
. . . . . . . . . . 11
![( (](lp.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![)
)](rp.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | 51, 52 | syl5ibrcom 156 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) |
54 | 53 | expr 373 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif)
![z z](_z.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
55 | 54 | impd 252 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) |
56 | 55 | exlimdv 1792 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif)
![z z](_z.gif) ![) )](rp.gif) ![)
)](rp.gif) |
57 | 56 | expimpd 361 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![NN NN](bbn.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) |
58 | 57 | rexlimdvva 2560 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) DECID
![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) |
59 | 13, 58 | syl5bir 152 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) |
60 | 59 | expdimp 257 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![w w](_w.gif) DECID ![seq seq](_seq.gif) ![w w](_w.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) |
61 | 12, 60 | sylan2b 285 |
. 2
![( (](lp.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) DECID ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![)
)](rp.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) |
62 | 5, 61 | sylan2 284 |
1
![( (](lp.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![F F](_cf.gif) ![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif)
![z z](_z.gif) ![) )](rp.gif) ![)
)](rp.gif) |