Proof of Theorem nchoicelem8
Step | Hyp | Ref
| Expression |
1 | | ce0lenc1 6239 |
. . . 4
![(](lp.gif) NC ![(](lp.gif) ![(](lp.gif) ↑c
0c
NC c Nc 1c![)](rp.gif) ![)](rp.gif) |
2 | 1 | notbid 285 |
. . 3
![(](lp.gif) NC ![(](lp.gif) ![(](lp.gif) ↑c
0c
NC c Nc 1c![)](rp.gif) ![)](rp.gif) |
3 | 2 | adantl 452 |
. 2
![(](lp.gif) c We NC NC ![(](lp.gif) ![(](lp.gif)
↑c 0c NC c Nc 1c![)](rp.gif) ![)](rp.gif) |
4 | | df-we 5906 |
. . . . . . . . . 10
We Or Fr ![)](rp.gif) |
5 | 4 | breqi 4645 |
. . . . . . . . 9
c We
NC c Or Fr NC ![)](rp.gif) |
6 | | brin 4693 |
. . . . . . . . 9
c Or Fr NC c Or NC c Fr NC ![)](rp.gif) ![)](rp.gif) |
7 | 5, 6 | bitri 240 |
. . . . . . . 8
c We
NC c Or NC c Fr NC ![)](rp.gif) ![)](rp.gif) |
8 | | sopc 5934 |
. . . . . . . . . 10
c Or
NC c Po NC c Connex NC ![)](rp.gif) ![)](rp.gif) |
9 | 8 | simprbi 450 |
. . . . . . . . 9
c Or
NC c Connex NC ![)](rp.gif) |
10 | 9 | adantr 451 |
. . . . . . . 8
![(](lp.gif) c Or NC c Fr NC c Connex NC ![)](rp.gif) |
11 | 7, 10 | sylbi 187 |
. . . . . . 7
c We
NC c Connex NC ![)](rp.gif) |
12 | | simpl 443 |
. . . . . . . 8
![(](lp.gif) c Connex NC NC c Connex NC ![)](rp.gif) |
13 | | simpr 447 |
. . . . . . . 8
![(](lp.gif) c Connex NC NC NC ![)](rp.gif) |
14 | | 1cex 4142 |
. . . . . . . . . 10
1c
![_V](rmcv.gif) |
15 | 14 | ncelncsi 6121 |
. . . . . . . . 9
Nc 1c NC |
16 | 15 | a1i 10 |
. . . . . . . 8
![(](lp.gif) c Connex NC NC Nc 1c NC ![)](rp.gif) |
17 | 12, 13, 16 | connexd 5931 |
. . . . . . 7
![(](lp.gif) c Connex NC NC ![(](lp.gif) c Nc 1c
Nc 1c c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 11, 17 | sylan 457 |
. . . . . 6
![(](lp.gif) c We NC NC ![(](lp.gif) c Nc 1c
Nc 1c c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 18 | ord 366 |
. . . . 5
![(](lp.gif) c We NC NC ![(](lp.gif) c Nc 1c
Nc 1c c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
20 | | id 19 |
. . . . . . . 8
Nc 1c Nc 1c ![M](_cm.gif) ![)](rp.gif) |
21 | | nclecid 6197 |
. . . . . . . . 9
Nc 1c NC Nc 1c c Nc
1c![)](rp.gif) |
22 | 15, 21 | ax-mp 5 |
. . . . . . . 8
Nc 1c c Nc
1c |
23 | 20, 22 | syl6eqbrr 4677 |
. . . . . . 7
Nc 1c c Nc 1c![)](rp.gif) |
24 | 23 | necon3bi 2557 |
. . . . . 6
![(](lp.gif) c Nc 1c
Nc 1c ![M](_cm.gif) ![)](rp.gif) |
25 | 24 | a1i 10 |
. . . . 5
![(](lp.gif) c We NC NC ![(](lp.gif) c Nc 1c
Nc 1c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 19, 25 | jcad 519 |
. . . 4
![(](lp.gif) c We NC NC ![(](lp.gif) c Nc 1c
Nc
1c c Nc 1c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 7 | simplbi 446 |
. . . . . . . . . . 11
c We
NC c Or NC ![)](rp.gif) |
28 | 8 | simplbi 446 |
. . . . . . . . . . 11
c Or
NC c Po NC ![)](rp.gif) |
29 | | df-partial 5902 |
. . . . . . . . . . . . . 14
Po ![(](lp.gif) Ref Trans Antisym ![)](rp.gif) |
30 | 29 | breqi 4645 |
. . . . . . . . . . . . 13
c Po
NC c ![(](lp.gif)
Ref Trans Antisym NC ![)](rp.gif) |
31 | | brin 4693 |
. . . . . . . . . . . . 13
c ![(](lp.gif) Ref Trans Antisym NC c
Ref Trans NC c Antisym NC ![)](rp.gif) ![)](rp.gif) |
32 | 30, 31 | bitri 240 |
. . . . . . . . . . . 12
c Po
NC c
Ref Trans NC c Antisym NC ![)](rp.gif) ![)](rp.gif) |
33 | 32 | simprbi 450 |
. . . . . . . . . . 11
c Po
NC c Antisym NC ![)](rp.gif) |
34 | 27, 28, 33 | 3syl 18 |
. . . . . . . . . 10
c We
NC c Antisym NC ![)](rp.gif) |
35 | 34 | adantr 451 |
. . . . . . . . 9
![(](lp.gif) c We NC NC c Antisym NC ![)](rp.gif) |
36 | 35 | adantr 451 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) c We NC NC Nc 1c c c Nc 1c![)](rp.gif) c Antisym NC ![)](rp.gif) |
37 | 15 | a1i 10 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) c We NC NC Nc 1c c c Nc 1c![)](rp.gif) Nc 1c
NC ![)](rp.gif) |
38 | | simplr 731 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) c We NC NC Nc 1c c c Nc 1c![)](rp.gif) NC ![)](rp.gif) |
39 | | simprl 732 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) c We NC NC Nc 1c c c Nc 1c![)](rp.gif) Nc 1c
c ![M](_cm.gif) ![)](rp.gif) |
40 | | simprr 733 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) c We NC NC Nc 1c c c Nc 1c![)](rp.gif) c Nc 1c![)](rp.gif) |
41 | 36, 37, 38, 39, 40 | antid 5929 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) c We NC NC Nc 1c c c Nc 1c![)](rp.gif) Nc 1c
![M](_cm.gif) ![)](rp.gif) |
42 | 41 | expr 598 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) c We NC NC Nc 1c c ![M](_cm.gif) ![(](lp.gif) c Nc 1c
Nc 1c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 42 | necon3ad 2552 |
. . . . 5
![(](lp.gif) ![(](lp.gif) c We NC NC Nc 1c c ![M](_cm.gif) Nc 1c c Nc 1c![)](rp.gif) ![)](rp.gif) |
44 | 43 | expimpd 586 |
. . . 4
![(](lp.gif) c We NC NC ![(](lp.gif) Nc
1c c Nc 1c ![M](_cm.gif)
c Nc
1c![)](rp.gif) ![)](rp.gif) |
45 | 26, 44 | impbid 183 |
. . 3
![(](lp.gif) c We NC NC ![(](lp.gif) c Nc 1c
Nc 1c c Nc 1c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
46 | | brltc 6114 |
. . 3
Nc 1c c Nc 1c c Nc
1c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 45, 46 | syl6bbr 254 |
. 2
![(](lp.gif) c We NC NC ![(](lp.gif) c Nc 1c
Nc 1c c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 3, 47 | bitrd 244 |
1
![(](lp.gif) c We NC NC ![(](lp.gif) ![(](lp.gif)
↑c 0c NC Nc
1c c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |