Metamath Proof Explorer


Theorem ovnssle

Description: The (multidimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnssle.1 φ X Fin
ovnssle.2 φ A B
ovnssle.3 φ B X
Assertion ovnssle φ voln* X A voln* X B

Proof

Step Hyp Ref Expression
1 ovnssle.1 φ X Fin
2 ovnssle.2 φ A B
3 ovnssle.3 φ B X
4 0le0 0 0
5 4 a1i φ X = 0 0
6 fveq2 X = voln* X = voln*
7 6 fveq1d X = voln* X A = voln* A
8 7 adantl φ X = voln* X A = voln* A
9 2 adantr φ X = A B
10 3 adantr φ X = B X
11 simpr φ X = X =
12 11 oveq2d φ X = X =
13 10 12 sseqtrd φ X = B
14 9 13 sstrd φ X = A
15 14 ovn0val φ X = voln* A = 0
16 8 15 eqtrd φ X = voln* X A = 0
17 6 fveq1d X = voln* X B = voln* B
18 17 adantl φ X = voln* X B = voln* B
19 13 ovn0val φ X = voln* B = 0
20 18 19 eqtrd φ X = voln* X B = 0
21 16 20 breq12d φ X = voln* X A voln* X B 0 0
22 5 21 mpbird φ X = voln* X A voln* X B
23 1 adantr φ ¬ X = X Fin
24 neqne ¬ X = X
25 24 adantl φ ¬ X = X
26 2 adantr φ ¬ X = A B
27 3 adantr φ ¬ X = B X
28 eqid z * | i 2 X A j k X . i j k z = sum^ j k X vol . i j k = z * | i 2 X A j k X . i j k z = sum^ j k X vol . i j k
29 eqid z * | i 2 X B j k X . i j k z = sum^ j k X vol . i j k = z * | i 2 X B j k X . i j k z = sum^ j k X vol . i j k
30 23 25 26 27 28 29 ovnsslelem φ ¬ X = voln* X A voln* X B
31 22 30 pm2.61dan φ voln* X A voln* X B