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 ⊢O∈V→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

Proof

Step Hyp Ref Expression
1 id ⊢x=O→x=O
2 dmeq ⊢x=O→dom⁡x=dom⁡O
3 1 2 feq12d ⊢x=O→x:dom⁡x⟶0+∞↔O:dom⁡O⟶0+∞
4 2 unieqd ⊢x=O→⋃dom⁡x=⋃dom⁡O
5 4 pweqd ⊢x=O→𝒫⋃dom⁡x=𝒫⋃dom⁡O
6 2 5 eqeq12d ⊢x=O→dom⁡x=𝒫⋃dom⁡x↔dom⁡O=𝒫⋃dom⁡O
7 3 6 anbi12d ⊢x=O→x:dom⁡x⟶0+∞∧dom⁡x=𝒫⋃dom⁡x↔O:dom⁡O⟶0+∞∧dom⁡O=𝒫⋃dom⁡O
8 fveq1 ⊢x=O→x⁡∅=O⁡∅
9 8 eqeq1d ⊢x=O→x⁡∅=0↔O⁡∅=0
10 7 9 anbi12d ⊢x=O→x:dom⁡x⟶0+∞∧dom⁡x=𝒫⋃dom⁡x∧x⁡∅=0↔O:dom⁡O⟶0+∞∧dom⁡O=𝒫⋃dom⁡O∧O⁡∅=0
11 fveq1 ⊢x=O→x⁡z=O⁡z
12 fveq1 ⊢x=O→x⁡y=O⁡y
13 11 12 breq12d ⊢x=O→x⁡z≤x⁡y↔O⁡z≤O⁡y
14 13 ralbidv ⊢x=O→∀z∈𝒫yx⁡z≤x⁡y↔∀z∈𝒫yO⁡z≤O⁡y
15 5 14 raleqbidv ⊢x=O→∀y∈𝒫⋃dom⁡x∀z∈𝒫yx⁡z≤x⁡y↔∀y∈𝒫⋃dom⁡O∀z∈𝒫yO⁡z≤O⁡y
16 10 15 anbi12d ⊢x=O→x:dom⁡x⟶0+∞∧dom⁡x=𝒫⋃dom⁡x∧x⁡∅=0∧∀y∈𝒫⋃dom⁡x∀z∈𝒫yx⁡z≤x⁡y↔O:dom⁡O⟶0+∞∧dom⁡O=𝒫⋃dom⁡O∧O⁡∅=0∧∀y∈𝒫⋃dom⁡O∀z∈𝒫yO⁡z≤O⁡y
17 2 pweqd ⊢x=O→𝒫dom⁡x=𝒫dom⁡O
18 fveq1 ⊢x=O→x⁡⋃y=O⁡⋃y
19 reseq1 ⊢x=O→x↾y=O↾y
20 19 fveq2d ⊢x=O→sum^⁡x↾y=sum^⁡O↾y
21 18 20 breq12d ⊢x=O→x⁡⋃y≤sum^⁡x↾y↔O⁡⋃y≤sum^⁡O↾y
22 21 imbi2d ⊢x=O→y≼ω→x⁡⋃y≤sum^⁡x↾y↔y≼ω→O⁡⋃y≤sum^⁡O↾y
23 17 22 raleqbidv ⊢x=O→∀y∈𝒫dom⁡xy≼ω→x⁡⋃y≤sum^⁡x↾y↔∀y∈𝒫dom⁡Oy≼ω→O⁡⋃y≤sum^⁡O↾y
24 16 23 anbi12d ⊢x=O→x:dom⁡x⟶0+∞∧dom⁡x=𝒫⋃dom⁡x∧x⁡∅=0∧∀y∈𝒫⋃dom⁡x∀z∈𝒫yx⁡z≤x⁡y∧∀y∈𝒫dom⁡xy≼ω→x⁡⋃y≤sum^⁡x↾y↔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
25 df-ome ⊢OutMeas=x|x:dom⁡x⟶0+∞∧dom⁡x=𝒫⋃dom⁡x∧x⁡∅=0∧∀y∈𝒫⋃dom⁡x∀z∈𝒫yx⁡z≤x⁡y∧∀y∈𝒫dom⁡xy≼ω→x⁡⋃y≤sum^⁡x↾y
26 24 25 elab2g ⊢O∈V→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