Step | Hyp | Ref
| Expression |
1 | | unissb 4869 |
. . 3
⊢ (∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ⊆ (ℝ ×
ℝ) ↔ ∀𝑧
∈ (ran (𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))𝑧 ⊆ (ℝ ×
ℝ)) |
2 | | elun 4124 |
. . . 4
⊢ (𝑧 ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ↔ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∨ 𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))))) |
3 | | eqid 2821 |
. . . . . . . . 9
⊢ (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) =
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) |
4 | 3 | rnmptss 6885 |
. . . . . . . 8
⊢
(∀𝑒 ∈
ℝ ((𝑒[,)+∞)
× ℝ) ∈ 𝒫 (ℝ × ℝ) → ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
⊆ 𝒫 (ℝ × ℝ)) |
5 | | pnfxr 10694 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
6 | | icossre 12816 |
. . . . . . . . . . 11
⊢ ((𝑒 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑒[,)+∞) ⊆
ℝ) |
7 | 5, 6 | mpan2 689 |
. . . . . . . . . 10
⊢ (𝑒 ∈ ℝ → (𝑒[,)+∞) ⊆
ℝ) |
8 | | xpss1 5573 |
. . . . . . . . . 10
⊢ ((𝑒[,)+∞) ⊆ ℝ
→ ((𝑒[,)+∞)
× ℝ) ⊆ (ℝ × ℝ)) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝑒 ∈ ℝ → ((𝑒[,)+∞) × ℝ)
⊆ (ℝ × ℝ)) |
10 | | ovex 7188 |
. . . . . . . . . . 11
⊢ (𝑒[,)+∞) ∈
V |
11 | | reex 10627 |
. . . . . . . . . . 11
⊢ ℝ
∈ V |
12 | 10, 11 | xpex 7475 |
. . . . . . . . . 10
⊢ ((𝑒[,)+∞) × ℝ)
∈ V |
13 | 12 | elpw 4542 |
. . . . . . . . 9
⊢ (((𝑒[,)+∞) × ℝ)
∈ 𝒫 (ℝ × ℝ) ↔ ((𝑒[,)+∞) × ℝ) ⊆
(ℝ × ℝ)) |
14 | 9, 13 | sylibr 236 |
. . . . . . . 8
⊢ (𝑒 ∈ ℝ → ((𝑒[,)+∞) × ℝ)
∈ 𝒫 (ℝ × ℝ)) |
15 | 4, 14 | mprg 3152 |
. . . . . . 7
⊢ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ⊆ 𝒫 (ℝ × ℝ) |
16 | 15 | sseli 3962 |
. . . . . 6
⊢ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) → 𝑧 ∈ 𝒫 (ℝ
× ℝ)) |
17 | 16 | elpwid 4549 |
. . . . 5
⊢ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) → 𝑧 ⊆ (ℝ ×
ℝ)) |
18 | | eqid 2821 |
. . . . . . . . 9
⊢ (𝑓 ∈ ℝ ↦ (ℝ
× (𝑓[,)+∞))) =
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) |
19 | 18 | rnmptss 6885 |
. . . . . . . 8
⊢
(∀𝑓 ∈
ℝ (ℝ × (𝑓[,)+∞)) ∈ 𝒫 (ℝ
× ℝ) → ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) ⊆
𝒫 (ℝ × ℝ)) |
20 | | icossre 12816 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑓[,)+∞) ⊆
ℝ) |
21 | 5, 20 | mpan2 689 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ℝ → (𝑓[,)+∞) ⊆
ℝ) |
22 | | xpss2 5574 |
. . . . . . . . . 10
⊢ ((𝑓[,)+∞) ⊆ ℝ
→ (ℝ × (𝑓[,)+∞)) ⊆ (ℝ ×
ℝ)) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝑓 ∈ ℝ → (ℝ
× (𝑓[,)+∞))
⊆ (ℝ × ℝ)) |
24 | | ovex 7188 |
. . . . . . . . . . 11
⊢ (𝑓[,)+∞) ∈
V |
25 | 11, 24 | xpex 7475 |
. . . . . . . . . 10
⊢ (ℝ
× (𝑓[,)+∞))
∈ V |
26 | 25 | elpw 4542 |
. . . . . . . . 9
⊢ ((ℝ
× (𝑓[,)+∞))
∈ 𝒫 (ℝ × ℝ) ↔ (ℝ × (𝑓[,)+∞)) ⊆ (ℝ
× ℝ)) |
27 | 23, 26 | sylibr 236 |
. . . . . . . 8
⊢ (𝑓 ∈ ℝ → (ℝ
× (𝑓[,)+∞))
∈ 𝒫 (ℝ × ℝ)) |
28 | 19, 27 | mprg 3152 |
. . . . . . 7
⊢ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) ⊆ 𝒫 (ℝ
× ℝ) |
29 | 28 | sseli 3962 |
. . . . . 6
⊢ (𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) →
𝑧 ∈ 𝒫 (ℝ
× ℝ)) |
30 | 29 | elpwid 4549 |
. . . . 5
⊢ (𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) →
𝑧 ⊆ (ℝ ×
ℝ)) |
31 | 17, 30 | jaoi 853 |
. . . 4
⊢ ((𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∨ 𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) →
𝑧 ⊆ (ℝ ×
ℝ)) |
32 | 2, 31 | sylbi 219 |
. . 3
⊢ (𝑧 ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) → 𝑧 ⊆ (ℝ ×
ℝ)) |
33 | 1, 32 | mprgbir 3153 |
. 2
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ⊆ (ℝ ×
ℝ) |
34 | | funmpt 6392 |
. . . . . 6
⊢ Fun
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) |
35 | | rexr 10686 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) ∈
ℝ*) |
36 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → +∞ ∈
ℝ*) |
37 | | ltpnf 12514 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) <
+∞) |
38 | | lbico1 12790 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑧) ∈ ℝ* ∧ +∞
∈ ℝ* ∧ (1st ‘𝑧) < +∞) → (1st
‘𝑧) ∈
((1st ‘𝑧)[,)+∞)) |
39 | 35, 36, 37, 38 | syl3anc 1367 |
. . . . . . . . . 10
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) ∈
((1st ‘𝑧)[,)+∞)) |
40 | 39 | anim1i 616 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) ∈ ℝ ∧ (2nd
‘𝑧) ∈ ℝ)
→ ((1st ‘𝑧) ∈ ((1st ‘𝑧)[,)+∞) ∧
(2nd ‘𝑧)
∈ ℝ)) |
41 | 40 | anim2i 618 |
. . . . . . . 8
⊢ ((𝑧 ∈ (V × V) ∧
((1st ‘𝑧)
∈ ℝ ∧ (2nd ‘𝑧) ∈ ℝ)) → (𝑧 ∈ (V × V) ∧ ((1st
‘𝑧) ∈
((1st ‘𝑧)[,)+∞) ∧ (2nd
‘𝑧) ∈
ℝ))) |
42 | | elxp7 7723 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℝ ×
ℝ) ↔ (𝑧 ∈
(V × V) ∧ ((1st ‘𝑧) ∈ ℝ ∧ (2nd
‘𝑧) ∈
ℝ))) |
43 | | elxp7 7723 |
. . . . . . . 8
⊢ (𝑧 ∈ (((1st
‘𝑧)[,)+∞)
× ℝ) ↔ (𝑧
∈ (V × V) ∧ ((1st ‘𝑧) ∈ ((1st ‘𝑧)[,)+∞) ∧
(2nd ‘𝑧)
∈ ℝ))) |
44 | 41, 42, 43 | 3imtr4i 294 |
. . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
(((1st ‘𝑧)[,)+∞) ×
ℝ)) |
45 | | xp1st 7720 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (1st ‘𝑧) ∈ ℝ) |
46 | | oveq1 7162 |
. . . . . . . . . 10
⊢ (𝑒 = (1st ‘𝑧) → (𝑒[,)+∞) = ((1st ‘𝑧)[,)+∞)) |
47 | 46 | xpeq1d 5583 |
. . . . . . . . 9
⊢ (𝑒 = (1st ‘𝑧) → ((𝑒[,)+∞) × ℝ) =
(((1st ‘𝑧)[,)+∞) ×
ℝ)) |
48 | | ovex 7188 |
. . . . . . . . . 10
⊢
((1st ‘𝑧)[,)+∞) ∈ V |
49 | 48, 11 | xpex 7475 |
. . . . . . . . 9
⊢
(((1st ‘𝑧)[,)+∞) × ℝ) ∈
V |
50 | 47, 3, 49 | fvmpt 6767 |
. . . . . . . 8
⊢
((1st ‘𝑧) ∈ ℝ → ((𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧)) = (((1st ‘𝑧)[,)+∞) ×
ℝ)) |
51 | 45, 50 | syl 17 |
. . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → ((𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧)) = (((1st ‘𝑧)[,)+∞) ×
ℝ)) |
52 | 44, 51 | eleqtrrd 2916 |
. . . . . 6
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
((𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧))) |
53 | | elunirn2 30395 |
. . . . . 6
⊢ ((Fun
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∧ 𝑧 ∈
((𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧))) → 𝑧 ∈ ∪ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))) |
54 | 34, 52, 53 | sylancr 589 |
. . . . 5
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))) |
55 | 54 | ssriv 3970 |
. . . 4
⊢ (ℝ
× ℝ) ⊆ ∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ)) |
56 | | ssun3 4149 |
. . . 4
⊢ ((ℝ
× ℝ) ⊆ ∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) →
(ℝ × ℝ) ⊆ (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))))) |
57 | 55, 56 | ax-mp 5 |
. . 3
⊢ (ℝ
× ℝ) ⊆ (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) |
58 | | uniun 4860 |
. . 3
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) |
59 | 57, 58 | sseqtrri 4003 |
. 2
⊢ (ℝ
× ℝ) ⊆ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) |
60 | 33, 59 | eqssi 3982 |
1
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = (ℝ ×
ℝ) |