Step | Hyp | Ref
| Expression |
1 | | ssun1 3738 |
. . 3
⊢ ∪ ran ((,) ∘ 𝐹) ⊆ (∪ ran
((,) ∘ 𝐹) ∪
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹))) |
2 | | uniioombl.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
3 | | ovolfcl 23042 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((1st
‘(𝐹‘𝑥)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑥)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑥)) ≤ (2nd
‘(𝐹‘𝑥)))) |
4 | 2, 3 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1st
‘(𝐹‘𝑥)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑥)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑥)) ≤ (2nd
‘(𝐹‘𝑥)))) |
5 | | rexr 9964 |
. . . . . . . 8
⊢
((1st ‘(𝐹‘𝑥)) ∈ ℝ → (1st
‘(𝐹‘𝑥)) ∈
ℝ*) |
6 | | rexr 9964 |
. . . . . . . 8
⊢
((2nd ‘(𝐹‘𝑥)) ∈ ℝ → (2nd
‘(𝐹‘𝑥)) ∈
ℝ*) |
7 | | id 22 |
. . . . . . . 8
⊢
((1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥)) → (1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥))) |
8 | | prunioo 12172 |
. . . . . . . 8
⊢
(((1st ‘(𝐹‘𝑥)) ∈ ℝ* ∧
(2nd ‘(𝐹‘𝑥)) ∈ ℝ* ∧
(1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥))) → (((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) ∪ {(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))}) = ((1st ‘(𝐹‘𝑥))[,](2nd ‘(𝐹‘𝑥)))) |
9 | 5, 6, 7, 8 | syl3an 1360 |
. . . . . . 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 6185 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥))) |
12 | 2, 11 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥))) |
13 | | inss2 3796 |
. . . . . . . . . . . 12
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
14 | 2 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
15 | 13, 14 | sseldi 3566 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ (ℝ ×
ℝ)) |
16 | | 1st2nd2 7096 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) ∈ (ℝ × ℝ) →
(𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
17 | 15, 16 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
18 | 17 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((,)‘(𝐹‘𝑥)) = ((,)‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉)) |
19 | | df-ov 6552 |
. . . . . . . . 9
⊢
((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) = ((,)‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉) |
20 | 18, 19 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((,)‘(𝐹‘𝑥)) = ((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥)))) |
21 | 12, 20 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥)))) |
22 | | df-pr 4128 |
. . . . . . . 8
⊢
{((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)} = ({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)}) |
23 | | fvco3 6185 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((1st
∘ 𝐹)‘𝑥) = (1st
‘(𝐹‘𝑥))) |
24 | 2, 23 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1st
∘ 𝐹)‘𝑥) = (1st
‘(𝐹‘𝑥))) |
25 | | fvco3 6185 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((2nd
∘ 𝐹)‘𝑥) = (2nd
‘(𝐹‘𝑥))) |
26 | 2, 25 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((2nd
∘ 𝐹)‘𝑥) = (2nd
‘(𝐹‘𝑥))) |
27 | 24, 26 | preq12d 4220 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → {((1st
∘ 𝐹)‘𝑥), ((2nd ∘
𝐹)‘𝑥)} = {(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))}) |
28 | 22, 27 | syl5eqr 2658 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ({((1st
∘ 𝐹)‘𝑥)} ∪ {((2nd
∘ 𝐹)‘𝑥)}) = {(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))}) |
29 | 21, 28 | uneq12d 3730 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((((,) ∘ 𝐹)‘𝑥) ∪ ({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)})) = (((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) ∪ {(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))})) |
30 | | fvco3 6185 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (([,] ∘ 𝐹)‘𝑥) = ([,]‘(𝐹‘𝑥))) |
31 | 2, 30 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (([,] ∘ 𝐹)‘𝑥) = ([,]‘(𝐹‘𝑥))) |
32 | 17 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ([,]‘(𝐹‘𝑥)) = ([,]‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉)) |
33 | | df-ov 6552 |
. . . . . . . 8
⊢
((1st ‘(𝐹‘𝑥))[,](2nd ‘(𝐹‘𝑥))) = ([,]‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉) |
34 | 32, 33 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ([,]‘(𝐹‘𝑥)) = ((1st ‘(𝐹‘𝑥))[,](2nd ‘(𝐹‘𝑥)))) |
35 | 31, 34 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (([,] ∘ 𝐹)‘𝑥) = ((1st ‘(𝐹‘𝑥))[,](2nd ‘(𝐹‘𝑥)))) |
36 | 10, 29, 35 | 3eqtr4rd 2655 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (([,] ∘ 𝐹)‘𝑥) = ((((,) ∘ 𝐹)‘𝑥) ∪ ({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)}))) |
37 | 36 | iuneq2dv 4478 |
. . . 4
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ (([,] ∘ 𝐹)‘𝑥) = ∪ 𝑥 ∈ ℕ ((((,) ∘
𝐹)‘𝑥) ∪ ({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)}))) |
38 | | iccf 12143 |
. . . . . . 7
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
39 | | ffn 5958 |
. . . . . . 7
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → [,] Fn (ℝ* ×
ℝ*)) |
40 | 38, 39 | ax-mp 5 |
. . . . . 6
⊢ [,] Fn
(ℝ* × ℝ*) |
41 | | rexpssxrxp 9963 |
. . . . . . . 8
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
42 | 13, 41 | sstri 3577 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
43 | | fss 5969 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
44 | 2, 42, 43 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
45 | | fnfco 5982 |
. . . . . 6
⊢ (([,] Fn
(ℝ* × ℝ*) ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ([,] ∘ 𝐹) Fn ℕ) |
46 | 40, 44, 45 | sylancr 694 |
. . . . 5
⊢ (𝜑 → ([,] ∘ 𝐹) Fn ℕ) |
47 | | fniunfv 6409 |
. . . . 5
⊢ (([,]
∘ 𝐹) Fn ℕ
→ ∪ 𝑥 ∈ ℕ (([,] ∘ 𝐹)‘𝑥) = ∪ ran ([,]
∘ 𝐹)) |
48 | 46, 47 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ (([,] ∘ 𝐹)‘𝑥) = ∪ ran ([,]
∘ 𝐹)) |
49 | | iunun 4540 |
. . . . 5
⊢ ∪ 𝑥 ∈ ℕ ((((,) ∘ 𝐹)‘𝑥) ∪ ({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)})) = (∪
𝑥 ∈ ℕ (((,)
∘ 𝐹)‘𝑥) ∪ ∪ 𝑥 ∈ ℕ ({((1st ∘
𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)})) |
50 | | ioof 12142 |
. . . . . . . . 9
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
51 | | ffn 5958 |
. . . . . . . . 9
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . 8
⊢ (,) Fn
(ℝ* × ℝ*) |
53 | | fnfco 5982 |
. . . . . . . 8
⊢ (((,) Fn
(ℝ* × ℝ*) ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹) Fn ℕ) |
54 | 52, 44, 53 | sylancr 694 |
. . . . . . 7
⊢ (𝜑 → ((,) ∘ 𝐹) Fn ℕ) |
55 | | fniunfv 6409 |
. . . . . . 7
⊢ (((,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,)
∘ 𝐹)) |
56 | 54, 55 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,)
∘ 𝐹)) |
57 | | iunun 4540 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ ℕ ({((1st ∘
𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)}) = (∪
𝑥 ∈ ℕ
{((1st ∘ 𝐹)‘𝑥)} ∪ ∪
𝑥 ∈ ℕ
{((2nd ∘ 𝐹)‘𝑥)}) |
58 | | fo1st 7079 |
. . . . . . . . . . . . . 14
⊢
1st :V–onto→V |
59 | | fofn 6030 |
. . . . . . . . . . . . . 14
⊢
(1st :V–onto→V → 1st Fn V) |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
1st Fn V |
61 | | ssv 3588 |
. . . . . . . . . . . . . 14
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ V |
62 | | fss 5969 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ V) → 𝐹:ℕ⟶V) |
63 | 2, 61, 62 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℕ⟶V) |
64 | | fnfco 5982 |
. . . . . . . . . . . . 13
⊢
((1st Fn V ∧ 𝐹:ℕ⟶V) → (1st
∘ 𝐹) Fn
ℕ) |
65 | 60, 63, 64 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1st ∘
𝐹) Fn
ℕ) |
66 | | fnfun 5902 |
. . . . . . . . . . . 12
⊢
((1st ∘ 𝐹) Fn ℕ → Fun (1st
∘ 𝐹)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun (1st
∘ 𝐹)) |
68 | | fndm 5904 |
. . . . . . . . . . . 12
⊢
((1st ∘ 𝐹) Fn ℕ → dom (1st
∘ 𝐹) =
ℕ) |
69 | | eqimss2 3621 |
. . . . . . . . . . . 12
⊢ (dom
(1st ∘ 𝐹)
= ℕ → ℕ ⊆ dom (1st ∘ 𝐹)) |
70 | 65, 68, 69 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ℕ ⊆ dom
(1st ∘ 𝐹)) |
71 | | dfimafn2 6156 |
. . . . . . . . . . 11
⊢ ((Fun
(1st ∘ 𝐹)
∧ ℕ ⊆ dom (1st ∘ 𝐹)) → ((1st ∘ 𝐹) “ ℕ) = ∪ 𝑥 ∈ ℕ {((1st ∘
𝐹)‘𝑥)}) |
72 | 67, 70, 71 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st ∘
𝐹) “ ℕ) =
∪ 𝑥 ∈ ℕ {((1st ∘
𝐹)‘𝑥)}) |
73 | | fnima 5923 |
. . . . . . . . . . 11
⊢
((1st ∘ 𝐹) Fn ℕ → ((1st ∘
𝐹) “ ℕ) = ran
(1st ∘ 𝐹)) |
74 | 65, 73 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st ∘
𝐹) “ ℕ) = ran
(1st ∘ 𝐹)) |
75 | 72, 74 | eqtr3d 2646 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ {((1st ∘
𝐹)‘𝑥)} = ran (1st ∘ 𝐹)) |
76 | | rnco2 5559 |
. . . . . . . . 9
⊢ ran
(1st ∘ 𝐹)
= (1st “ ran 𝐹) |
77 | 75, 76 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ {((1st ∘
𝐹)‘𝑥)} = (1st “ ran 𝐹)) |
78 | | fo2nd 7080 |
. . . . . . . . . . . . . 14
⊢
2nd :V–onto→V |
79 | | fofn 6030 |
. . . . . . . . . . . . . 14
⊢
(2nd :V–onto→V → 2nd Fn V) |
80 | 78, 79 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
2nd Fn V |
81 | | fnfco 5982 |
. . . . . . . . . . . . 13
⊢
((2nd Fn V ∧ 𝐹:ℕ⟶V) → (2nd
∘ 𝐹) Fn
ℕ) |
82 | 80, 63, 81 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2nd ∘
𝐹) Fn
ℕ) |
83 | | fnfun 5902 |
. . . . . . . . . . . 12
⊢
((2nd ∘ 𝐹) Fn ℕ → Fun (2nd
∘ 𝐹)) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun (2nd
∘ 𝐹)) |
85 | | fndm 5904 |
. . . . . . . . . . . 12
⊢
((2nd ∘ 𝐹) Fn ℕ → dom (2nd
∘ 𝐹) =
ℕ) |
86 | | eqimss2 3621 |
. . . . . . . . . . . 12
⊢ (dom
(2nd ∘ 𝐹)
= ℕ → ℕ ⊆ dom (2nd ∘ 𝐹)) |
87 | 82, 85, 86 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ℕ ⊆ dom
(2nd ∘ 𝐹)) |
88 | | dfimafn2 6156 |
. . . . . . . . . . 11
⊢ ((Fun
(2nd ∘ 𝐹)
∧ ℕ ⊆ dom (2nd ∘ 𝐹)) → ((2nd ∘ 𝐹) “ ℕ) = ∪ 𝑥 ∈ ℕ {((2nd ∘
𝐹)‘𝑥)}) |
89 | 84, 87, 88 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ((2nd ∘
𝐹) “ ℕ) =
∪ 𝑥 ∈ ℕ {((2nd ∘
𝐹)‘𝑥)}) |
90 | | fnima 5923 |
. . . . . . . . . . 11
⊢
((2nd ∘ 𝐹) Fn ℕ → ((2nd ∘
𝐹) “ ℕ) = ran
(2nd ∘ 𝐹)) |
91 | 82, 90 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((2nd ∘
𝐹) “ ℕ) = ran
(2nd ∘ 𝐹)) |
92 | 89, 91 | eqtr3d 2646 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ {((2nd ∘
𝐹)‘𝑥)} = ran (2nd ∘ 𝐹)) |
93 | | rnco2 5559 |
. . . . . . . . 9
⊢ ran
(2nd ∘ 𝐹)
= (2nd “ ran 𝐹) |
94 | 92, 93 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ {((2nd ∘
𝐹)‘𝑥)} = (2nd “ ran 𝐹)) |
95 | 77, 94 | uneq12d 3730 |
. . . . . . 7
⊢ (𝜑 → (∪ 𝑥 ∈ ℕ {((1st ∘
𝐹)‘𝑥)} ∪ ∪
𝑥 ∈ ℕ
{((2nd ∘ 𝐹)‘𝑥)}) = ((1st “ ran 𝐹) ∪ (2nd “
ran 𝐹))) |
96 | 57, 95 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ ({((1st ∘
𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)}) = ((1st “ ran 𝐹) ∪ (2nd “
ran 𝐹))) |
97 | 56, 96 | uneq12d 3730 |
. . . . 5
⊢ (𝜑 → (∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) ∪ ∪
𝑥 ∈ ℕ
({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)})) = (∪ ran ((,)
∘ 𝐹) ∪
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)))) |
98 | 49, 97 | syl5eq 2656 |
. . . 4
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ ((((,) ∘ 𝐹)‘𝑥) ∪ ({((1st ∘ 𝐹)‘𝑥)} ∪ {((2nd ∘ 𝐹)‘𝑥)})) = (∪ ran ((,)
∘ 𝐹) ∪
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)))) |
99 | 37, 48, 98 | 3eqtr3d 2652 |
. . 3
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) = (∪ ran ((,)
∘ 𝐹) ∪
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)))) |
100 | 1, 99 | syl5sseqr 3617 |
. 2
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹)) |
101 | | ovolficcss 23045 |
. . . . 5
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐹) ⊆
ℝ) |
102 | 2, 101 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ) |
103 | 102 | ssdifssd 3710 |
. . 3
⊢ (𝜑 → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ⊆
ℝ) |
104 | | omelon 8426 |
. . . . . . . . . . 11
⊢ ω
∈ On |
105 | | nnenom 12641 |
. . . . . . . . . . . 12
⊢ ℕ
≈ ω |
106 | 105 | ensymi 7892 |
. . . . . . . . . . 11
⊢ ω
≈ ℕ |
107 | | isnumi 8655 |
. . . . . . . . . . 11
⊢ ((ω
∈ On ∧ ω ≈ ℕ) → ℕ ∈ dom
card) |
108 | 104, 106,
107 | mp2an 704 |
. . . . . . . . . 10
⊢ ℕ
∈ dom card |
109 | | fofun 6029 |
. . . . . . . . . . . . 13
⊢
(1st :V–onto→V → Fun 1st ) |
110 | 58, 109 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun
1st |
111 | | ssv 3588 |
. . . . . . . . . . . . 13
⊢ ran 𝐹 ⊆ V |
112 | | fof 6028 |
. . . . . . . . . . . . . . 15
⊢
(1st :V–onto→V → 1st
:V⟶V) |
113 | 58, 112 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
1st :V⟶V |
114 | 113 | fdmi 5965 |
. . . . . . . . . . . . 13
⊢ dom
1st = V |
115 | 111, 114 | sseqtr4i 3601 |
. . . . . . . . . . . 12
⊢ ran 𝐹 ⊆ dom
1st |
116 | | fores 6037 |
. . . . . . . . . . . 12
⊢ ((Fun
1st ∧ ran 𝐹
⊆ dom 1st ) → (1st ↾ ran 𝐹):ran 𝐹–onto→(1st “ ran 𝐹)) |
117 | 110, 115,
116 | mp2an 704 |
. . . . . . . . . . 11
⊢
(1st ↾ ran 𝐹):ran 𝐹–onto→(1st “ ran 𝐹) |
118 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝐹 Fn ℕ) |
119 | 2, 118 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 Fn ℕ) |
120 | | dffn4 6034 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn ℕ ↔ 𝐹:ℕ–onto→ran 𝐹) |
121 | 119, 120 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℕ–onto→ran 𝐹) |
122 | | foco 6038 |
. . . . . . . . . . 11
⊢
(((1st ↾ ran 𝐹):ran 𝐹–onto→(1st “ ran 𝐹) ∧ 𝐹:ℕ–onto→ran 𝐹) → ((1st ↾ ran 𝐹) ∘ 𝐹):ℕ–onto→(1st “ ran 𝐹)) |
123 | 117, 121,
122 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st ↾
ran 𝐹) ∘ 𝐹):ℕ–onto→(1st “ ran 𝐹)) |
124 | | fodomnum 8763 |
. . . . . . . . . 10
⊢ (ℕ
∈ dom card → (((1st ↾ ran 𝐹) ∘ 𝐹):ℕ–onto→(1st “ ran 𝐹) → (1st “ ran 𝐹) ≼
ℕ)) |
125 | 108, 123,
124 | mpsyl 66 |
. . . . . . . . 9
⊢ (𝜑 → (1st “
ran 𝐹) ≼
ℕ) |
126 | | domentr 7901 |
. . . . . . . . 9
⊢
(((1st “ ran 𝐹) ≼ ℕ ∧ ℕ ≈
ω) → (1st “ ran 𝐹) ≼ ω) |
127 | 125, 105,
126 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → (1st “
ran 𝐹) ≼
ω) |
128 | | fofun 6029 |
. . . . . . . . . . . . 13
⊢
(2nd :V–onto→V → Fun 2nd ) |
129 | 78, 128 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun
2nd |
130 | | fof 6028 |
. . . . . . . . . . . . . . 15
⊢
(2nd :V–onto→V → 2nd
:V⟶V) |
131 | 78, 130 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
2nd :V⟶V |
132 | 131 | fdmi 5965 |
. . . . . . . . . . . . 13
⊢ dom
2nd = V |
133 | 111, 132 | sseqtr4i 3601 |
. . . . . . . . . . . 12
⊢ ran 𝐹 ⊆ dom
2nd |
134 | | fores 6037 |
. . . . . . . . . . . 12
⊢ ((Fun
2nd ∧ ran 𝐹
⊆ dom 2nd ) → (2nd ↾ ran 𝐹):ran 𝐹–onto→(2nd “ ran 𝐹)) |
135 | 129, 133,
134 | mp2an 704 |
. . . . . . . . . . 11
⊢
(2nd ↾ ran 𝐹):ran 𝐹–onto→(2nd “ ran 𝐹) |
136 | | foco 6038 |
. . . . . . . . . . 11
⊢
(((2nd ↾ ran 𝐹):ran 𝐹–onto→(2nd “ ran 𝐹) ∧ 𝐹:ℕ–onto→ran 𝐹) → ((2nd ↾ ran 𝐹) ∘ 𝐹):ℕ–onto→(2nd “ ran 𝐹)) |
137 | 135, 121,
136 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝜑 → ((2nd ↾
ran 𝐹) ∘ 𝐹):ℕ–onto→(2nd “ ran 𝐹)) |
138 | | fodomnum 8763 |
. . . . . . . . . 10
⊢ (ℕ
∈ dom card → (((2nd ↾ ran 𝐹) ∘ 𝐹):ℕ–onto→(2nd “ ran 𝐹) → (2nd “ ran 𝐹) ≼
ℕ)) |
139 | 108, 137,
138 | mpsyl 66 |
. . . . . . . . 9
⊢ (𝜑 → (2nd “
ran 𝐹) ≼
ℕ) |
140 | | domentr 7901 |
. . . . . . . . 9
⊢
(((2nd “ ran 𝐹) ≼ ℕ ∧ ℕ ≈
ω) → (2nd “ ran 𝐹) ≼ ω) |
141 | 139, 105,
140 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → (2nd “
ran 𝐹) ≼
ω) |
142 | | unctb 8910 |
. . . . . . . 8
⊢
(((1st “ ran 𝐹) ≼ ω ∧ (2nd
“ ran 𝐹) ≼
ω) → ((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)) ≼
ω) |
143 | 127, 141,
142 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((1st “
ran 𝐹) ∪
(2nd “ ran 𝐹)) ≼ ω) |
144 | | reldom 7847 |
. . . . . . . 8
⊢ Rel
≼ |
145 | 144 | brrelexi 5082 |
. . . . . . 7
⊢
(((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)) ≼ ω →
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)) ∈ V) |
146 | 143, 145 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((1st “
ran 𝐹) ∪
(2nd “ ran 𝐹)) ∈ V) |
147 | | ssid 3587 |
. . . . . . . 8
⊢ ∪ ran ([,] ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹) |
148 | 147, 99 | syl5sseq 3616 |
. . . . . . 7
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ⊆ (∪ ran
((,) ∘ 𝐹) ∪
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)))) |
149 | | ssundif 4004 |
. . . . . . 7
⊢ (∪ ran ([,] ∘ 𝐹) ⊆ (∪ ran
((,) ∘ 𝐹) ∪
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹))) ↔ (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ⊆
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹))) |
150 | 148, 149 | sylib 207 |
. . . . . 6
⊢ (𝜑 → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ⊆
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹))) |
151 | | ssdomg 7887 |
. . . . . 6
⊢
(((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)) ∈ V → ((∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ⊆
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)) → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)))) |
152 | 146, 150,
151 | sylc 63 |
. . . . 5
⊢ (𝜑 → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹))) |
153 | | domtr 7895 |
. . . . 5
⊢ (((∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
((1st “ ran 𝐹) ∪ (2nd “ ran 𝐹)) ∧ ((1st
“ ran 𝐹) ∪
(2nd “ ran 𝐹)) ≼ ω) → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
ω) |
154 | 152, 143,
153 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
ω) |
155 | | domentr 7901 |
. . . 4
⊢ (((∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
ω ∧ ω ≈ ℕ) → (∪ ran
([,] ∘ 𝐹) ∖
∪ ran ((,) ∘ 𝐹)) ≼ ℕ) |
156 | 154, 106,
155 | sylancl 693 |
. . 3
⊢ (𝜑 → (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
ℕ) |
157 | | ovolctb2 23067 |
. . 3
⊢ (((∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ⊆
ℝ ∧ (∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹)) ≼
ℕ) → (vol*‘(∪ ran ([,] ∘
𝐹) ∖ ∪ ran ((,) ∘ 𝐹))) = 0) |
158 | 103, 156,
157 | syl2anc 691 |
. 2
⊢ (𝜑 → (vol*‘(∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹))) =
0) |
159 | 100, 158 | jca 553 |
1
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹) ∧
(vol*‘(∪ ran ([,] ∘ 𝐹) ∖ ∪ ran
((,) ∘ 𝐹))) =
0)) |