| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ovolval4lem2.a | . 2
⊢ (𝜑 → 𝐴 ⊆ ℝ) | 
| 2 |  | ovolval4lem2.m | . . 3
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} | 
| 3 |  | iftrue 4531 | . . . . . . . . . . . . . . 15
⊢
((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛))) = (2nd ‘(𝑓‘𝑛))) | 
| 4 | 3 | opeq2d 4880 | . . . . . . . . . . . . . 14
⊢
((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → 〈(1st ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛)))〉 = 〈(1st
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛))〉) | 
| 5 | 4 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 =
〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉) | 
| 6 |  | df-br 5144 | . . . . . . . . . . . . . . 15
⊢
((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) ↔ 〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉 ∈ ≤ ) | 
| 7 | 6 | biimpi 216 | . . . . . . . . . . . . . 14
⊢
((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → 〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉 ∈ ≤ ) | 
| 8 | 7 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛))〉 ∈ ≤
) | 
| 9 | 5, 8 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ ≤
) | 
| 10 |  | iffalse 4534 | . . . . . . . . . . . . . . 15
⊢ (¬
(1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛))) = (1st ‘(𝑓‘𝑛))) | 
| 11 | 10 | opeq2d 4880 | . . . . . . . . . . . . . 14
⊢ (¬
(1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → 〈(1st ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛)))〉 = 〈(1st
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))〉) | 
| 12 | 11 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ ¬ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 =
〈(1st ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛))〉) | 
| 13 |  | elmapi 8889 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝑓:ℕ⟶(ℝ ×
ℝ)) | 
| 14 | 13 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ (ℝ ×
ℝ)) | 
| 15 |  | xp1st 8046 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑓‘𝑛) ∈ (ℝ × ℝ) →
(1st ‘(𝑓‘𝑛)) ∈ ℝ) | 
| 16 | 14, 15 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝑓‘𝑛)) ∈
ℝ) | 
| 17 | 16 | leidd 11829 | . . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝑓‘𝑛)) ≤ (1st
‘(𝑓‘𝑛))) | 
| 18 |  | df-br 5144 | . . . . . . . . . . . . . . 15
⊢
((1st ‘(𝑓‘𝑛)) ≤ (1st ‘(𝑓‘𝑛)) ↔ 〈(1st ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛))〉 ∈ ≤ ) | 
| 19 | 17, 18 | sylib 218 | . . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))〉 ∈ ≤
) | 
| 20 | 19 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ ¬ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))〉 ∈ ≤
) | 
| 21 | 12, 20 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ ¬ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ ≤
) | 
| 22 | 9, 21 | pm2.61dan 813 | . . . . . . . . . . 11
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ ≤
) | 
| 23 |  | xp2nd 8047 | . . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑛) ∈ (ℝ × ℝ) →
(2nd ‘(𝑓‘𝑛)) ∈ ℝ) | 
| 24 | 14, 23 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝑓‘𝑛)) ∈
ℝ) | 
| 25 | 24, 16 | ifcld 4572 | . . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))) ∈
ℝ) | 
| 26 |  | opelxpi 5722 | . . . . . . . . . . . 12
⊢
(((1st ‘(𝑓‘𝑛)) ∈ ℝ ∧ if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))) ∈ ℝ) →
〈(1st ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛)))〉 ∈ (ℝ ×
ℝ)) | 
| 27 | 16, 25, 26 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ (ℝ
× ℝ)) | 
| 28 | 22, 27 | elind 4200 | . . . . . . . . . 10
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ ( ≤ ∩
(ℝ × ℝ))) | 
| 29 |  | ovolval4lem2.g | . . . . . . . . . 10
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉) | 
| 30 | 28, 29 | fmptd 7134 | . . . . . . . . 9
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 31 |  | reex 11246 | . . . . . . . . . . . . 13
⊢ ℝ
∈ V | 
| 32 | 31, 31 | xpex 7773 | . . . . . . . . . . . 12
⊢ (ℝ
× ℝ) ∈ V | 
| 33 | 32 | inex2 5318 | . . . . . . . . . . 11
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V | 
| 34 | 33 | a1i 11 | . . . . . . . . . 10
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ( ≤ ∩ (ℝ ×
ℝ)) ∈ V) | 
| 35 |  | nnex 12272 | . . . . . . . . . . 11
⊢ ℕ
∈ V | 
| 36 | 35 | a1i 11 | . . . . . . . . . 10
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ℕ ∈ V) | 
| 37 | 34, 36 | elmapd 8880 | . . . . . . . . 9
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (𝐺 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ)))) | 
| 38 | 30, 37 | mpbird 257 | . . . . . . . 8
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝐺 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) | 
| 39 | 38 | adantr 480 | . . . . . . 7
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → 𝐺 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) | 
| 40 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝑓)) | 
| 41 |  | rexpssxrxp 11306 | . . . . . . . . . . . . . . 15
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) | 
| 42 | 41 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (ℝ × ℝ) ⊆
(ℝ* × ℝ*)) | 
| 43 | 13, 42 | fssd 6753 | . . . . . . . . . . . . 13
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝑓:ℕ⟶(ℝ* ×
ℝ*)) | 
| 44 |  | 2fveq3 6911 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (1st ‘(𝑓‘𝑘)) = (1st ‘(𝑓‘𝑛))) | 
| 45 |  | 2fveq3 6911 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (2nd ‘(𝑓‘𝑘)) = (2nd ‘(𝑓‘𝑛))) | 
| 46 | 44, 45 | breq12d 5156 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((1st ‘(𝑓‘𝑘)) ≤ (2nd ‘(𝑓‘𝑘)) ↔ (1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)))) | 
| 47 | 46 | cbvrabv 3447 | . . . . . . . . . . . . 13
⊢ {𝑘 ∈ ℕ ∣
(1st ‘(𝑓‘𝑘)) ≤ (2nd ‘(𝑓‘𝑘))} = {𝑛 ∈ ℕ ∣ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))} | 
| 48 | 43, 29, 47 | ovolval4lem1 46664 | . . . . . . . . . . . 12
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (∪ ran
((,) ∘ 𝑓) = ∪ ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝑓)) = (vol ∘ ((,) ∘
𝐺)))) | 
| 49 | 48 | simpld 494 | . . . . . . . . . . 11
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪ ran
((,) ∘ 𝑓) = ∪ ran ((,) ∘ 𝐺)) | 
| 50 | 49 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
∪ ran ((,) ∘ 𝑓) = ∪ ran ((,)
∘ 𝐺)) | 
| 51 | 40, 50 | sseqtrd 4020 | . . . . . . . . 9
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝐺)) | 
| 52 | 51 | adantrr 717 | . . . . . . . 8
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → 𝐴 ⊆ ∪ ran
((,) ∘ 𝐺)) | 
| 53 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) | 
| 54 | 48 | simprd 495 | . . . . . . . . . . . . 13
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (vol ∘ ((,) ∘ 𝑓)) = (vol ∘ ((,) ∘
𝐺))) | 
| 55 |  | coass 6285 | . . . . . . . . . . . . . 14
⊢ ((vol
∘ (,)) ∘ 𝑓) =
(vol ∘ ((,) ∘ 𝑓)) | 
| 56 | 55 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((vol ∘ (,)) ∘ 𝑓) = (vol ∘ ((,) ∘
𝑓))) | 
| 57 |  | coass 6285 | . . . . . . . . . . . . . 14
⊢ ((vol
∘ (,)) ∘ 𝐺) =
(vol ∘ ((,) ∘ 𝐺)) | 
| 58 | 57 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((vol ∘ (,)) ∘ 𝐺) = (vol ∘ ((,) ∘
𝐺))) | 
| 59 | 54, 56, 58 | 3eqtr4d 2787 | . . . . . . . . . . . 12
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((vol ∘ (,)) ∘ 𝑓) = ((vol ∘ (,)) ∘
𝐺)) | 
| 60 | 59 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) | 
| 61 | 60 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) | 
| 62 | 53, 61 | eqtrd 2777 | . . . . . . . . 9
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) | 
| 63 | 62 | adantrl 716 | . . . . . . . 8
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) | 
| 64 | 52, 63 | jca 511 | . . . . . . 7
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐺) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺)))) | 
| 65 |  | coeq2 5869 | . . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → ((,) ∘ 𝑔) = ((,) ∘ 𝐺)) | 
| 66 | 65 | rneqd 5949 | . . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ran ((,) ∘ 𝑔) = ran ((,) ∘ 𝐺)) | 
| 67 | 66 | unieqd 4920 | . . . . . . . . . 10
⊢ (𝑔 = 𝐺 → ∪ ran
((,) ∘ 𝑔) = ∪ ran ((,) ∘ 𝐺)) | 
| 68 | 67 | sseq2d 4016 | . . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ↔
𝐴 ⊆ ∪ ran ((,) ∘ 𝐺))) | 
| 69 |  | coeq2 5869 | . . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ((vol ∘ (,)) ∘ 𝑔) = ((vol ∘ (,)) ∘
𝐺)) | 
| 70 | 69 | fveq2d 6910 | . . . . . . . . . 10
⊢ (𝑔 = 𝐺 →
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) | 
| 71 | 70 | eqeq2d 2748 | . . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) ↔ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺)))) | 
| 72 | 68, 71 | anbi12d 632 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝐺) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))))) | 
| 73 | 72 | rspcev 3622 | . . . . . . 7
⊢ ((𝐺 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝐺) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺)))) → ∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) | 
| 74 | 39, 64, 73 | syl2anc 584 | . . . . . 6
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → ∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) | 
| 75 | 74 | rexlimiva 3147 | . . . . 5
⊢
(∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) | 
| 76 |  | inss2 4238 | . . . . . . . . . 10
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) | 
| 77 |  | mapss 8929 | . . . . . . . . . 10
⊢
(((ℝ × ℝ) ∈ V ∧ ( ≤ ∩ (ℝ ×
ℝ)) ⊆ (ℝ × ℝ)) → (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ⊆ ((ℝ ×
ℝ) ↑m ℕ)) | 
| 78 | 32, 76, 77 | mp2an 692 | . . . . . . . . 9
⊢ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ) ⊆ ((ℝ
× ℝ) ↑m ℕ) | 
| 79 | 78 | sseli 3979 | . . . . . . . 8
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → 𝑔 ∈ ((ℝ × ℝ)
↑m ℕ)) | 
| 80 | 79 | adantr 480 | . . . . . . 7
⊢ ((𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) → 𝑔 ∈ ((ℝ × ℝ)
↑m ℕ)) | 
| 81 |  | simpr 484 | . . . . . . 7
⊢ ((𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) | 
| 82 |  | coeq2 5869 | . . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → ((,) ∘ 𝑓) = ((,) ∘ 𝑔)) | 
| 83 | 82 | rneqd 5949 | . . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ran ((,) ∘ 𝑓) = ran ((,) ∘ 𝑔)) | 
| 84 | 83 | unieqd 4920 | . . . . . . . . . 10
⊢ (𝑓 = 𝑔 → ∪ ran ((,)
∘ 𝑓) = ∪ ran ((,) ∘ 𝑔)) | 
| 85 | 84 | sseq2d 4016 | . . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ↔
𝐴 ⊆ ∪ ran ((,) ∘ 𝑔))) | 
| 86 |  | coeq2 5869 | . . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ((vol ∘ (,)) ∘ 𝑓) = ((vol ∘ (,)) ∘
𝑔)) | 
| 87 | 86 | fveq2d 6910 | . . . . . . . . . 10
⊢ (𝑓 = 𝑔 →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) | 
| 88 | 87 | eqeq2d 2748 | . . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) | 
| 89 | 85, 88 | anbi12d 632 | . . . . . . . 8
⊢ (𝑓 = 𝑔 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))))) | 
| 90 | 89 | rspcev 3622 | . . . . . . 7
⊢ ((𝑔 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) | 
| 91 | 80, 81, 90 | syl2anc 584 | . . . . . 6
⊢ ((𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) | 
| 92 | 91 | rexlimiva 3147 | . . . . 5
⊢
(∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) | 
| 93 | 75, 92 | impbii 209 | . . . 4
⊢
(∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) | 
| 94 | 93 | rabbii 3442 | . . 3
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} = {𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} | 
| 95 | 2, 94 | eqtri 2765 | . 2
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} | 
| 96 | 1, 95 | ovolval3 46662 | 1
⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, <
)) |