Step | Hyp | Ref
| Expression |
1 | | unissb 4900 |
. . 3
⊢ (∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ⊆ (ℝ ×
ℝ) ↔ ∀𝑧
∈ (ran (𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))𝑧 ⊆ (ℝ ×
ℝ)) |
2 | | elun 4108 |
. . . 4
⊢ (𝑧 ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ↔ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∨ 𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))))) |
3 | | eqid 2736 |
. . . . . . . . 9
⊢ (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) =
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) |
4 | 3 | rnmptss 7070 |
. . . . . . . 8
⊢
(∀𝑒 ∈
ℝ ((𝑒[,)+∞)
× ℝ) ∈ 𝒫 (ℝ × ℝ) → ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
⊆ 𝒫 (ℝ × ℝ)) |
5 | | pnfxr 11209 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
6 | | icossre 13345 |
. . . . . . . . . . 11
⊢ ((𝑒 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑒[,)+∞) ⊆
ℝ) |
7 | 5, 6 | mpan2 689 |
. . . . . . . . . 10
⊢ (𝑒 ∈ ℝ → (𝑒[,)+∞) ⊆
ℝ) |
8 | | xpss1 5652 |
. . . . . . . . . 10
⊢ ((𝑒[,)+∞) ⊆ ℝ
→ ((𝑒[,)+∞)
× ℝ) ⊆ (ℝ × ℝ)) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝑒 ∈ ℝ → ((𝑒[,)+∞) × ℝ)
⊆ (ℝ × ℝ)) |
10 | | ovex 7390 |
. . . . . . . . . . 11
⊢ (𝑒[,)+∞) ∈
V |
11 | | reex 11142 |
. . . . . . . . . . 11
⊢ ℝ
∈ V |
12 | 10, 11 | xpex 7687 |
. . . . . . . . . 10
⊢ ((𝑒[,)+∞) × ℝ)
∈ V |
13 | 12 | elpw 4564 |
. . . . . . . . 9
⊢ (((𝑒[,)+∞) × ℝ)
∈ 𝒫 (ℝ × ℝ) ↔ ((𝑒[,)+∞) × ℝ) ⊆
(ℝ × ℝ)) |
14 | 9, 13 | sylibr 233 |
. . . . . . . 8
⊢ (𝑒 ∈ ℝ → ((𝑒[,)+∞) × ℝ)
∈ 𝒫 (ℝ × ℝ)) |
15 | 4, 14 | mprg 3070 |
. . . . . . 7
⊢ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ⊆ 𝒫 (ℝ × ℝ) |
16 | 15 | sseli 3940 |
. . . . . 6
⊢ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) → 𝑧 ∈ 𝒫 (ℝ
× ℝ)) |
17 | 16 | elpwid 4569 |
. . . . 5
⊢ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) → 𝑧 ⊆ (ℝ ×
ℝ)) |
18 | | eqid 2736 |
. . . . . . . . 9
⊢ (𝑓 ∈ ℝ ↦ (ℝ
× (𝑓[,)+∞))) =
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) |
19 | 18 | rnmptss 7070 |
. . . . . . . 8
⊢
(∀𝑓 ∈
ℝ (ℝ × (𝑓[,)+∞)) ∈ 𝒫 (ℝ
× ℝ) → ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) ⊆
𝒫 (ℝ × ℝ)) |
20 | | icossre 13345 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑓[,)+∞) ⊆
ℝ) |
21 | 5, 20 | mpan2 689 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ℝ → (𝑓[,)+∞) ⊆
ℝ) |
22 | | xpss2 5653 |
. . . . . . . . . 10
⊢ ((𝑓[,)+∞) ⊆ ℝ
→ (ℝ × (𝑓[,)+∞)) ⊆ (ℝ ×
ℝ)) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝑓 ∈ ℝ → (ℝ
× (𝑓[,)+∞))
⊆ (ℝ × ℝ)) |
24 | | ovex 7390 |
. . . . . . . . . . 11
⊢ (𝑓[,)+∞) ∈
V |
25 | 11, 24 | xpex 7687 |
. . . . . . . . . 10
⊢ (ℝ
× (𝑓[,)+∞))
∈ V |
26 | 25 | elpw 4564 |
. . . . . . . . 9
⊢ ((ℝ
× (𝑓[,)+∞))
∈ 𝒫 (ℝ × ℝ) ↔ (ℝ × (𝑓[,)+∞)) ⊆ (ℝ
× ℝ)) |
27 | 23, 26 | sylibr 233 |
. . . . . . . 8
⊢ (𝑓 ∈ ℝ → (ℝ
× (𝑓[,)+∞))
∈ 𝒫 (ℝ × ℝ)) |
28 | 19, 27 | mprg 3070 |
. . . . . . 7
⊢ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) ⊆ 𝒫 (ℝ
× ℝ) |
29 | 28 | sseli 3940 |
. . . . . 6
⊢ (𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) →
𝑧 ∈ 𝒫 (ℝ
× ℝ)) |
30 | 29 | elpwid 4569 |
. . . . 5
⊢ (𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) →
𝑧 ⊆ (ℝ ×
ℝ)) |
31 | 17, 30 | jaoi 855 |
. . . 4
⊢ ((𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∨ 𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) →
𝑧 ⊆ (ℝ ×
ℝ)) |
32 | 2, 31 | sylbi 216 |
. . 3
⊢ (𝑧 ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) → 𝑧 ⊆ (ℝ ×
ℝ)) |
33 | 1, 32 | mprgbir 3071 |
. 2
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ⊆ (ℝ ×
ℝ) |
34 | | rexr 11201 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) ∈
ℝ*) |
35 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → +∞ ∈
ℝ*) |
36 | | ltpnf 13041 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) <
+∞) |
37 | | lbico1 13318 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑧) ∈ ℝ* ∧ +∞
∈ ℝ* ∧ (1st ‘𝑧) < +∞) → (1st
‘𝑧) ∈
((1st ‘𝑧)[,)+∞)) |
38 | 34, 35, 36, 37 | syl3anc 1371 |
. . . . . . . . . 10
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) ∈
((1st ‘𝑧)[,)+∞)) |
39 | 38 | anim1i 615 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) ∈ ℝ ∧ (2nd
‘𝑧) ∈ ℝ)
→ ((1st ‘𝑧) ∈ ((1st ‘𝑧)[,)+∞) ∧
(2nd ‘𝑧)
∈ ℝ)) |
40 | 39 | anim2i 617 |
. . . . . . . 8
⊢ ((𝑧 ∈ (V × V) ∧
((1st ‘𝑧)
∈ ℝ ∧ (2nd ‘𝑧) ∈ ℝ)) → (𝑧 ∈ (V × V) ∧ ((1st
‘𝑧) ∈
((1st ‘𝑧)[,)+∞) ∧ (2nd
‘𝑧) ∈
ℝ))) |
41 | | elxp7 7956 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℝ ×
ℝ) ↔ (𝑧 ∈
(V × V) ∧ ((1st ‘𝑧) ∈ ℝ ∧ (2nd
‘𝑧) ∈
ℝ))) |
42 | | elxp7 7956 |
. . . . . . . 8
⊢ (𝑧 ∈ (((1st
‘𝑧)[,)+∞)
× ℝ) ↔ (𝑧
∈ (V × V) ∧ ((1st ‘𝑧) ∈ ((1st ‘𝑧)[,)+∞) ∧
(2nd ‘𝑧)
∈ ℝ))) |
43 | 40, 41, 42 | 3imtr4i 291 |
. . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
(((1st ‘𝑧)[,)+∞) ×
ℝ)) |
44 | | xp1st 7953 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (1st ‘𝑧) ∈ ℝ) |
45 | | oveq1 7364 |
. . . . . . . . . 10
⊢ (𝑒 = (1st ‘𝑧) → (𝑒[,)+∞) = ((1st ‘𝑧)[,)+∞)) |
46 | 45 | xpeq1d 5662 |
. . . . . . . . 9
⊢ (𝑒 = (1st ‘𝑧) → ((𝑒[,)+∞) × ℝ) =
(((1st ‘𝑧)[,)+∞) ×
ℝ)) |
47 | | ovex 7390 |
. . . . . . . . . 10
⊢
((1st ‘𝑧)[,)+∞) ∈ V |
48 | 47, 11 | xpex 7687 |
. . . . . . . . 9
⊢
(((1st ‘𝑧)[,)+∞) × ℝ) ∈
V |
49 | 46, 3, 48 | fvmpt 6948 |
. . . . . . . 8
⊢
((1st ‘𝑧) ∈ ℝ → ((𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧)) = (((1st ‘𝑧)[,)+∞) ×
ℝ)) |
50 | 44, 49 | syl 17 |
. . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → ((𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧)) = (((1st ‘𝑧)[,)+∞) ×
ℝ)) |
51 | 43, 50 | eleqtrrd 2841 |
. . . . . 6
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
((𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧))) |
52 | | elfvunirn 6874 |
. . . . . 6
⊢ (𝑧 ∈ ((𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧)) → 𝑧 ∈ ∪ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))) |
53 | 51, 52 | syl 17 |
. . . . 5
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))) |
54 | 53 | ssriv 3948 |
. . . 4
⊢ (ℝ
× ℝ) ⊆ ∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ)) |
55 | | ssun3 4134 |
. . . 4
⊢ ((ℝ
× ℝ) ⊆ ∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) →
(ℝ × ℝ) ⊆ (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))))) |
56 | 54, 55 | ax-mp 5 |
. . 3
⊢ (ℝ
× ℝ) ⊆ (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) |
57 | | uniun 4891 |
. . 3
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) |
58 | 56, 57 | sseqtrri 3981 |
. 2
⊢ (ℝ
× ℝ) ⊆ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) |
59 | 33, 58 | eqssi 3960 |
1
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = (ℝ ×
ℝ) |