Description: Choice-free proof of cniccibl . (Contributed by Brendan Leahy, 2-Nov-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | cnicciblnc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iccmbl | |
|
2 | cnmbf | |
|
3 | 1 2 | stoic3 | |
4 | simp3 | |
|
5 | cncff | |
|
6 | fdm | |
|
7 | 4 5 6 | 3syl | |
8 | 7 | fveq2d | |
9 | iccvolcl | |
|
10 | 9 | 3adant3 | |
11 | 8 10 | eqeltrd | |
12 | cniccbdd | |
|
13 | 7 | raleqdv | |
14 | 13 | rexbidv | |
15 | 12 14 | mpbird | |
16 | bddiblnc | |
|
17 | 3 11 15 16 | syl3anc | |