Step | Hyp | Ref
| Expression |
1 | | df-sfin 4446 |
. . . 4
Sfin ![(](lp.gif) ![Z](_cz.gif) ![X](_cx.gif) ![(](lp.gif) Nn Nn ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) 1
![~P](scrp.gif) ![X](_cx.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | sfineq1 4526 |
. . . . . . 7
![(](lp.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) Sfin ![(](lp.gif) ![Z](_cz.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | eleq1 2413 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
Spfin Spfin ![)](rp.gif) ![)](rp.gif) |
4 | 3 | imbi2d 307 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Spfin Spfin ![(](lp.gif) Spfin Spfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
5 | 2, 4 | imbi12d 311 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![(](lp.gif)
Spfin Spfin ![)](rp.gif)
Sfin ![(](lp.gif) ![Z](_cz.gif) ![x](_x.gif) ![(](lp.gif) Spfin Spfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | sfineq2 4527 |
. . . . . . 7
![(](lp.gif) Sfin ![(](lp.gif) ![Z](_cz.gif) ![x](_x.gif) Sfin ![(](lp.gif) ![Z](_cz.gif) ![X](_cx.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | eleq1 2413 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
Spfin Spfin ![)](rp.gif) ![)](rp.gif) |
8 | 7 | imbi1d 308 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Spfin Spfin ![(](lp.gif) Spfin Spfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 6, 8 | imbi12d 311 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Sfin ![(](lp.gif) ![Z](_cz.gif) ![x](_x.gif) ![(](lp.gif)
Spfin Spfin ![)](rp.gif)
Sfin ![(](lp.gif) ![Z](_cz.gif) ![X](_cx.gif) ![(](lp.gif) Spfin Spfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | | sfineq2 4527 |
. . . . . . . . . . . . . . 15
![(](lp.gif) Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif) Sfin ![(](lp.gif) ![q](_q.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 10 | imbi1d 308 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif)
![a](_a.gif) Sfin ![(](lp.gif) ![q](_q.gif) ![x](_x.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 11 | albidv 1625 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![A.](forall.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![q](_q.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | 12 | rspcv 2951 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif)
![A.](forall.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![A.](forall.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![q](_q.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | sfineq1 4526 |
. . . . . . . . . . . . . . 15
![(](lp.gif) Sfin ![(](lp.gif) ![q](_q.gif) ![x](_x.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | | eleq1 2413 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 14, 15 | imbi12d 311 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Sfin ![(](lp.gif) ![q](_q.gif) ![x](_x.gif)
![a](_a.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | spv 1998 |
. . . . . . . . . . . . 13
![(](lp.gif) ![A.](forall.gif) ![q](_q.gif)
Sfin ![(](lp.gif) ![q](_q.gif) ![x](_x.gif) ![a](_a.gif) Sfin ![(](lp.gif) ![z](_z.gif)
![x](_x.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 17 | com12 27 |
. . . . . . . . . . . 12
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![(](lp.gif) ![A.](forall.gif) ![q](_q.gif) Sfin
![(](lp.gif) ![q](_q.gif) ![x](_x.gif) ![a](_a.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 13, 18 | syl9r 67 |
. . . . . . . . . . 11
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![A.](forall.gif) ![q](_q.gif) Sfin
![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 19 | com23 72 |
. . . . . . . . . 10
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![(](lp.gif) ![A.](forall.gif) ![A.](forall.gif) ![q](_q.gif) Sfin
![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![(](lp.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 20 | adantld 453 |
. . . . . . . . 9
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![(](lp.gif) Ncfin ![A.](forall.gif)
![A.](forall.gif) ![q](_q.gif)
Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![)](rp.gif) ![(](lp.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 21 | a2d 23 |
. . . . . . . 8
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) Ncfin ![A.](forall.gif)
![A.](forall.gif) ![q](_q.gif)
Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![)](rp.gif) ![a](_a.gif) ![(](lp.gif) Ncfin ![A.](forall.gif) ![A.](forall.gif) ![q](_q.gif) Sfin
![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![)](rp.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 22 | alimdv 1621 |
. . . . . . 7
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![(](lp.gif) ![A.](forall.gif) ![a](_a.gif) ![(](lp.gif) Ncfin
![A.](forall.gif)
![A.](forall.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif)
![a](_a.gif) ![)](rp.gif) ![a](_a.gif) ![A.](forall.gif) ![a](_a.gif) ![(](lp.gif)
Ncfin ![A.](forall.gif)
![A.](forall.gif) ![q](_q.gif)
Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![)](rp.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | df-spfin 4447 |
. . . . . . . . 9
Spfin ![|^|](bigcap.gif) ![{](lbrace.gif) Ncfin
![A.](forall.gif)
![A.](forall.gif) ![q](_q.gif) Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
25 | 24 | eleq2i 2417 |
. . . . . . . 8
![(](lp.gif) Spfin ![|^|](bigcap.gif) ![{](lbrace.gif) Ncfin
![A.](forall.gif) ![A.](forall.gif) ![q](_q.gif) Sfin
![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
26 | | vex 2862 |
. . . . . . . . 9
![_V](rmcv.gif) |
27 | 26 | elintab 3937 |
. . . . . . . 8
![(](lp.gif) ![|^|](bigcap.gif) ![{](lbrace.gif)
Ncfin ![A.](forall.gif)
![A.](forall.gif) ![q](_q.gif)
Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![A.](forall.gif) ![a](_a.gif) ![(](lp.gif)
Ncfin ![A.](forall.gif)
![A.](forall.gif) ![q](_q.gif)
Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![)](rp.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 25, 27 | bitri 240 |
. . . . . . 7
![(](lp.gif) Spfin ![A.](forall.gif) ![a](_a.gif) ![(](lp.gif)
Ncfin ![A.](forall.gif)
![A.](forall.gif) ![q](_q.gif)
Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![)](rp.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 24 | eleq2i 2417 |
. . . . . . . 8
![(](lp.gif) Spfin ![|^|](bigcap.gif) ![{](lbrace.gif) Ncfin
![A.](forall.gif) ![A.](forall.gif) ![q](_q.gif) Sfin
![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
30 | | vex 2862 |
. . . . . . . . 9
![_V](rmcv.gif) |
31 | 30 | elintab 3937 |
. . . . . . . 8
![(](lp.gif) ![|^|](bigcap.gif) ![{](lbrace.gif)
Ncfin ![A.](forall.gif)
![A.](forall.gif) ![q](_q.gif)
Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![A.](forall.gif) ![a](_a.gif) ![(](lp.gif)
Ncfin ![A.](forall.gif)
![A.](forall.gif) ![q](_q.gif)
Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![)](rp.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 29, 31 | bitri 240 |
. . . . . . 7
![(](lp.gif) Spfin ![A.](forall.gif) ![a](_a.gif) ![(](lp.gif)
Ncfin ![A.](forall.gif)
![A.](forall.gif) ![q](_q.gif)
Sfin ![(](lp.gif) ![q](_q.gif) ![p](_p.gif) ![a](_a.gif) ![)](rp.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 23, 28, 32 | 3imtr4g 261 |
. . . . . 6
Sfin ![(](lp.gif) ![z](_z.gif) ![x](_x.gif) ![(](lp.gif) Spfin Spfin ![)](rp.gif) ![)](rp.gif) |
34 | 5, 9, 33 | vtocl2g 2918 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn Nn Sfin ![(](lp.gif) ![Z](_cz.gif) ![X](_cx.gif) ![(](lp.gif) Spfin Spfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 34 | 3adant3 975 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn Nn ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) 1
![~P](scrp.gif) ![X](_cx.gif) ![)](rp.gif)
Sfin ![(](lp.gif) ![Z](_cz.gif) ![X](_cx.gif) ![(](lp.gif) Spfin Spfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 1, 35 | sylbi 187 |
. . 3
Sfin ![(](lp.gif) ![Z](_cz.gif) ![X](_cx.gif) Sfin ![(](lp.gif) ![Z](_cz.gif)
![X](_cx.gif) ![(](lp.gif) Spfin Spfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 36 | pm2.43i 43 |
. 2
Sfin ![(](lp.gif) ![Z](_cz.gif) ![X](_cx.gif) ![(](lp.gif) Spfin Spfin ![)](rp.gif) ![)](rp.gif) |
38 | 37 | impcom 419 |
1
![(](lp.gif) ![(](lp.gif) Spfin Sfin ![(](lp.gif) ![Z](_cz.gif) ![X](_cx.gif) ![)](rp.gif) Spfin ![)](rp.gif) |