Step | Hyp | Ref
| Expression |
1 | | unissb 4873 |
. . 3
⊢ (∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ⊆ (ℝ ×
ℝ) ↔ ∀𝑧
∈ (ran (𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))𝑧 ⊆ (ℝ ×
ℝ)) |
2 | | elun 4083 |
. . . 4
⊢ (𝑧 ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ↔ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∨ 𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))))) |
3 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) =
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) |
4 | 3 | rnmptss 6996 |
. . . . . . . 8
⊢
(∀𝑒 ∈
ℝ ((𝑒[,)+∞)
× ℝ) ∈ 𝒫 (ℝ × ℝ) → ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
⊆ 𝒫 (ℝ × ℝ)) |
5 | | pnfxr 11029 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
6 | | icossre 13160 |
. . . . . . . . . . 11
⊢ ((𝑒 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑒[,)+∞) ⊆
ℝ) |
7 | 5, 6 | mpan2 688 |
. . . . . . . . . 10
⊢ (𝑒 ∈ ℝ → (𝑒[,)+∞) ⊆
ℝ) |
8 | | xpss1 5608 |
. . . . . . . . . 10
⊢ ((𝑒[,)+∞) ⊆ ℝ
→ ((𝑒[,)+∞)
× ℝ) ⊆ (ℝ × ℝ)) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝑒 ∈ ℝ → ((𝑒[,)+∞) × ℝ)
⊆ (ℝ × ℝ)) |
10 | | ovex 7308 |
. . . . . . . . . . 11
⊢ (𝑒[,)+∞) ∈
V |
11 | | reex 10962 |
. . . . . . . . . . 11
⊢ ℝ
∈ V |
12 | 10, 11 | xpex 7603 |
. . . . . . . . . 10
⊢ ((𝑒[,)+∞) × ℝ)
∈ V |
13 | 12 | elpw 4537 |
. . . . . . . . 9
⊢ (((𝑒[,)+∞) × ℝ)
∈ 𝒫 (ℝ × ℝ) ↔ ((𝑒[,)+∞) × ℝ) ⊆
(ℝ × ℝ)) |
14 | 9, 13 | sylibr 233 |
. . . . . . . 8
⊢ (𝑒 ∈ ℝ → ((𝑒[,)+∞) × ℝ)
∈ 𝒫 (ℝ × ℝ)) |
15 | 4, 14 | mprg 3078 |
. . . . . . 7
⊢ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ⊆ 𝒫 (ℝ × ℝ) |
16 | 15 | sseli 3917 |
. . . . . 6
⊢ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) → 𝑧 ∈ 𝒫 (ℝ
× ℝ)) |
17 | 16 | elpwid 4544 |
. . . . 5
⊢ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) → 𝑧 ⊆ (ℝ ×
ℝ)) |
18 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑓 ∈ ℝ ↦ (ℝ
× (𝑓[,)+∞))) =
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) |
19 | 18 | rnmptss 6996 |
. . . . . . . 8
⊢
(∀𝑓 ∈
ℝ (ℝ × (𝑓[,)+∞)) ∈ 𝒫 (ℝ
× ℝ) → ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) ⊆
𝒫 (ℝ × ℝ)) |
20 | | icossre 13160 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑓[,)+∞) ⊆
ℝ) |
21 | 5, 20 | mpan2 688 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ℝ → (𝑓[,)+∞) ⊆
ℝ) |
22 | | xpss2 5609 |
. . . . . . . . . 10
⊢ ((𝑓[,)+∞) ⊆ ℝ
→ (ℝ × (𝑓[,)+∞)) ⊆ (ℝ ×
ℝ)) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝑓 ∈ ℝ → (ℝ
× (𝑓[,)+∞))
⊆ (ℝ × ℝ)) |
24 | | ovex 7308 |
. . . . . . . . . . 11
⊢ (𝑓[,)+∞) ∈
V |
25 | 11, 24 | xpex 7603 |
. . . . . . . . . 10
⊢ (ℝ
× (𝑓[,)+∞))
∈ V |
26 | 25 | elpw 4537 |
. . . . . . . . 9
⊢ ((ℝ
× (𝑓[,)+∞))
∈ 𝒫 (ℝ × ℝ) ↔ (ℝ × (𝑓[,)+∞)) ⊆ (ℝ
× ℝ)) |
27 | 23, 26 | sylibr 233 |
. . . . . . . 8
⊢ (𝑓 ∈ ℝ → (ℝ
× (𝑓[,)+∞))
∈ 𝒫 (ℝ × ℝ)) |
28 | 19, 27 | mprg 3078 |
. . . . . . 7
⊢ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) ⊆ 𝒫 (ℝ
× ℝ) |
29 | 28 | sseli 3917 |
. . . . . 6
⊢ (𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) →
𝑧 ∈ 𝒫 (ℝ
× ℝ)) |
30 | 29 | elpwid 4544 |
. . . . 5
⊢ (𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) →
𝑧 ⊆ (ℝ ×
ℝ)) |
31 | 17, 30 | jaoi 854 |
. . . 4
⊢ ((𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∨ 𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) →
𝑧 ⊆ (ℝ ×
ℝ)) |
32 | 2, 31 | sylbi 216 |
. . 3
⊢ (𝑧 ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) → 𝑧 ⊆ (ℝ ×
ℝ)) |
33 | 1, 32 | mprgbir 3079 |
. 2
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ⊆ (ℝ ×
ℝ) |
34 | | funmpt 6472 |
. . . . . 6
⊢ Fun
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) |
35 | | rexr 11021 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) ∈
ℝ*) |
36 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → +∞ ∈
ℝ*) |
37 | | ltpnf 12856 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) <
+∞) |
38 | | lbico1 13133 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑧) ∈ ℝ* ∧ +∞
∈ ℝ* ∧ (1st ‘𝑧) < +∞) → (1st
‘𝑧) ∈
((1st ‘𝑧)[,)+∞)) |
39 | 35, 36, 37, 38 | syl3anc 1370 |
. . . . . . . . . 10
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) ∈
((1st ‘𝑧)[,)+∞)) |
40 | 39 | anim1i 615 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) ∈ ℝ ∧ (2nd
‘𝑧) ∈ ℝ)
→ ((1st ‘𝑧) ∈ ((1st ‘𝑧)[,)+∞) ∧
(2nd ‘𝑧)
∈ ℝ)) |
41 | 40 | anim2i 617 |
. . . . . . . 8
⊢ ((𝑧 ∈ (V × V) ∧
((1st ‘𝑧)
∈ ℝ ∧ (2nd ‘𝑧) ∈ ℝ)) → (𝑧 ∈ (V × V) ∧ ((1st
‘𝑧) ∈
((1st ‘𝑧)[,)+∞) ∧ (2nd
‘𝑧) ∈
ℝ))) |
42 | | elxp7 7866 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℝ ×
ℝ) ↔ (𝑧 ∈
(V × V) ∧ ((1st ‘𝑧) ∈ ℝ ∧ (2nd
‘𝑧) ∈
ℝ))) |
43 | | elxp7 7866 |
. . . . . . . 8
⊢ (𝑧 ∈ (((1st
‘𝑧)[,)+∞)
× ℝ) ↔ (𝑧
∈ (V × V) ∧ ((1st ‘𝑧) ∈ ((1st ‘𝑧)[,)+∞) ∧
(2nd ‘𝑧)
∈ ℝ))) |
44 | 41, 42, 43 | 3imtr4i 292 |
. . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
(((1st ‘𝑧)[,)+∞) ×
ℝ)) |
45 | | xp1st 7863 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (1st ‘𝑧) ∈ ℝ) |
46 | | oveq1 7282 |
. . . . . . . . . 10
⊢ (𝑒 = (1st ‘𝑧) → (𝑒[,)+∞) = ((1st ‘𝑧)[,)+∞)) |
47 | 46 | xpeq1d 5618 |
. . . . . . . . 9
⊢ (𝑒 = (1st ‘𝑧) → ((𝑒[,)+∞) × ℝ) =
(((1st ‘𝑧)[,)+∞) ×
ℝ)) |
48 | | ovex 7308 |
. . . . . . . . . 10
⊢
((1st ‘𝑧)[,)+∞) ∈ V |
49 | 48, 11 | xpex 7603 |
. . . . . . . . 9
⊢
(((1st ‘𝑧)[,)+∞) × ℝ) ∈
V |
50 | 47, 3, 49 | fvmpt 6875 |
. . . . . . . 8
⊢
((1st ‘𝑧) ∈ ℝ → ((𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧)) = (((1st ‘𝑧)[,)+∞) ×
ℝ)) |
51 | 45, 50 | syl 17 |
. . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → ((𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧)) = (((1st ‘𝑧)[,)+∞) ×
ℝ)) |
52 | 44, 51 | eleqtrrd 2842 |
. . . . . 6
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
((𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧))) |
53 | | elunirn2 7126 |
. . . . . 6
⊢ ((Fun
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∧ 𝑧 ∈
((𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧))) → 𝑧 ∈ ∪ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))) |
54 | 34, 52, 53 | sylancr 587 |
. . . . 5
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))) |
55 | 54 | ssriv 3925 |
. . . 4
⊢ (ℝ
× ℝ) ⊆ ∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ)) |
56 | | ssun3 4108 |
. . . 4
⊢ ((ℝ
× ℝ) ⊆ ∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) →
(ℝ × ℝ) ⊆ (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))))) |
57 | 55, 56 | ax-mp 5 |
. . 3
⊢ (ℝ
× ℝ) ⊆ (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) |
58 | | uniun 4864 |
. . 3
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) |
59 | 57, 58 | sseqtrri 3958 |
. 2
⊢ (ℝ
× ℝ) ⊆ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) |
60 | 33, 59 | eqssi 3937 |
1
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = (ℝ ×
ℝ) |