Step | Hyp | Ref
| Expression |
1 | | df-sfin 4446 |
. . 3
Sfin ![(](lp.gif) ![M](_cm.gif) ![N](_cn.gif) ![(](lp.gif) Nn Nn ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1
![~P](scrp.gif) ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | 3simpa 952 |
. . 3
![(](lp.gif) ![(](lp.gif) Nn Nn ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1
![~P](scrp.gif) ![N](_cn.gif) ![)](rp.gif)
![(](lp.gif)
Nn Nn ![)](rp.gif) ![)](rp.gif) |
3 | 1, 2 | sylbi 187 |
. 2
Sfin ![(](lp.gif) ![M](_cm.gif) ![N](_cn.gif) ![(](lp.gif) Nn Nn ![)](rp.gif) ![)](rp.gif) |
4 | | sfintfinlem1 4531 |
. . . 4
![{](lbrace.gif) ![A.](forall.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![k](_k.gif) ![n](_n.gif) Sfin Tfin ![k](_k.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
5 | | sfineq1 4526 |
. . . . . 6
![(](lp.gif) 0c Sfin ![(](lp.gif) ![k](_k.gif)
![n](_n.gif) Sfin 0c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | tfineq 4488 |
. . . . . . . 8
![(](lp.gif) 0c Tfin Tfin
0c![)](rp.gif) |
7 | | tfin0c 4497 |
. . . . . . . 8
Tfin 0c 0c |
8 | 6, 7 | syl6eq 2401 |
. . . . . . 7
![(](lp.gif) 0c Tfin 0c![)](rp.gif) |
9 | | sfineq1 4526 |
. . . . . . 7
Tfin
0c Sfin Tfin ![k](_k.gif) Tfin
![n](_n.gif) Sfin 0c Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 8, 9 | syl 15 |
. . . . . 6
![(](lp.gif) 0c Sfin Tfin ![k](_k.gif)
Tfin ![n](_n.gif) Sfin 0c Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 5, 10 | imbi12d 311 |
. . . . 5
![(](lp.gif) 0c ![(](lp.gif) Sfin ![(](lp.gif) ![k](_k.gif) ![n](_n.gif) Sfin Tfin ![k](_k.gif)
Tfin ![n](_n.gif) ![)](rp.gif) Sfin 0c ![n](_n.gif) Sfin 0c Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 11 | albidv 1625 |
. . . 4
![(](lp.gif) 0c ![(](lp.gif) ![A.](forall.gif) ![n](_n.gif) Sfin
![(](lp.gif) ![k](_k.gif) ![n](_n.gif) Sfin Tfin ![k](_k.gif) Tfin
![n](_n.gif) ![)](rp.gif) ![A.](forall.gif) ![n](_n.gif) Sfin 0c ![n](_n.gif) Sfin 0c Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | sfineq1 4526 |
. . . . . . 7
![(](lp.gif) Sfin ![(](lp.gif) ![k](_k.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | tfineq 4488 |
. . . . . . . 8
![(](lp.gif) Tfin
Tfin ![m](_m.gif) ![)](rp.gif) |
15 | | sfineq1 4526 |
. . . . . . . 8
Tfin
Tfin Sfin Tfin ![k](_k.gif)
Tfin ![n](_n.gif) Sfin Tfin ![m](_m.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 14, 15 | syl 15 |
. . . . . . 7
![(](lp.gif) Sfin Tfin ![k](_k.gif) Tfin
![n](_n.gif) Sfin Tfin ![m](_m.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 13, 16 | imbi12d 311 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Sfin ![(](lp.gif) ![k](_k.gif) ![n](_n.gif) Sfin
Tfin ![k](_k.gif)
Tfin ![n](_n.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![n](_n.gif) Sfin Tfin ![m](_m.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 17 | albidv 1625 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![k](_k.gif) ![n](_n.gif) Sfin Tfin ![k](_k.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![A.](forall.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![n](_n.gif) Sfin
Tfin ![m](_m.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | sfineq2 4527 |
. . . . . . 7
![(](lp.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | | tfineq 4488 |
. . . . . . . 8
![(](lp.gif) Tfin
Tfin ![p](_p.gif) ![)](rp.gif) |
21 | | sfineq2 4527 |
. . . . . . . 8
Tfin
Tfin Sfin Tfin ![m](_m.gif)
Tfin ![n](_n.gif) Sfin Tfin ![m](_m.gif)
Tfin ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 20, 21 | syl 15 |
. . . . . . 7
![(](lp.gif) Sfin Tfin ![m](_m.gif) Tfin ![n](_n.gif)
Sfin Tfin
![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 19, 22 | imbi12d 311 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![n](_n.gif) Sfin
Tfin ![m](_m.gif)
Tfin ![n](_n.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif)
Tfin ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 23 | cbvalv 2002 |
. . . . 5
![(](lp.gif) ![A.](forall.gif) ![n](_n.gif)
Sfin ![(](lp.gif) ![m](_m.gif) ![n](_n.gif) Sfin Tfin ![m](_m.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![A.](forall.gif) ![p](_p.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin
Tfin ![m](_m.gif)
Tfin ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 18, 24 | syl6bb 252 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![k](_k.gif) ![n](_n.gif) Sfin Tfin ![k](_k.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![A.](forall.gif) ![p](_p.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin
Tfin ![m](_m.gif)
Tfin ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | | sfineq1 4526 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1c Sfin ![(](lp.gif) ![k](_k.gif)
![n](_n.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | | tfineq 4488 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1c Tfin Tfin
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
28 | | sfineq1 4526 |
. . . . . . 7
Tfin
Tfin ![(](lp.gif)
1c
Sfin Tfin ![k](_k.gif) Tfin
![n](_n.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 27, 28 | syl 15 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1c Sfin Tfin ![k](_k.gif)
Tfin ![n](_n.gif) Sfin Tfin ![(](lp.gif)
1c![)](rp.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 26, 29 | imbi12d 311 |
. . . . 5
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) Sfin ![(](lp.gif) ![k](_k.gif) ![n](_n.gif) Sfin Tfin ![k](_k.gif)
Tfin ![n](_n.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) Sfin Tfin ![(](lp.gif)
1c![)](rp.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 30 | albidv 1625 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![A.](forall.gif) ![n](_n.gif) Sfin
![(](lp.gif) ![k](_k.gif) ![n](_n.gif) Sfin Tfin ![k](_k.gif) Tfin
![n](_n.gif) ![)](rp.gif) ![A.](forall.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) Sfin Tfin ![(](lp.gif)
1c![)](rp.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | | sfineq1 4526 |
. . . . . 6
![(](lp.gif) Sfin ![(](lp.gif) ![k](_k.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![M](_cm.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | | tfineq 4488 |
. . . . . . 7
![(](lp.gif) Tfin
Tfin ![M](_cm.gif) ![)](rp.gif) |
34 | | sfineq1 4526 |
. . . . . . 7
Tfin
Tfin Sfin Tfin ![k](_k.gif)
Tfin ![n](_n.gif) Sfin Tfin ![M](_cm.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 33, 34 | syl 15 |
. . . . . 6
![(](lp.gif) Sfin Tfin ![k](_k.gif) Tfin
![n](_n.gif) Sfin Tfin ![M](_cm.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 32, 35 | imbi12d 311 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Sfin ![(](lp.gif) ![k](_k.gif) ![n](_n.gif) Sfin
Tfin ![k](_k.gif)
Tfin ![n](_n.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![M](_cm.gif) ![n](_n.gif) Sfin Tfin ![M](_cm.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 36 | albidv 1625 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![k](_k.gif) ![n](_n.gif) Sfin Tfin ![k](_k.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![A.](forall.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![M](_cm.gif) ![n](_n.gif) Sfin
Tfin ![M](_cm.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | | sfin01 4528 |
. . . . . . 7
Sfin 0c 1c![)](rp.gif) |
39 | | sfin112 4529 |
. . . . . . 7
![(](lp.gif) Sfin
0c ![n](_n.gif) Sfin 0c 1c![)](rp.gif)
1c![)](rp.gif) |
40 | 38, 39 | mpan2 652 |
. . . . . 6
Sfin 0c ![n](_n.gif) 1c![)](rp.gif) |
41 | | tfineq 4488 |
. . . . . . . . 9
![(](lp.gif) 1c Tfin Tfin
1c![)](rp.gif) |
42 | | tfin1c 4499 |
. . . . . . . . 9
Tfin 1c 1c |
43 | 41, 42 | syl6eq 2401 |
. . . . . . . 8
![(](lp.gif) 1c Tfin 1c![)](rp.gif) |
44 | | sfineq2 4527 |
. . . . . . . 8
Tfin
1c Sfin 0c Tfin ![n](_n.gif) Sfin 0c 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 43, 44 | syl 15 |
. . . . . . 7
![(](lp.gif) 1c Sfin 0c Tfin ![n](_n.gif)
Sfin 0c 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
46 | 38, 45 | mpbiri 224 |
. . . . . 6
![(](lp.gif) 1c Sfin 0c Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 40, 46 | syl 15 |
. . . . 5
Sfin 0c ![n](_n.gif) Sfin 0c Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 47 | ax-gen 1546 |
. . . 4
![A.](forall.gif) ![n](_n.gif) Sfin 0c ![n](_n.gif) Sfin 0c Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
49 | | df-sfin 4446 |
. . . . . . . . . 10
Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) 1c Nn
Nn ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1
![(](lp.gif) 1c ![~P](scrp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 49 | simp3bi 972 |
. . . . . . . . 9
Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1
![(](lp.gif) 1c ![~P](scrp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 50 | 3ad2ant3 978 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1
![(](lp.gif) 1c ![~P](scrp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
52 | | sfindbl 4530 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn 1
![(](lp.gif) 1c![)](rp.gif) ![E.](exists.gif)
Nn Sfin ![(](lp.gif) ![m](_m.gif)
![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | 52 | 3ad2antl1 1117 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) 1 ![(](lp.gif)
1c![)](rp.gif) ![E.](exists.gif)
Nn Sfin ![(](lp.gif) ![m](_m.gif)
![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
54 | | sfineq2 4527 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
55 | | tfineq 4488 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) Tfin
Tfin ![q](_q.gif) ![)](rp.gif) |
56 | | sfineq2 4527 |
. . . . . . . . . . . . . . . . . . . . . . 23
Tfin
Tfin Sfin Tfin ![m](_m.gif)
Tfin ![p](_p.gif) Sfin Tfin ![m](_m.gif)
Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
57 | 55, 56 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif)
Sfin Tfin
![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 54, 57 | imbi12d 311 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin
Tfin ![m](_m.gif)
Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin Tfin ![m](_m.gif)
Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
59 | 58 | spv 1998 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![A.](forall.gif) ![p](_p.gif)
Sfin ![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif)
Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin Tfin ![m](_m.gif)
Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
60 | | simprrl 740 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) Sfin
![(](lp.gif) ![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
61 | 60 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
62 | | simplrl 736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
63 | | simprrr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) Sfin
![(](lp.gif) ![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
64 | 63 | ad2antlr 707 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
65 | | sfin112 4529 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) Sfin
![(](lp.gif) ![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
66 | 62, 64, 65 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
67 | | df-sfin 4446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) ![q](_q.gif)
Nn ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1
![(](lp.gif) 1c ![~P](scrp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
68 | 67 | simp3bi 972 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1 ![(](lp.gif)
1c
![~P](scrp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
69 | 64, 68 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1
![(](lp.gif) 1c ![~P](scrp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
70 | | simp2 956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
1 ![(](lp.gif)
1c![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
71 | | df-sfin 4446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
Tfin
Nn Tfin Nn ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1
Tfin ![~P](scrp.gif) Tfin
![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
72 | 71 | simp1bi 970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
Tfin
Nn ![)](rp.gif) |
73 | 70, 72 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
1 ![(](lp.gif)
1c![)](rp.gif) Tfin
Nn ![)](rp.gif) |
74 | | simp1l 979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
1 ![(](lp.gif)
1c![)](rp.gif) Nn ![)](rp.gif) |
75 | | peano2 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) |
76 | 74, 75 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
1 ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c Nn ![)](rp.gif) |
77 | | simp3 957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
1 ![(](lp.gif)
1c![)](rp.gif) 1 ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
78 | | tfinpw1 4494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn 1
![(](lp.gif) 1c![)](rp.gif) 1 1 Tfin ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
79 | 76, 77, 78 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
1 ![(](lp.gif)
1c![)](rp.gif) 1 1 Tfin ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
80 | | ne0i 3556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) 1
![(](lp.gif) 1c ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
81 | 80 | 3ad2ant3 978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
1 ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
82 | | tfinsuc 4498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) Tfin ![(](lp.gif)
1c
Tfin 1c![)](rp.gif) ![)](rp.gif) |
83 | 74, 81, 82 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
1 ![(](lp.gif)
1c![)](rp.gif) Tfin ![(](lp.gif)
1c
Tfin 1c![)](rp.gif) ![)](rp.gif) |
84 | 79, 83 | eleqtrd 2429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
1 ![(](lp.gif)
1c![)](rp.gif) 1 1 Tfin 1c![)](rp.gif) ![)](rp.gif) |
85 | | sfindbl 4530 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) Tfin
Nn 1 1 Tfin 1c![)](rp.gif) ![E.](exists.gif)
Nn Sfin Tfin ![m](_m.gif)
![k](_k.gif) Sfin ![(](lp.gif) Tfin
1c![)](rp.gif) ![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
86 | 73, 84, 85 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
1 ![(](lp.gif)
1c![)](rp.gif) ![E.](exists.gif)
Nn Sfin Tfin ![m](_m.gif)
![k](_k.gif) Sfin ![(](lp.gif) Tfin
1c![)](rp.gif) ![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
87 | | simp2 956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
Sfin Tfin ![m](_m.gif) ![k](_k.gif)
Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
88 | | simp3l 983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
Sfin Tfin ![m](_m.gif) ![k](_k.gif)
Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) |
89 | | sfin112 4529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) Sfin
Tfin ![m](_m.gif)
Tfin ![q](_q.gif) Sfin Tfin ![m](_m.gif) ![k](_k.gif) ![)](rp.gif) Tfin
![k](_k.gif) ![)](rp.gif) |
90 | 87, 88, 89 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
Sfin Tfin ![m](_m.gif) ![k](_k.gif)
Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Tfin
![k](_k.gif) ![)](rp.gif) |
91 | | addceq12 4385 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
![(](lp.gif) Tfin
Tfin ![k](_k.gif) Tfin Tfin ![q](_q.gif)
![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) |
92 | 91 | anidms 626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
Tfin
Tfin Tfin ![q](_q.gif)
![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) |
93 | | sfineq2 4527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
![(](lp.gif) Tfin
Tfin ![q](_q.gif)
![(](lp.gif) ![k](_k.gif) Sfin ![(](lp.gif) Tfin
1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) Sfin ![(](lp.gif) Tfin 1c![)](rp.gif) ![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
94 | 92, 93 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
Tfin
Sfin ![(](lp.gif) Tfin
1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) Sfin ![(](lp.gif) Tfin 1c![)](rp.gif) ![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
95 | 94 | biimprcd 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
![(](lp.gif) ![k](_k.gif) ![)](rp.gif) Tfin Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
96 | 95 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) Sfin
Tfin ![m](_m.gif)
![k](_k.gif) Sfin ![(](lp.gif) Tfin
1c![)](rp.gif) ![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) Tfin
Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
97 | 96 | 3ad2ant3 978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
Sfin Tfin ![m](_m.gif) ![k](_k.gif)
Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Tfin
Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
98 | 90, 97 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
Sfin Tfin ![m](_m.gif) ![k](_k.gif)
Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
99 | 98 | 3expia 1153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) ![(](lp.gif) Sfin Tfin ![m](_m.gif)
![k](_k.gif) Sfin ![(](lp.gif) Tfin
1c![)](rp.gif) ![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
100 | 99 | rexlimdvw 2741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn Sfin Tfin ![m](_m.gif)
![k](_k.gif) Sfin ![(](lp.gif) Tfin
1c![)](rp.gif) ![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
101 | 100 | 3adant3 975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
1 ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn Sfin Tfin ![m](_m.gif)
![k](_k.gif) Sfin ![(](lp.gif) Tfin
1c![)](rp.gif) ![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
102 | 86, 101 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif)
1 ![(](lp.gif)
1c![)](rp.gif) Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
103 | 102 | 3expia 1153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) ![(](lp.gif) 1 ![(](lp.gif) 1c Sfin ![(](lp.gif) Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
104 | 103 | adantrd 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) 1
![(](lp.gif) 1c ![~P](scrp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif)
Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
105 | 104 | exlimdv 1636 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1 ![(](lp.gif)
1c
![~P](scrp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif)
Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
106 | 69, 105 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
107 | | simpll 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) Nn ![)](rp.gif) |
108 | 80 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![(](lp.gif) 1
![(](lp.gif) 1c ![~P](scrp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif)
![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
109 | 108 | exlimiv 1634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1
![(](lp.gif) 1c ![~P](scrp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif)
![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
110 | 64, 68, 109 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
111 | 107, 110,
82 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) Tfin ![(](lp.gif)
1c
Tfin 1c![)](rp.gif) ![)](rp.gif) |
112 | | simprrl 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif)
Nn ![)](rp.gif) |
113 | 112 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) Nn ![)](rp.gif) |
114 | | ne0i 3556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![~P](scrp.gif) ![(](lp.gif) ![q](_q.gif) ![(](lp.gif) ![q](_q.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
115 | 114 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![(](lp.gif) 1
![(](lp.gif) 1c ![~P](scrp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif)
![(](lp.gif) ![q](_q.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
116 | 115 | exlimiv 1634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1
![(](lp.gif) 1c ![~P](scrp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif)
![(](lp.gif) ![q](_q.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
117 | 64, 68, 116 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
118 | | tfindi 4496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![q](_q.gif)
![(/)](varnothing.gif) Tfin ![(](lp.gif) ![q](_q.gif) Tfin
Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
119 | 113, 113,
117, 118 | syl3anc 1182 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) Tfin ![(](lp.gif)
![q](_q.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
120 | | sfineq1 4526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Tfin ![(](lp.gif)
1c
Tfin 1c Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) Sfin ![(](lp.gif) Tfin 1c![)](rp.gif) Tfin ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
121 | | sfineq2 4527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Tfin ![(](lp.gif)
![q](_q.gif)
Tfin Tfin ![q](_q.gif) Sfin ![(](lp.gif)
Tfin 1c![)](rp.gif)
Tfin ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) Sfin ![(](lp.gif) Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
122 | 120, 121 | sylan9bb 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) Tfin
![(](lp.gif) 1c
Tfin 1c Tfin ![(](lp.gif)
![q](_q.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif)
Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) Sfin ![(](lp.gif) Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
123 | 111, 119,
122 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) Sfin ![(](lp.gif) Tfin 1c![)](rp.gif)
Tfin Tfin ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
124 | 106, 123 | mpbird 223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
125 | | tfineq 4488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
Tfin
Tfin ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
126 | | sfineq2 4527 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Tfin
Tfin ![(](lp.gif) ![q](_q.gif) Sfin Tfin ![(](lp.gif)
1c![)](rp.gif) Tfin ![n](_n.gif)
Sfin Tfin
![(](lp.gif) 1c![)](rp.gif)
Tfin ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
127 | 125, 126 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) Sfin Tfin ![(](lp.gif)
1c![)](rp.gif) Tfin ![(](lp.gif)
![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
128 | 127 | biimprcd 216 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
129 | 124, 128 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![q](_q.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
130 | 66, 129 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif) Tfin ![q](_q.gif) ![)](rp.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
131 | 130 | ex 423 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![m](_m.gif)
Tfin ![q](_q.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
132 | 61, 131 | embantd 50 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin Tfin ![m](_m.gif)
Tfin ![q](_q.gif) ![)](rp.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
133 | 59, 132 | syl5 28 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![p](_p.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif)
Tfin ![p](_p.gif) ![)](rp.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
134 | 133 | exp32 588 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![p](_p.gif)
Sfin ![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif)
Tfin ![p](_p.gif) ![)](rp.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
135 | 134 | com34 77 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) Nn Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
136 | 135 | com23 72 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) Nn ![(](lp.gif) ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
137 | 136 | 3imp 1145 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) Nn Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
138 | 137 | exp3a 425 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![(](lp.gif) Nn ![(](lp.gif) Sfin ![(](lp.gif) ![m](_m.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![(](lp.gif)
1c![)](rp.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
139 | 138 | rexlimdv 2737 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn Sfin ![(](lp.gif) ![m](_m.gif)
![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![(](lp.gif)
1c![)](rp.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
140 | 139 | adantr 451 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) 1 ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn Sfin ![(](lp.gif) ![m](_m.gif)
![q](_q.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) Sfin Tfin ![(](lp.gif)
1c![)](rp.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
141 | 53, 140 | mpd 14 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) 1 ![(](lp.gif)
1c![)](rp.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
142 | 141 | ex 423 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![(](lp.gif) 1
![(](lp.gif) 1c Sfin Tfin ![(](lp.gif)
1c![)](rp.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
143 | 142 | adantrd 454 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) 1
![(](lp.gif) 1c ![~P](scrp.gif) ![n](_n.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
144 | 143 | exlimdv 1636 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1
![(](lp.gif) 1c ![~P](scrp.gif) ![n](_n.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
145 | 51, 144 | mpd 14 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) Sfin Tfin ![(](lp.gif) 1c![)](rp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
146 | 145 | 3expia 1153 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) Sfin Tfin ![(](lp.gif)
1c![)](rp.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
147 | 146 | alrimiv 1631 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![A.](forall.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) Sfin Tfin ![(](lp.gif)
1c![)](rp.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
148 | 147 | ex 423 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![A.](forall.gif) ![p](_p.gif) Sfin
![(](lp.gif) ![m](_m.gif) ![p](_p.gif) Sfin Tfin ![m](_m.gif) Tfin ![p](_p.gif) ![)](rp.gif) ![A.](forall.gif) ![n](_n.gif)
Sfin ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) Sfin Tfin ![(](lp.gif)
1c![)](rp.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
149 | 4, 12, 25, 31, 37, 48, 148 | finds 4411 |
. . 3
![(](lp.gif) Nn ![A.](forall.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![M](_cm.gif) ![n](_n.gif) Sfin Tfin ![M](_cm.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
150 | | sfineq2 4527 |
. . . . 5
![(](lp.gif) Sfin ![(](lp.gif) ![M](_cm.gif) ![n](_n.gif) Sfin ![(](lp.gif) ![M](_cm.gif) ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
151 | | tfineq 4488 |
. . . . . 6
![(](lp.gif) Tfin
Tfin ![N](_cn.gif) ![)](rp.gif) |
152 | | sfineq2 4527 |
. . . . . 6
Tfin
Tfin Sfin Tfin ![M](_cm.gif)
Tfin ![n](_n.gif) Sfin Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
153 | 151, 152 | syl 15 |
. . . . 5
![(](lp.gif) Sfin Tfin ![M](_cm.gif) Tfin ![n](_n.gif)
Sfin Tfin
![M](_cm.gif) Tfin ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
154 | 150, 153 | imbi12d 311 |
. . . 4
![(](lp.gif) ![(](lp.gif) Sfin ![(](lp.gif) ![M](_cm.gif) ![n](_n.gif) Sfin
Tfin ![M](_cm.gif)
Tfin ![n](_n.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![M](_cm.gif) ![N](_cn.gif) Sfin Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
155 | 154 | spcgv 2939 |
. . 3
![(](lp.gif) Nn ![(](lp.gif) ![A.](forall.gif) ![n](_n.gif) Sfin
![(](lp.gif) ![M](_cm.gif) ![n](_n.gif) Sfin Tfin ![M](_cm.gif) Tfin ![n](_n.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![M](_cm.gif) ![N](_cn.gif) Sfin Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
156 | 149, 155 | mpan9 455 |
. 2
![(](lp.gif) ![(](lp.gif) Nn Nn Sfin ![(](lp.gif) ![M](_cm.gif) ![N](_cn.gif) Sfin Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
157 | 3, 156 | mpcom 32 |
1
Sfin ![(](lp.gif) ![M](_cm.gif) ![N](_cn.gif) Sfin Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |