Metamath Proof Explorer


Theorem uniiccdif

Description: A union of closed intervals differs from the equivalent union of open intervals by a nullset. (Contributed by Mario Carneiro, 25-Mar-2015)

Ref Expression
Hypothesis uniioombl.1 φ F : 2
Assertion uniiccdif φ ran . F ran . F vol * ran . F ran . F = 0

Proof

Step Hyp Ref Expression
1 uniioombl.1 φ F : 2
2 ssun1 ran . F ran . F 1 st ran F 2 nd ran F
3 ovolfcl F : 2 x 1 st F x 2 nd F x 1 st F x 2 nd F x
4 1 3 sylan φ x 1 st F x 2 nd F x 1 st F x 2 nd F x
5 rexr 1 st F x 1 st F x *
6 rexr 2 nd F x 2 nd F x *
7 id 1 st F x 2 nd F x 1 st F x 2 nd F x
8 prunioo 1 st F x * 2 nd F x * 1 st F x 2 nd F x 1 st F x 2 nd F x 1 st F x 2 nd F x = 1 st F x 2 nd F x
9 5 6 7 8 syl3an 1 st F x 2 nd F x 1 st F x 2 nd F x 1 st F x 2 nd F x 1 st F x 2 nd F x = 1 st F x 2 nd F x
10 4 9 syl φ x 1 st F x 2 nd F x 1 st F x 2 nd F x = 1 st F x 2 nd F x
11 fvco3 F : 2 x . F x = . F x
12 1 11 sylan φ x . F x = . F x
13 1 ffvelrnda φ x F x 2
14 13 elin2d φ x F x 2
15 1st2nd2 F x 2 F x = 1 st F x 2 nd F x
16 14 15 syl φ x F x = 1 st F x 2 nd F x
17 16 fveq2d φ x . F x = . 1 st F x 2 nd F x
18 df-ov 1 st F x 2 nd F x = . 1 st F x 2 nd F x
19 17 18 eqtr4di φ x . F x = 1 st F x 2 nd F x
20 12 19 eqtrd φ x . F x = 1 st F x 2 nd F x
21 df-pr 1 st F x 2 nd F x = 1 st F x 2 nd F x
22 fvco3 F : 2 x 1 st F x = 1 st F x
23 1 22 sylan φ x 1 st F x = 1 st F x
24 fvco3 F : 2 x 2 nd F x = 2 nd F x
25 1 24 sylan φ x 2 nd F x = 2 nd F x
26 23 25 preq12d φ x 1 st F x 2 nd F x = 1 st F x 2 nd F x
27 21 26 eqtr3id φ x 1 st F x 2 nd F x = 1 st F x 2 nd F x
28 20 27 uneq12d φ x . F x 1 st F x 2 nd F x = 1 st F x 2 nd F x 1 st F x 2 nd F x
29 fvco3 F : 2 x . F x = . F x
30 1 29 sylan φ x . F x = . F x
31 16 fveq2d φ x . F x = . 1 st F x 2 nd F x
32 df-ov 1 st F x 2 nd F x = . 1 st F x 2 nd F x
33 31 32 eqtr4di φ x . F x = 1 st F x 2 nd F x
34 30 33 eqtrd φ x . F x = 1 st F x 2 nd F x
35 10 28 34 3eqtr4rd φ x . F x = . F x 1 st F x 2 nd F x
36 35 iuneq2dv φ x . F x = x . F x 1 st F x 2 nd F x
37 iccf . : * × * 𝒫 *
38 ffn . : * × * 𝒫 * . Fn * × *
39 37 38 ax-mp . Fn * × *
40 inss2 2 2
41 rexpssxrxp 2 * × *
42 40 41 sstri 2 * × *
43 fss F : 2 2 * × * F : * × *
44 1 42 43 sylancl φ F : * × *
45 fnfco . Fn * × * F : * × * . F Fn
46 39 44 45 sylancr φ . F Fn
47 fniunfv . F Fn x . F x = ran . F
48 46 47 syl φ x . F x = ran . F
49 iunun x . F x 1 st F x 2 nd F x = x . F x x 1 st F x 2 nd F x
50 ioof . : * × * 𝒫
51 ffn . : * × * 𝒫 . Fn * × *
52 50 51 ax-mp . Fn * × *
53 fnfco . Fn * × * F : * × * . F Fn
54 52 44 53 sylancr φ . F Fn
55 fniunfv . F Fn x . F x = ran . F
56 54 55 syl φ x . F x = ran . F
57 iunun x 1 st F x 2 nd F x = x 1 st F x x 2 nd F x
58 fo1st 1 st : V onto V
59 fofn 1 st : V onto V 1 st Fn V
60 58 59 ax-mp 1 st Fn V
61 ssv 2 V
62 fss F : 2 2 V F : V
63 1 61 62 sylancl φ F : V
64 fnfco 1 st Fn V F : V 1 st F Fn
65 60 63 64 sylancr φ 1 st F Fn
66 fnfun 1 st F Fn Fun 1 st F
67 65 66 syl φ Fun 1 st F
68 fndm 1 st F Fn dom 1 st F =
69 eqimss2 dom 1 st F = dom 1 st F
70 65 68 69 3syl φ dom 1 st F
71 dfimafn2 Fun 1 st F dom 1 st F 1 st F = x 1 st F x
72 67 70 71 syl2anc φ 1 st F = x 1 st F x
73 fnima 1 st F Fn 1 st F = ran 1 st F
74 65 73 syl φ 1 st F = ran 1 st F
75 72 74 eqtr3d φ x 1 st F x = ran 1 st F
76 rnco2 ran 1 st F = 1 st ran F
77 75 76 eqtrdi φ x 1 st F x = 1 st ran F
78 fo2nd 2 nd : V onto V
79 fofn 2 nd : V onto V 2 nd Fn V
80 78 79 ax-mp 2 nd Fn V
81 fnfco 2 nd Fn V F : V 2 nd F Fn
82 80 63 81 sylancr φ 2 nd F Fn
83 fnfun 2 nd F Fn Fun 2 nd F
84 82 83 syl φ Fun 2 nd F
85 fndm 2 nd F Fn dom 2 nd F =
86 eqimss2 dom 2 nd F = dom 2 nd F
87 82 85 86 3syl φ dom 2 nd F
88 dfimafn2 Fun 2 nd F dom 2 nd F 2 nd F = x 2 nd F x
89 84 87 88 syl2anc φ 2 nd F = x 2 nd F x
90 fnima 2 nd F Fn 2 nd F = ran 2 nd F
91 82 90 syl φ 2 nd F = ran 2 nd F
92 89 91 eqtr3d φ x 2 nd F x = ran 2 nd F
93 rnco2 ran 2 nd F = 2 nd ran F
94 92 93 eqtrdi φ x 2 nd F x = 2 nd ran F
95 77 94 uneq12d φ x 1 st F x x 2 nd F x = 1 st ran F 2 nd ran F
96 57 95 syl5eq φ x 1 st F x 2 nd F x = 1 st ran F 2 nd ran F
97 56 96 uneq12d φ x . F x x 1 st F x 2 nd F x = ran . F 1 st ran F 2 nd ran F
98 49 97 syl5eq φ x . F x 1 st F x 2 nd F x = ran . F 1 st ran F 2 nd ran F
99 36 48 98 3eqtr3d φ ran . F = ran . F 1 st ran F 2 nd ran F
100 2 99 sseqtrrid φ ran . F ran . F
101 ovolficcss F : 2 ran . F
102 1 101 syl φ ran . F
103 102 ssdifssd φ ran . F ran . F
104 omelon ω On
105 nnenom ω
106 105 ensymi ω
107 isnumi ω On ω dom card
108 104 106 107 mp2an dom card
109 fofun 1 st : V onto V Fun 1 st
110 58 109 ax-mp Fun 1 st
111 ssv ran F V
112 fof 1 st : V onto V 1 st : V V
113 58 112 ax-mp 1 st : V V
114 113 fdmi dom 1 st = V
115 111 114 sseqtrri ran F dom 1 st
116 fores Fun 1 st ran F dom 1 st 1 st ran F : ran F onto 1 st ran F
117 110 115 116 mp2an 1 st ran F : ran F onto 1 st ran F
118 1 ffnd φ F Fn
119 dffn4 F Fn F : onto ran F
120 118 119 sylib φ F : onto ran F
121 foco 1 st ran F : ran F onto 1 st ran F F : onto ran F 1 st ran F F : onto 1 st ran F
122 117 120 121 sylancr φ 1 st ran F F : onto 1 st ran F
123 fodomnum dom card 1 st ran F F : onto 1 st ran F 1 st ran F
124 108 122 123 mpsyl φ 1 st ran F
125 domentr 1 st ran F ω 1 st ran F ω
126 124 105 125 sylancl φ 1 st ran F ω
127 fofun 2 nd : V onto V Fun 2 nd
128 78 127 ax-mp Fun 2 nd
129 fof 2 nd : V onto V 2 nd : V V
130 78 129 ax-mp 2 nd : V V
131 130 fdmi dom 2 nd = V
132 111 131 sseqtrri ran F dom 2 nd
133 fores Fun 2 nd ran F dom 2 nd 2 nd ran F : ran F onto 2 nd ran F
134 128 132 133 mp2an 2 nd ran F : ran F onto 2 nd ran F
135 foco 2 nd ran F : ran F onto 2 nd ran F F : onto ran F 2 nd ran F F : onto 2 nd ran F
136 134 120 135 sylancr φ 2 nd ran F F : onto 2 nd ran F
137 fodomnum dom card 2 nd ran F F : onto 2 nd ran F 2 nd ran F
138 108 136 137 mpsyl φ 2 nd ran F
139 domentr 2 nd ran F ω 2 nd ran F ω
140 138 105 139 sylancl φ 2 nd ran F ω
141 unctb 1 st ran F ω 2 nd ran F ω 1 st ran F 2 nd ran F ω
142 126 140 141 syl2anc φ 1 st ran F 2 nd ran F ω
143 ctex 1 st ran F 2 nd ran F ω 1 st ran F 2 nd ran F V
144 142 143 syl φ 1 st ran F 2 nd ran F V
145 ssid ran . F ran . F
146 145 99 sseqtrid φ ran . F ran . F 1 st ran F 2 nd ran F
147 ssundif ran . F ran . F 1 st ran F 2 nd ran F ran . F ran . F 1 st ran F 2 nd ran F
148 146 147 sylib φ ran . F ran . F 1 st ran F 2 nd ran F
149 ssdomg 1 st ran F 2 nd ran F V ran . F ran . F 1 st ran F 2 nd ran F ran . F ran . F 1 st ran F 2 nd ran F
150 144 148 149 sylc φ ran . F ran . F 1 st ran F 2 nd ran F
151 domtr ran . F ran . F 1 st ran F 2 nd ran F 1 st ran F 2 nd ran F ω ran . F ran . F ω
152 150 142 151 syl2anc φ ran . F ran . F ω
153 domentr ran . F ran . F ω ω ran . F ran . F
154 152 106 153 sylancl φ ran . F ran . F
155 ovolctb2 ran . F ran . F ran . F ran . F vol * ran . F ran . F = 0
156 103 154 155 syl2anc φ vol * ran . F ran . F = 0
157 100 156 jca φ ran . F ran . F vol * ran . F ran . F = 0