Metamath Proof Explorer


Theorem cnicciblnc

Description: Choice-free proof of cniccibl . (Contributed by Brendan Leahy, 2-Nov-2017)

Ref Expression
Assertion cnicciblnc ABF:ABcnF𝐿1

Proof

Step Hyp Ref Expression
1 iccmbl ABABdomvol
2 cnmbf ABdomvolF:ABcnFMblFn
3 1 2 stoic3 ABF:ABcnFMblFn
4 simp3 ABF:ABcnF:ABcn
5 cncff F:ABcnF:AB
6 fdm F:ABdomF=AB
7 4 5 6 3syl ABF:ABcndomF=AB
8 7 fveq2d ABF:ABcnvoldomF=volAB
9 iccvolcl ABvolAB
10 9 3adant3 ABF:ABcnvolAB
11 8 10 eqeltrd ABF:ABcnvoldomF
12 cniccbdd ABF:ABcnxyABFyx
13 7 raleqdv ABF:ABcnydomFFyxyABFyx
14 13 rexbidv ABF:ABcnxydomFFyxxyABFyx
15 12 14 mpbird ABF:ABcnxydomFFyx
16 bddiblnc FMblFnvoldomFxydomFFyxF𝐿1
17 3 11 15 16 syl3anc ABF:ABcnF𝐿1