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	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	omessle.x	⊢ 𝑋 = ∪ dom 𝑂
	omessle.b	⊢ ( 𝜑 → 𝐵 ⊆ 𝑋 )
	omessle.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion	omessle	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ≤ ( 𝑂 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		omessle.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		omessle.x	⊢ 𝑋 = ∪ dom 𝑂
3		omessle.b	⊢ ( 𝜑 → 𝐵 ⊆ 𝑋 )
4		omessle.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
5	1 2	unidmex	⊢ ( 𝜑 → 𝑋 ∈ V )
6	5 3	ssexd	⊢ ( 𝜑 → 𝐵 ∈ V )
7	6 4	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
8		elpwg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )
9	7 8	syl	⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )
10	4 9	mpbird	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝐵 )
11	3 2	sseqtrdi	⊢ ( 𝜑 → 𝐵 ⊆ ∪ dom 𝑂 )
12		elpwg	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ 𝒫 ∪ dom 𝑂 ↔ 𝐵 ⊆ ∪ dom 𝑂 ) )
13	6 12	syl	⊢ ( 𝜑 → ( 𝐵 ∈ 𝒫 ∪ dom 𝑂 ↔ 𝐵 ⊆ ∪ dom 𝑂 ) )
14	11 13	mpbird	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 ∪ dom 𝑂 )
15		isome	⊢ ( 𝑂 ∈ OutMeas → ( 𝑂 ∈ OutMeas ↔ ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) ) )
16	1 15	syl	⊢ ( 𝜑 → ( 𝑂 ∈ OutMeas ↔ ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) ) )
17	1 16	mpbid	⊢ ( 𝜑 → ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) )
18	17	simplrd	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) )
19		pweq	⊢ ( 𝑦 = 𝐵 → 𝒫 𝑦 = 𝒫 𝐵 )
20	19	raleqdv	⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝒫 𝐵 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) )
21		fveq2	⊢ ( 𝑦 = 𝐵 → ( 𝑂 ‘ 𝑦 ) = ( 𝑂 ‘ 𝐵 ) )
22	21	breq2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ↔ ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝐵 ) ) )
23	22	ralbidv	⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑧 ∈ 𝒫 𝐵 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝒫 𝐵 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝐵 ) ) )
24	20 23	bitrd	⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝒫 𝐵 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝐵 ) ) )
25	24	rspcva	⊢ ( ( 𝐵 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) → ∀ 𝑧 ∈ 𝒫 𝐵 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝐵 ) )
26	14 18 25	syl2anc	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝒫 𝐵 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝐵 ) )
27		fveq2	⊢ ( 𝑧 = 𝐴 → ( 𝑂 ‘ 𝑧 ) = ( 𝑂 ‘ 𝐴 ) )
28	27	breq1d	⊢ ( 𝑧 = 𝐴 → ( ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝐵 ) ↔ ( 𝑂 ‘ 𝐴 ) ≤ ( 𝑂 ‘ 𝐵 ) ) )
29	28	rspcva	⊢ ( ( 𝐴 ∈ 𝒫 𝐵 ∧ ∀ 𝑧 ∈ 𝒫 𝐵 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝐵 ) ) → ( 𝑂 ‘ 𝐴 ) ≤ ( 𝑂 ‘ 𝐵 ) )
30	10 26 29	syl2anc	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ≤ ( 𝑂 ‘ 𝐵 ) )