Metamath Proof Explorer

Theorem isome

Description: Express the predicate " O is an outer measure." Definition 113A of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion isome ( 𝑂 ∈ 𝑉 → ( 𝑂 ∈ OutMeas ↔ ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝑥 = 𝑂 → 𝑥 = 𝑂 )
2 dmeq ⊢ ( 𝑥 = 𝑂 → dom 𝑥 = dom 𝑂 )
3 1 2 feq12d ⊢ ( 𝑥 = 𝑂 → ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ↔ 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ) )
4 2 unieqd ⊢ ( 𝑥 = 𝑂 → ∪ dom 𝑥 = ∪ dom 𝑂 )
5 4 pweqd ⊢ ( 𝑥 = 𝑂 → 𝒫 ∪ dom 𝑥 = 𝒫 ∪ dom 𝑂 )
6 2 5 eqeq12d ⊢ ( 𝑥 = 𝑂 → ( dom 𝑥 = 𝒫 ∪ dom 𝑥 ↔ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) )
7 3 6 anbi12d ⊢ ( 𝑥 = 𝑂 → ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥 ) ↔ ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ) )
8 fveq1 ⊢ ( 𝑥 = 𝑂 → ( 𝑥 ‘ ∅ ) = ( 𝑂 ‘ ∅ ) )
9 8 eqeq1d ⊢ ( 𝑥 = 𝑂 → ( ( 𝑥 ‘ ∅ ) = 0 ↔ ( 𝑂 ‘ ∅ ) = 0 ) )
10 7 9 anbi12d ⊢ ( 𝑥 = 𝑂 → ( ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥 ) ∧ ( 𝑥 ‘ ∅ ) = 0 ) ↔ ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ) )
11 fveq1 ⊢ ( 𝑥 = 𝑂 → ( 𝑥 ‘ 𝑧 ) = ( 𝑂 ‘ 𝑧 ) )
12 fveq1 ⊢ ( 𝑥 = 𝑂 → ( 𝑥 ‘ 𝑦 ) = ( 𝑂 ‘ 𝑦 ) )
13 11 12 breq12d ⊢ ( 𝑥 = 𝑂 → ( ( 𝑥 ‘ 𝑧 ) ≤ ( 𝑥 ‘ 𝑦 ) ↔ ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) )
14 13 ralbidv ⊢ ( 𝑥 = 𝑂 → ( ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑥 ‘ 𝑧 ) ≤ ( 𝑥 ‘ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) )
15 5 14 raleqbidv ⊢ ( 𝑥 = 𝑂 → ( ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑥 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑥 ‘ 𝑧 ) ≤ ( 𝑥 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) )
16 10 15 anbi12d ⊢ ( 𝑥 = 𝑂 → ( ( ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥 ) ∧ ( 𝑥 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑥 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑥 ‘ 𝑧 ) ≤ ( 𝑥 ‘ 𝑦 ) ) ↔ ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ) )
17 2 pweqd ⊢ ( 𝑥 = 𝑂 → 𝒫 dom 𝑥 = 𝒫 dom 𝑂 )
18 fveq1 ⊢ ( 𝑥 = 𝑂 → ( 𝑥 ‘ ∪ 𝑦 ) = ( 𝑂 ‘ ∪ 𝑦 ) )
19 reseq1 ⊢ ( 𝑥 = 𝑂 → ( 𝑥 ↾ 𝑦 ) = ( 𝑂 ↾ 𝑦 ) )
20 19 fveq2d ⊢ ( 𝑥 = 𝑂 → ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) = ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) )
21 18 20 breq12d ⊢ ( 𝑥 = 𝑂 → ( ( 𝑥 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) ↔ ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) )
22 21 imbi2d ⊢ ( 𝑥 = 𝑂 → ( ( 𝑦 ≼ ω → ( 𝑥 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) ) ↔ ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) )
23 17 22 raleqbidv ⊢ ( 𝑥 = 𝑂 → ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≼ ω → ( 𝑥 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) )
24 16 23 anbi12d ⊢ ( 𝑥 = 𝑂 → ( ( ( ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥 ) ∧ ( 𝑥 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑥 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑥 ‘ 𝑧 ) ≤ ( 𝑥 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≼ ω → ( 𝑥 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) ) ) ↔ ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) ) )
25 df-ome ⊢ OutMeas = { 𝑥 ∣ ( ( ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥 ) ∧ ( 𝑥 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑥 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑥 ‘ 𝑧 ) ≤ ( 𝑥 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≼ ω → ( 𝑥 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) ) ) }
26 24 25 elab2g ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑂 ∈ OutMeas ↔ ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) ) )