Step | Hyp | Ref
| Expression |
1 | | unissb 4830 |
. . 3
⊢ (∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ⊆ (ℝ ×
ℝ) ↔ ∀𝑧
∈ (ran (𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))𝑧 ⊆ (ℝ ×
ℝ)) |
2 | | elun 4039 |
. . . 4
⊢ (𝑧 ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ↔ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∨ 𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))))) |
3 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) =
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) |
4 | 3 | rnmptss 6896 |
. . . . . . . 8
⊢
(∀𝑒 ∈
ℝ ((𝑒[,)+∞)
× ℝ) ∈ 𝒫 (ℝ × ℝ) → ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
⊆ 𝒫 (ℝ × ℝ)) |
5 | | pnfxr 10773 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
6 | | icossre 12902 |
. . . . . . . . . . 11
⊢ ((𝑒 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑒[,)+∞) ⊆
ℝ) |
7 | 5, 6 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑒 ∈ ℝ → (𝑒[,)+∞) ⊆
ℝ) |
8 | | xpss1 5544 |
. . . . . . . . . 10
⊢ ((𝑒[,)+∞) ⊆ ℝ
→ ((𝑒[,)+∞)
× ℝ) ⊆ (ℝ × ℝ)) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝑒 ∈ ℝ → ((𝑒[,)+∞) × ℝ)
⊆ (ℝ × ℝ)) |
10 | | ovex 7203 |
. . . . . . . . . . 11
⊢ (𝑒[,)+∞) ∈
V |
11 | | reex 10706 |
. . . . . . . . . . 11
⊢ ℝ
∈ V |
12 | 10, 11 | xpex 7494 |
. . . . . . . . . 10
⊢ ((𝑒[,)+∞) × ℝ)
∈ V |
13 | 12 | elpw 4492 |
. . . . . . . . 9
⊢ (((𝑒[,)+∞) × ℝ)
∈ 𝒫 (ℝ × ℝ) ↔ ((𝑒[,)+∞) × ℝ) ⊆
(ℝ × ℝ)) |
14 | 9, 13 | sylibr 237 |
. . . . . . . 8
⊢ (𝑒 ∈ ℝ → ((𝑒[,)+∞) × ℝ)
∈ 𝒫 (ℝ × ℝ)) |
15 | 4, 14 | mprg 3067 |
. . . . . . 7
⊢ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ⊆ 𝒫 (ℝ × ℝ) |
16 | 15 | sseli 3873 |
. . . . . 6
⊢ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) → 𝑧 ∈ 𝒫 (ℝ
× ℝ)) |
17 | 16 | elpwid 4499 |
. . . . 5
⊢ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) → 𝑧 ⊆ (ℝ ×
ℝ)) |
18 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑓 ∈ ℝ ↦ (ℝ
× (𝑓[,)+∞))) =
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) |
19 | 18 | rnmptss 6896 |
. . . . . . . 8
⊢
(∀𝑓 ∈
ℝ (ℝ × (𝑓[,)+∞)) ∈ 𝒫 (ℝ
× ℝ) → ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) ⊆
𝒫 (ℝ × ℝ)) |
20 | | icossre 12902 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑓[,)+∞) ⊆
ℝ) |
21 | 5, 20 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ℝ → (𝑓[,)+∞) ⊆
ℝ) |
22 | | xpss2 5545 |
. . . . . . . . . 10
⊢ ((𝑓[,)+∞) ⊆ ℝ
→ (ℝ × (𝑓[,)+∞)) ⊆ (ℝ ×
ℝ)) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝑓 ∈ ℝ → (ℝ
× (𝑓[,)+∞))
⊆ (ℝ × ℝ)) |
24 | | ovex 7203 |
. . . . . . . . . . 11
⊢ (𝑓[,)+∞) ∈
V |
25 | 11, 24 | xpex 7494 |
. . . . . . . . . 10
⊢ (ℝ
× (𝑓[,)+∞))
∈ V |
26 | 25 | elpw 4492 |
. . . . . . . . 9
⊢ ((ℝ
× (𝑓[,)+∞))
∈ 𝒫 (ℝ × ℝ) ↔ (ℝ × (𝑓[,)+∞)) ⊆ (ℝ
× ℝ)) |
27 | 23, 26 | sylibr 237 |
. . . . . . . 8
⊢ (𝑓 ∈ ℝ → (ℝ
× (𝑓[,)+∞))
∈ 𝒫 (ℝ × ℝ)) |
28 | 19, 27 | mprg 3067 |
. . . . . . 7
⊢ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) ⊆ 𝒫 (ℝ
× ℝ) |
29 | 28 | sseli 3873 |
. . . . . 6
⊢ (𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) →
𝑧 ∈ 𝒫 (ℝ
× ℝ)) |
30 | 29 | elpwid 4499 |
. . . . 5
⊢ (𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) →
𝑧 ⊆ (ℝ ×
ℝ)) |
31 | 17, 30 | jaoi 856 |
. . . 4
⊢ ((𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∨ 𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) →
𝑧 ⊆ (ℝ ×
ℝ)) |
32 | 2, 31 | sylbi 220 |
. . 3
⊢ (𝑧 ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) → 𝑧 ⊆ (ℝ ×
ℝ)) |
33 | 1, 32 | mprgbir 3068 |
. 2
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ⊆ (ℝ ×
ℝ) |
34 | | funmpt 6377 |
. . . . . 6
⊢ Fun
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) |
35 | | rexr 10765 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) ∈
ℝ*) |
36 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → +∞ ∈
ℝ*) |
37 | | ltpnf 12598 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) <
+∞) |
38 | | lbico1 12875 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑧) ∈ ℝ* ∧ +∞
∈ ℝ* ∧ (1st ‘𝑧) < +∞) → (1st
‘𝑧) ∈
((1st ‘𝑧)[,)+∞)) |
39 | 35, 36, 37, 38 | syl3anc 1372 |
. . . . . . . . . 10
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) ∈
((1st ‘𝑧)[,)+∞)) |
40 | 39 | anim1i 618 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) ∈ ℝ ∧ (2nd
‘𝑧) ∈ ℝ)
→ ((1st ‘𝑧) ∈ ((1st ‘𝑧)[,)+∞) ∧
(2nd ‘𝑧)
∈ ℝ)) |
41 | 40 | anim2i 620 |
. . . . . . . 8
⊢ ((𝑧 ∈ (V × V) ∧
((1st ‘𝑧)
∈ ℝ ∧ (2nd ‘𝑧) ∈ ℝ)) → (𝑧 ∈ (V × V) ∧ ((1st
‘𝑧) ∈
((1st ‘𝑧)[,)+∞) ∧ (2nd
‘𝑧) ∈
ℝ))) |
42 | | elxp7 7749 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℝ ×
ℝ) ↔ (𝑧 ∈
(V × V) ∧ ((1st ‘𝑧) ∈ ℝ ∧ (2nd
‘𝑧) ∈
ℝ))) |
43 | | elxp7 7749 |
. . . . . . . 8
⊢ (𝑧 ∈ (((1st
‘𝑧)[,)+∞)
× ℝ) ↔ (𝑧
∈ (V × V) ∧ ((1st ‘𝑧) ∈ ((1st ‘𝑧)[,)+∞) ∧
(2nd ‘𝑧)
∈ ℝ))) |
44 | 41, 42, 43 | 3imtr4i 295 |
. . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
(((1st ‘𝑧)[,)+∞) ×
ℝ)) |
45 | | xp1st 7746 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (1st ‘𝑧) ∈ ℝ) |
46 | | oveq1 7177 |
. . . . . . . . . 10
⊢ (𝑒 = (1st ‘𝑧) → (𝑒[,)+∞) = ((1st ‘𝑧)[,)+∞)) |
47 | 46 | xpeq1d 5554 |
. . . . . . . . 9
⊢ (𝑒 = (1st ‘𝑧) → ((𝑒[,)+∞) × ℝ) =
(((1st ‘𝑧)[,)+∞) ×
ℝ)) |
48 | | ovex 7203 |
. . . . . . . . . 10
⊢
((1st ‘𝑧)[,)+∞) ∈ V |
49 | 48, 11 | xpex 7494 |
. . . . . . . . 9
⊢
(((1st ‘𝑧)[,)+∞) × ℝ) ∈
V |
50 | 47, 3, 49 | fvmpt 6775 |
. . . . . . . 8
⊢
((1st ‘𝑧) ∈ ℝ → ((𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧)) = (((1st ‘𝑧)[,)+∞) ×
ℝ)) |
51 | 45, 50 | syl 17 |
. . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → ((𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧)) = (((1st ‘𝑧)[,)+∞) ×
ℝ)) |
52 | 44, 51 | eleqtrrd 2836 |
. . . . . 6
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
((𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧))) |
53 | | elunirn2 30563 |
. . . . . 6
⊢ ((Fun
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∧ 𝑧 ∈
((𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧))) → 𝑧 ∈ ∪ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))) |
54 | 34, 52, 53 | sylancr 590 |
. . . . 5
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))) |
55 | 54 | ssriv 3881 |
. . . 4
⊢ (ℝ
× ℝ) ⊆ ∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ)) |
56 | | ssun3 4064 |
. . . 4
⊢ ((ℝ
× ℝ) ⊆ ∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) →
(ℝ × ℝ) ⊆ (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))))) |
57 | 55, 56 | ax-mp 5 |
. . 3
⊢ (ℝ
× ℝ) ⊆ (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) |
58 | | uniun 4821 |
. . 3
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) |
59 | 57, 58 | sseqtrri 3914 |
. 2
⊢ (ℝ
× ℝ) ⊆ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) |
60 | 33, 59 | eqssi 3893 |
1
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = (ℝ ×
ℝ) |