| Step | Hyp | Ref
| Expression |
| 1 | | ssun1 4178 |
. . 3
⊢ ∪ ran ((,) ∘ 𝐹) ⊆ (∪ ran
((,) ∘ 𝐹) ∪
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹))) |
| 2 | | uniioombl.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 3 | | ovolfcl 25501 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((1st
‘(𝐹‘𝑥)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑥)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑥)) ≤ (2nd
‘(𝐹‘𝑥)))) |
| 4 | 2, 3 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1st
‘(𝐹‘𝑥)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑥)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑥)) ≤ (2nd
‘(𝐹‘𝑥)))) |
| 5 | | rexr 11307 |
. . . . . . . 8
⊢
((1st ‘(𝐹‘𝑥)) ∈ ℝ → (1st
‘(𝐹‘𝑥)) ∈
ℝ*) |
| 6 | | rexr 11307 |
. . . . . . . 8
⊢
((2nd ‘(𝐹‘𝑥)) ∈ ℝ → (2nd
‘(𝐹‘𝑥)) ∈
ℝ*) |
| 7 | | id 22 |
. . . . . . . 8
⊢
((1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥)) → (1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥))) |
| 8 | | prunioo 13521 |
. . . . . . . 8
⊢
(((1st ‘(𝐹‘𝑥)) ∈ ℝ* ∧
(2nd ‘(𝐹‘𝑥)) ∈ ℝ* ∧
(1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥))) → (((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) ∪ {(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))}) = ((1st ‘(𝐹‘𝑥))[,](2nd ‘(𝐹‘𝑥)))) |
| 9 | 5, 6, 7, 8 | syl3an 1161 |
. . . . . . 7
⊢
(((1st ‘(𝐹‘𝑥)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑥)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥))) → (((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) ∪ {(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))}) = ((1st ‘(𝐹‘𝑥))[,](2nd ‘(𝐹‘𝑥)))) |
| 10 | 4, 9 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((1st
‘(𝐹‘𝑥))(,)(2nd
‘(𝐹‘𝑥))) ∪ {(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))}) = ((1st
‘(𝐹‘𝑥))[,](2nd
‘(𝐹‘𝑥)))) |
| 11 | | fvco3 7008 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥))) |
| 12 | 2, 11 | sylan 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥))) |
| 13 | 2 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 14 | 13 | elin2d 4205 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ (ℝ ×
ℝ)) |
| 15 | | 1st2nd2 8053 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) ∈ (ℝ × ℝ) →
(𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
| 17 | 16 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((,)‘(𝐹‘𝑥)) = ((,)‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉)) |
| 18 | | df-ov 7434 |
. . . . . . . . 9
⊢
((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) = ((,)‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉) |
| 19 | 17, 18 | eqtr4di 2795 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((,)‘(𝐹‘𝑥)) = ((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥)))) |
| 20 | 12, 19 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥)))) |
| 21 | | df-pr 4629 |
. . . . . . . 8
⊢
{((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)} = ({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)}) |
| 22 | | fvco3 7008 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((1st
∘ 𝐹)‘𝑥) = (1st
‘(𝐹‘𝑥))) |
| 23 | 2, 22 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1st
∘ 𝐹)‘𝑥) = (1st
‘(𝐹‘𝑥))) |
| 24 | | fvco3 7008 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((2nd
∘ 𝐹)‘𝑥) = (2nd
‘(𝐹‘𝑥))) |
| 25 | 2, 24 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((2nd
∘ 𝐹)‘𝑥) = (2nd
‘(𝐹‘𝑥))) |
| 26 | 23, 25 | preq12d 4741 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → {((1st
∘ 𝐹)‘𝑥), ((2nd ∘
𝐹)‘𝑥)} = {(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))}) |
| 27 | 21, 26 | eqtr3id 2791 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ({((1st
∘ 𝐹)‘𝑥)} ∪ {((2nd
∘ 𝐹)‘𝑥)}) = {(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))}) |
| 28 | 20, 27 | uneq12d 4169 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((((,) ∘ 𝐹)‘𝑥) ∪ ({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)})) = (((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) ∪ {(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))})) |
| 29 | | fvco3 7008 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (([,] ∘ 𝐹)‘𝑥) = ([,]‘(𝐹‘𝑥))) |
| 30 | 2, 29 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (([,] ∘ 𝐹)‘𝑥) = ([,]‘(𝐹‘𝑥))) |
| 31 | 16 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ([,]‘(𝐹‘𝑥)) = ([,]‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉)) |
| 32 | | df-ov 7434 |
. . . . . . . 8
⊢
((1st ‘(𝐹‘𝑥))[,](2nd ‘(𝐹‘𝑥))) = ([,]‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉) |
| 33 | 31, 32 | eqtr4di 2795 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ([,]‘(𝐹‘𝑥)) = ((1st ‘(𝐹‘𝑥))[,](2nd ‘(𝐹‘𝑥)))) |
| 34 | 30, 33 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (([,] ∘ 𝐹)‘𝑥) = ((1st ‘(𝐹‘𝑥))[,](2nd ‘(𝐹‘𝑥)))) |
| 35 | 10, 28, 34 | 3eqtr4rd 2788 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (([,] ∘ 𝐹)‘𝑥) = ((((,) ∘ 𝐹)‘𝑥) ∪ ({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)}))) |
| 36 | 35 | iuneq2dv 5016 |
. . . 4
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ (([,] ∘ 𝐹)‘𝑥) = ∪ 𝑥 ∈ ℕ ((((,) ∘
𝐹)‘𝑥) ∪ ({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)}))) |
| 37 | | iccf 13488 |
. . . . . . 7
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
| 38 | | ffn 6736 |
. . . . . . 7
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → [,] Fn (ℝ* ×
ℝ*)) |
| 39 | 37, 38 | ax-mp 5 |
. . . . . 6
⊢ [,] Fn
(ℝ* × ℝ*) |
| 40 | | inss2 4238 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
| 41 | | rexpssxrxp 11306 |
. . . . . . . 8
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
| 42 | 40, 41 | sstri 3993 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
| 43 | | fss 6752 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 44 | 2, 42, 43 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 45 | | fnfco 6773 |
. . . . . 6
⊢ (([,] Fn
(ℝ* × ℝ*) ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ([,] ∘ 𝐹) Fn ℕ) |
| 46 | 39, 44, 45 | sylancr 587 |
. . . . 5
⊢ (𝜑 → ([,] ∘ 𝐹) Fn ℕ) |
| 47 | | fniunfv 7267 |
. . . . 5
⊢ (([,]
∘ 𝐹) Fn ℕ
→ ∪ 𝑥 ∈ ℕ (([,] ∘ 𝐹)‘𝑥) = ∪ ran ([,]
∘ 𝐹)) |
| 48 | 46, 47 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ (([,] ∘ 𝐹)‘𝑥) = ∪ ran ([,]
∘ 𝐹)) |
| 49 | | iunun 5093 |
. . . . 5
⊢ ∪ 𝑥 ∈ ℕ ((((,) ∘ 𝐹)‘𝑥) ∪ ({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)})) = (∪
𝑥 ∈ ℕ (((,)
∘ 𝐹)‘𝑥) ∪ ∪ 𝑥 ∈ ℕ ({((1st ∘
𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)})) |
| 50 | | ioof 13487 |
. . . . . . . . 9
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 51 | | ffn 6736 |
. . . . . . . . 9
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
| 52 | 50, 51 | ax-mp 5 |
. . . . . . . 8
⊢ (,) Fn
(ℝ* × ℝ*) |
| 53 | | fnfco 6773 |
. . . . . . . 8
⊢ (((,) Fn
(ℝ* × ℝ*) ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹) Fn ℕ) |
| 54 | 52, 44, 53 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → ((,) ∘ 𝐹) Fn ℕ) |
| 55 | | fniunfv 7267 |
. . . . . . 7
⊢ (((,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,)
∘ 𝐹)) |
| 56 | 54, 55 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,)
∘ 𝐹)) |
| 57 | | iunun 5093 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ ℕ ({((1st ∘
𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)}) = (∪
𝑥 ∈ ℕ
{((1st ∘ 𝐹)‘𝑥)} ∪ ∪
𝑥 ∈ ℕ
{((2nd ∘ 𝐹)‘𝑥)}) |
| 58 | | fo1st 8034 |
. . . . . . . . . . . . . 14
⊢
1st :V–onto→V |
| 59 | | fofn 6822 |
. . . . . . . . . . . . . 14
⊢
(1st :V–onto→V → 1st Fn V) |
| 60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
1st Fn V |
| 61 | | ssv 4008 |
. . . . . . . . . . . . . 14
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ V |
| 62 | | fss 6752 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ V) → 𝐹:ℕ⟶V) |
| 63 | 2, 61, 62 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℕ⟶V) |
| 64 | | fnfco 6773 |
. . . . . . . . . . . . 13
⊢
((1st Fn V ∧ 𝐹:ℕ⟶V) → (1st
∘ 𝐹) Fn
ℕ) |
| 65 | 60, 63, 64 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1st ∘
𝐹) Fn
ℕ) |
| 66 | | fnfun 6668 |
. . . . . . . . . . . 12
⊢
((1st ∘ 𝐹) Fn ℕ → Fun (1st
∘ 𝐹)) |
| 67 | 65, 66 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun (1st
∘ 𝐹)) |
| 68 | | fndm 6671 |
. . . . . . . . . . . 12
⊢
((1st ∘ 𝐹) Fn ℕ → dom (1st
∘ 𝐹) =
ℕ) |
| 69 | | eqimss2 4043 |
. . . . . . . . . . . 12
⊢ (dom
(1st ∘ 𝐹)
= ℕ → ℕ ⊆ dom (1st ∘ 𝐹)) |
| 70 | 65, 68, 69 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ℕ ⊆ dom
(1st ∘ 𝐹)) |
| 71 | | dfimafn2 6972 |
. . . . . . . . . . 11
⊢ ((Fun
(1st ∘ 𝐹)
∧ ℕ ⊆ dom (1st ∘ 𝐹)) → ((1st ∘ 𝐹) “ ℕ) = ∪ 𝑥 ∈ ℕ {((1st ∘
𝐹)‘𝑥)}) |
| 72 | 67, 70, 71 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st ∘
𝐹) “ ℕ) =
∪ 𝑥 ∈ ℕ {((1st ∘
𝐹)‘𝑥)}) |
| 73 | | fnima 6698 |
. . . . . . . . . . 11
⊢
((1st ∘ 𝐹) Fn ℕ → ((1st ∘
𝐹) “ ℕ) = ran
(1st ∘ 𝐹)) |
| 74 | 65, 73 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st ∘
𝐹) “ ℕ) = ran
(1st ∘ 𝐹)) |
| 75 | 72, 74 | eqtr3d 2779 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ {((1st ∘
𝐹)‘𝑥)} = ran (1st ∘ 𝐹)) |
| 76 | | rnco2 6273 |
. . . . . . . . 9
⊢ ran
(1st ∘ 𝐹)
= (1st “ ran 𝐹) |
| 77 | 75, 76 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ {((1st ∘
𝐹)‘𝑥)} = (1st “ ran 𝐹)) |
| 78 | | fo2nd 8035 |
. . . . . . . . . . . . . 14
⊢
2nd :V–onto→V |
| 79 | | fofn 6822 |
. . . . . . . . . . . . . 14
⊢
(2nd :V–onto→V → 2nd Fn V) |
| 80 | 78, 79 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
2nd Fn V |
| 81 | | fnfco 6773 |
. . . . . . . . . . . . 13
⊢
((2nd Fn V ∧ 𝐹:ℕ⟶V) → (2nd
∘ 𝐹) Fn
ℕ) |
| 82 | 80, 63, 81 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2nd ∘
𝐹) Fn
ℕ) |
| 83 | | fnfun 6668 |
. . . . . . . . . . . 12
⊢
((2nd ∘ 𝐹) Fn ℕ → Fun (2nd
∘ 𝐹)) |
| 84 | 82, 83 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun (2nd
∘ 𝐹)) |
| 85 | | fndm 6671 |
. . . . . . . . . . . 12
⊢
((2nd ∘ 𝐹) Fn ℕ → dom (2nd
∘ 𝐹) =
ℕ) |
| 86 | | eqimss2 4043 |
. . . . . . . . . . . 12
⊢ (dom
(2nd ∘ 𝐹)
= ℕ → ℕ ⊆ dom (2nd ∘ 𝐹)) |
| 87 | 82, 85, 86 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ℕ ⊆ dom
(2nd ∘ 𝐹)) |
| 88 | | dfimafn2 6972 |
. . . . . . . . . . 11
⊢ ((Fun
(2nd ∘ 𝐹)
∧ ℕ ⊆ dom (2nd ∘ 𝐹)) → ((2nd ∘ 𝐹) “ ℕ) = ∪ 𝑥 ∈ ℕ {((2nd ∘
𝐹)‘𝑥)}) |
| 89 | 84, 87, 88 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((2nd ∘
𝐹) “ ℕ) =
∪ 𝑥 ∈ ℕ {((2nd ∘
𝐹)‘𝑥)}) |
| 90 | | fnima 6698 |
. . . . . . . . . . 11
⊢
((2nd ∘ 𝐹) Fn ℕ → ((2nd ∘
𝐹) “ ℕ) = ran
(2nd ∘ 𝐹)) |
| 91 | 82, 90 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((2nd ∘
𝐹) “ ℕ) = ran
(2nd ∘ 𝐹)) |
| 92 | 89, 91 | eqtr3d 2779 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ {((2nd ∘
𝐹)‘𝑥)} = ran (2nd ∘ 𝐹)) |
| 93 | | rnco2 6273 |
. . . . . . . . 9
⊢ ran
(2nd ∘ 𝐹)
= (2nd “ ran 𝐹) |
| 94 | 92, 93 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ {((2nd ∘
𝐹)‘𝑥)} = (2nd “ ran 𝐹)) |
| 95 | 77, 94 | uneq12d 4169 |
. . . . . . 7
⊢ (𝜑 → (∪ 𝑥 ∈ ℕ {((1st ∘
𝐹)‘𝑥)} ∪ ∪
𝑥 ∈ ℕ
{((2nd ∘ 𝐹)‘𝑥)}) = ((1st “ ran 𝐹) ∪ (2nd “
ran 𝐹))) |
| 96 | 57, 95 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ ({((1st ∘
𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)}) = ((1st “ ran 𝐹) ∪ (2nd “
ran 𝐹))) |
| 97 | 56, 96 | uneq12d 4169 |
. . . . 5
⊢ (𝜑 → (∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) ∪ ∪
𝑥 ∈ ℕ
({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)})) = (∪ ran ((,)
∘ 𝐹) ∪
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)))) |
| 98 | 49, 97 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ ((((,) ∘ 𝐹)‘𝑥) ∪ ({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)})) = (∪ ran ((,)
∘ 𝐹) ∪
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)))) |
| 99 | 36, 48, 98 | 3eqtr3d 2785 |
. . 3
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) = (∪ ran ((,)
∘ 𝐹) ∪
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)))) |
| 100 | 1, 99 | sseqtrrid 4027 |
. 2
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹)) |
| 101 | | ovolficcss 25504 |
. . . . 5
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐹) ⊆
ℝ) |
| 102 | 2, 101 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ) |
| 103 | 102 | ssdifssd 4147 |
. . 3
⊢ (𝜑 → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ⊆
ℝ) |
| 104 | | omelon 9686 |
. . . . . . . . . . 11
⊢ ω
∈ On |
| 105 | | nnenom 14021 |
. . . . . . . . . . . 12
⊢ ℕ
≈ ω |
| 106 | 105 | ensymi 9044 |
. . . . . . . . . . 11
⊢ ω
≈ ℕ |
| 107 | | isnumi 9986 |
. . . . . . . . . . 11
⊢ ((ω
∈ On ∧ ω ≈ ℕ) → ℕ ∈ dom
card) |
| 108 | 104, 106,
107 | mp2an 692 |
. . . . . . . . . 10
⊢ ℕ
∈ dom card |
| 109 | | fofun 6821 |
. . . . . . . . . . . . 13
⊢
(1st :V–onto→V → Fun 1st ) |
| 110 | 58, 109 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun
1st |
| 111 | | ssv 4008 |
. . . . . . . . . . . . 13
⊢ ran 𝐹 ⊆ V |
| 112 | | fof 6820 |
. . . . . . . . . . . . . . 15
⊢
(1st :V–onto→V → 1st
:V⟶V) |
| 113 | 58, 112 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
1st :V⟶V |
| 114 | 113 | fdmi 6747 |
. . . . . . . . . . . . 13
⊢ dom
1st = V |
| 115 | 111, 114 | sseqtrri 4033 |
. . . . . . . . . . . 12
⊢ ran 𝐹 ⊆ dom
1st |
| 116 | | fores 6830 |
. . . . . . . . . . . 12
⊢ ((Fun
1st ∧ ran 𝐹
⊆ dom 1st ) → (1st ↾ ran 𝐹):ran 𝐹–onto→(1st “ ran 𝐹)) |
| 117 | 110, 115,
116 | mp2an 692 |
. . . . . . . . . . 11
⊢
(1st ↾ ran 𝐹):ran 𝐹–onto→(1st “ ran 𝐹) |
| 118 | 2 | ffnd 6737 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 Fn ℕ) |
| 119 | | dffn4 6826 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn ℕ ↔ 𝐹:ℕ–onto→ran 𝐹) |
| 120 | 118, 119 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℕ–onto→ran 𝐹) |
| 121 | | foco 6834 |
. . . . . . . . . . 11
⊢
(((1st ↾ ran 𝐹):ran 𝐹–onto→(1st “ ran 𝐹) ∧ 𝐹:ℕ–onto→ran 𝐹) → ((1st ↾ ran 𝐹) ∘ 𝐹):ℕ–onto→(1st “ ran 𝐹)) |
| 122 | 117, 120,
121 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st ↾
ran 𝐹) ∘ 𝐹):ℕ–onto→(1st “ ran 𝐹)) |
| 123 | | fodomnum 10097 |
. . . . . . . . . 10
⊢ (ℕ
∈ dom card → (((1st ↾ ran 𝐹) ∘ 𝐹):ℕ–onto→(1st “ ran 𝐹) → (1st “ ran 𝐹) ≼
ℕ)) |
| 124 | 108, 122,
123 | mpsyl 68 |
. . . . . . . . 9
⊢ (𝜑 → (1st “
ran 𝐹) ≼
ℕ) |
| 125 | | domentr 9053 |
. . . . . . . . 9
⊢
(((1st “ ran 𝐹) ≼ ℕ ∧ ℕ ≈
ω) → (1st “ ran 𝐹) ≼ ω) |
| 126 | 124, 105,
125 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → (1st “
ran 𝐹) ≼
ω) |
| 127 | | fofun 6821 |
. . . . . . . . . . . . 13
⊢
(2nd :V–onto→V → Fun 2nd ) |
| 128 | 78, 127 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun
2nd |
| 129 | | fof 6820 |
. . . . . . . . . . . . . . 15
⊢
(2nd :V–onto→V → 2nd
:V⟶V) |
| 130 | 78, 129 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
2nd :V⟶V |
| 131 | 130 | fdmi 6747 |
. . . . . . . . . . . . 13
⊢ dom
2nd = V |
| 132 | 111, 131 | sseqtrri 4033 |
. . . . . . . . . . . 12
⊢ ran 𝐹 ⊆ dom
2nd |
| 133 | | fores 6830 |
. . . . . . . . . . . 12
⊢ ((Fun
2nd ∧ ran 𝐹
⊆ dom 2nd ) → (2nd ↾ ran 𝐹):ran 𝐹–onto→(2nd “ ran 𝐹)) |
| 134 | 128, 132,
133 | mp2an 692 |
. . . . . . . . . . 11
⊢
(2nd ↾ ran 𝐹):ran 𝐹–onto→(2nd “ ran 𝐹) |
| 135 | | foco 6834 |
. . . . . . . . . . 11
⊢
(((2nd ↾ ran 𝐹):ran 𝐹–onto→(2nd “ ran 𝐹) ∧ 𝐹:ℕ–onto→ran 𝐹) → ((2nd ↾ ran 𝐹) ∘ 𝐹):ℕ–onto→(2nd “ ran 𝐹)) |
| 136 | 134, 120,
135 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → ((2nd ↾
ran 𝐹) ∘ 𝐹):ℕ–onto→(2nd “ ran 𝐹)) |
| 137 | | fodomnum 10097 |
. . . . . . . . . 10
⊢ (ℕ
∈ dom card → (((2nd ↾ ran 𝐹) ∘ 𝐹):ℕ–onto→(2nd “ ran 𝐹) → (2nd “ ran 𝐹) ≼
ℕ)) |
| 138 | 108, 136,
137 | mpsyl 68 |
. . . . . . . . 9
⊢ (𝜑 → (2nd “
ran 𝐹) ≼
ℕ) |
| 139 | | domentr 9053 |
. . . . . . . . 9
⊢
(((2nd “ ran 𝐹) ≼ ℕ ∧ ℕ ≈
ω) → (2nd “ ran 𝐹) ≼ ω) |
| 140 | 138, 105,
139 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → (2nd “
ran 𝐹) ≼
ω) |
| 141 | | unctb 10244 |
. . . . . . . 8
⊢
(((1st “ ran 𝐹) ≼ ω ∧ (2nd
“ ran 𝐹) ≼
ω) → ((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)) ≼
ω) |
| 142 | 126, 140,
141 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((1st “
ran 𝐹) ∪
(2nd “ ran 𝐹)) ≼ ω) |
| 143 | | ctex 9004 |
. . . . . . 7
⊢
(((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)) ≼ ω →
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)) ∈ V) |
| 144 | 142, 143 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((1st “
ran 𝐹) ∪
(2nd “ ran 𝐹)) ∈ V) |
| 145 | | ssid 4006 |
. . . . . . . 8
⊢ ∪ ran ([,] ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹) |
| 146 | 145, 99 | sseqtrid 4026 |
. . . . . . 7
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ⊆ (∪ ran
((,) ∘ 𝐹) ∪
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)))) |
| 147 | | ssundif 4488 |
. . . . . . 7
⊢ (∪ ran ([,] ∘ 𝐹) ⊆ (∪ ran
((,) ∘ 𝐹) ∪
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹))) ↔ (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ⊆
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹))) |
| 148 | 146, 147 | sylib 218 |
. . . . . 6
⊢ (𝜑 → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ⊆
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹))) |
| 149 | | ssdomg 9040 |
. . . . . 6
⊢
(((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)) ∈ V → ((∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ⊆
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)) → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)))) |
| 150 | 144, 148,
149 | sylc 65 |
. . . . 5
⊢ (𝜑 → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹))) |
| 151 | | domtr 9047 |
. . . . 5
⊢ (((∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)) ∧ ((1st
“ ran 𝐹) ∪
(2nd “ ran 𝐹)) ≼ ω) → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
ω) |
| 152 | 150, 142,
151 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
ω) |
| 153 | | domentr 9053 |
. . . 4
⊢ (((∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
ω ∧ ω ≈ ℕ) → (∪ ran
([,] ∘ 𝐹) ∖
∪ ran ((,) ∘ 𝐹)) ≼ ℕ) |
| 154 | 152, 106,
153 | sylancl 586 |
. . 3
⊢ (𝜑 → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
ℕ) |
| 155 | | ovolctb2 25527 |
. . 3
⊢ (((∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ⊆
ℝ ∧ (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
ℕ) → (vol*‘(∪ ran ([,] ∘
𝐹) ∖ ∪ ran ((,) ∘ 𝐹))) = 0) |
| 156 | 103, 154,
155 | syl2anc 584 |
. 2
⊢ (𝜑 → (vol*‘(∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹))) =
0) |
| 157 | 100, 156 | jca 511 |
1
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹) ∧
(vol*‘(∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹))) =
0)) |