Metamath Proof Explorer

Theorem omessle

Description: The outer measure of a set is greater than or equal to the measure of a subset, Definition 113A (ii) of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses omessle.o ⊢φ→O∈OutMeas
omessle.x ⊢X=⋃dom⁡O
omessle.b ⊢φ→B⊆X
omessle.a ⊢φ→A⊆B
Assertion omessle ⊢φ→O⁡A≤O⁡B

Proof

Step Hyp Ref Expression
1 omessle.o ⊢φ→O∈OutMeas
2 omessle.x ⊢X=⋃dom⁡O
3 omessle.b ⊢φ→B⊆X
4 omessle.a ⊢φ→A⊆B
5 1 2 unidmex ⊢φ→X∈V
6 5 3 ssexd ⊢φ→B∈V
7 6 4 ssexd ⊢φ→A∈V
8 elpwg ⊢A∈V→A∈𝒫B↔A⊆B
9 7 8 syl ⊢φ→A∈𝒫B↔A⊆B
10 4 9 mpbird ⊢φ→A∈𝒫B
11 3 2 sseqtrdi ⊢φ→B⊆⋃dom⁡O
12 elpwg ⊢B∈V→B∈𝒫⋃dom⁡O↔B⊆⋃dom⁡O
13 6 12 syl ⊢φ→B∈𝒫⋃dom⁡O↔B⊆⋃dom⁡O
14 11 13 mpbird ⊢φ→B∈𝒫⋃dom⁡O
15 isome ⊢O∈OutMeas→O∈OutMeas↔O:dom⁡O⟶0+∞∧dom⁡O=𝒫⋃dom⁡O∧O⁡∅=0∧∀y∈𝒫⋃dom⁡O∀z∈𝒫yO⁡z≤O⁡y∧∀y∈𝒫dom⁡Oy≼ω→O⁡⋃y≤sum^⁡O↾y
16 1 15 syl ⊢φ→O∈OutMeas↔O:dom⁡O⟶0+∞∧dom⁡O=𝒫⋃dom⁡O∧O⁡∅=0∧∀y∈𝒫⋃dom⁡O∀z∈𝒫yO⁡z≤O⁡y∧∀y∈𝒫dom⁡Oy≼ω→O⁡⋃y≤sum^⁡O↾y
17 1 16 mpbid ⊢φ→O:dom⁡O⟶0+∞∧dom⁡O=𝒫⋃dom⁡O∧O⁡∅=0∧∀y∈𝒫⋃dom⁡O∀z∈𝒫yO⁡z≤O⁡y∧∀y∈𝒫dom⁡Oy≼ω→O⁡⋃y≤sum^⁡O↾y
18 17 simplrd ⊢φ→∀y∈𝒫⋃dom⁡O∀z∈𝒫yO⁡z≤O⁡y
19 pweq ⊢y=B→𝒫y=𝒫B
20 19 raleqdv ⊢y=B→∀z∈𝒫yO⁡z≤O⁡y↔∀z∈𝒫BO⁡z≤O⁡y
21 fveq2 ⊢y=B→O⁡y=O⁡B
22 21 breq2d ⊢y=B→O⁡z≤O⁡y↔O⁡z≤O⁡B
23 22 ralbidv ⊢y=B→∀z∈𝒫BO⁡z≤O⁡y↔∀z∈𝒫BO⁡z≤O⁡B
24 20 23 bitrd ⊢y=B→∀z∈𝒫yO⁡z≤O⁡y↔∀z∈𝒫BO⁡z≤O⁡B
25 24 rspcva ⊢B∈𝒫⋃dom⁡O∧∀y∈𝒫⋃dom⁡O∀z∈𝒫yO⁡z≤O⁡y→∀z∈𝒫BO⁡z≤O⁡B
26 14 18 25 syl2anc ⊢φ→∀z∈𝒫BO⁡z≤O⁡B
27 fveq2 ⊢z=A→O⁡z=O⁡A
28 27 breq1d ⊢z=A→O⁡z≤O⁡B↔O⁡A≤O⁡B
29 28 rspcva ⊢A∈𝒫B∧∀z∈𝒫BO⁡z≤O⁡B→O⁡A≤O⁡B
30 10 26 29 syl2anc ⊢φ→O⁡A≤O⁡B