| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | unissb 4938 | . . 3
⊢ (∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ⊆ (ℝ ×
ℝ) ↔ ∀𝑧
∈ (ran (𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))𝑧 ⊆ (ℝ ×
ℝ)) | 
| 2 |  | elun 4152 | . . . 4
⊢ (𝑧 ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ↔ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∨ 𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))))) | 
| 3 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) =
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) | 
| 4 | 3 | rnmptss 7142 | . . . . . . . 8
⊢
(∀𝑒 ∈
ℝ ((𝑒[,)+∞)
× ℝ) ∈ 𝒫 (ℝ × ℝ) → ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
⊆ 𝒫 (ℝ × ℝ)) | 
| 5 |  | pnfxr 11316 | . . . . . . . . . . 11
⊢ +∞
∈ ℝ* | 
| 6 |  | icossre 13469 | . . . . . . . . . . 11
⊢ ((𝑒 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑒[,)+∞) ⊆
ℝ) | 
| 7 | 5, 6 | mpan2 691 | . . . . . . . . . 10
⊢ (𝑒 ∈ ℝ → (𝑒[,)+∞) ⊆
ℝ) | 
| 8 |  | xpss1 5703 | . . . . . . . . . 10
⊢ ((𝑒[,)+∞) ⊆ ℝ
→ ((𝑒[,)+∞)
× ℝ) ⊆ (ℝ × ℝ)) | 
| 9 | 7, 8 | syl 17 | . . . . . . . . 9
⊢ (𝑒 ∈ ℝ → ((𝑒[,)+∞) × ℝ)
⊆ (ℝ × ℝ)) | 
| 10 |  | ovex 7465 | . . . . . . . . . . 11
⊢ (𝑒[,)+∞) ∈
V | 
| 11 |  | reex 11247 | . . . . . . . . . . 11
⊢ ℝ
∈ V | 
| 12 | 10, 11 | xpex 7774 | . . . . . . . . . 10
⊢ ((𝑒[,)+∞) × ℝ)
∈ V | 
| 13 | 12 | elpw 4603 | . . . . . . . . 9
⊢ (((𝑒[,)+∞) × ℝ)
∈ 𝒫 (ℝ × ℝ) ↔ ((𝑒[,)+∞) × ℝ) ⊆
(ℝ × ℝ)) | 
| 14 | 9, 13 | sylibr 234 | . . . . . . . 8
⊢ (𝑒 ∈ ℝ → ((𝑒[,)+∞) × ℝ)
∈ 𝒫 (ℝ × ℝ)) | 
| 15 | 4, 14 | mprg 3066 | . . . . . . 7
⊢ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ⊆ 𝒫 (ℝ × ℝ) | 
| 16 | 15 | sseli 3978 | . . . . . 6
⊢ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) → 𝑧 ∈ 𝒫 (ℝ
× ℝ)) | 
| 17 | 16 | elpwid 4608 | . . . . 5
⊢ (𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) → 𝑧 ⊆ (ℝ ×
ℝ)) | 
| 18 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑓 ∈ ℝ ↦ (ℝ
× (𝑓[,)+∞))) =
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) | 
| 19 | 18 | rnmptss 7142 | . . . . . . . 8
⊢
(∀𝑓 ∈
ℝ (ℝ × (𝑓[,)+∞)) ∈ 𝒫 (ℝ
× ℝ) → ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) ⊆
𝒫 (ℝ × ℝ)) | 
| 20 |  | icossre 13469 | . . . . . . . . . . 11
⊢ ((𝑓 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑓[,)+∞) ⊆
ℝ) | 
| 21 | 5, 20 | mpan2 691 | . . . . . . . . . 10
⊢ (𝑓 ∈ ℝ → (𝑓[,)+∞) ⊆
ℝ) | 
| 22 |  | xpss2 5704 | . . . . . . . . . 10
⊢ ((𝑓[,)+∞) ⊆ ℝ
→ (ℝ × (𝑓[,)+∞)) ⊆ (ℝ ×
ℝ)) | 
| 23 | 21, 22 | syl 17 | . . . . . . . . 9
⊢ (𝑓 ∈ ℝ → (ℝ
× (𝑓[,)+∞))
⊆ (ℝ × ℝ)) | 
| 24 |  | ovex 7465 | . . . . . . . . . . 11
⊢ (𝑓[,)+∞) ∈
V | 
| 25 | 11, 24 | xpex 7774 | . . . . . . . . . 10
⊢ (ℝ
× (𝑓[,)+∞))
∈ V | 
| 26 | 25 | elpw 4603 | . . . . . . . . 9
⊢ ((ℝ
× (𝑓[,)+∞))
∈ 𝒫 (ℝ × ℝ) ↔ (ℝ × (𝑓[,)+∞)) ⊆ (ℝ
× ℝ)) | 
| 27 | 23, 26 | sylibr 234 | . . . . . . . 8
⊢ (𝑓 ∈ ℝ → (ℝ
× (𝑓[,)+∞))
∈ 𝒫 (ℝ × ℝ)) | 
| 28 | 19, 27 | mprg 3066 | . . . . . . 7
⊢ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) ⊆ 𝒫 (ℝ
× ℝ) | 
| 29 | 28 | sseli 3978 | . . . . . 6
⊢ (𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) →
𝑧 ∈ 𝒫 (ℝ
× ℝ)) | 
| 30 | 29 | elpwid 4608 | . . . . 5
⊢ (𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))) →
𝑧 ⊆ (ℝ ×
ℝ)) | 
| 31 | 17, 30 | jaoi 857 | . . . 4
⊢ ((𝑧 ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∨ 𝑧 ∈ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) →
𝑧 ⊆ (ℝ ×
ℝ)) | 
| 32 | 2, 31 | sylbi 217 | . . 3
⊢ (𝑧 ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) → 𝑧 ⊆ (ℝ ×
ℝ)) | 
| 33 | 1, 32 | mprgbir 3067 | . 2
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ⊆ (ℝ ×
ℝ) | 
| 34 |  | rexr 11308 | . . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) ∈
ℝ*) | 
| 35 | 5 | a1i 11 | . . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → +∞ ∈
ℝ*) | 
| 36 |  | ltpnf 13163 | . . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ ℝ → (1st
‘𝑧) <
+∞) | 
| 37 |  | lbico1 13442 | . . . . . . . . . . 11
⊢
(((1st ‘𝑧) ∈ ℝ* ∧ +∞
∈ ℝ* ∧ (1st ‘𝑧) < +∞) → (1st
‘𝑧) ∈
((1st ‘𝑧)[,)+∞)) | 
| 38 | 34, 35, 36, 37 | syl3anc 1372 | . . . . . . . . . 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 8050 | . . . . . . . 8
⊢ (𝑧 ∈ (ℝ ×
ℝ) ↔ (𝑧 ∈
(V × V) ∧ ((1st ‘𝑧) ∈ ℝ ∧ (2nd
‘𝑧) ∈
ℝ))) | 
| 42 |  | elxp7 8050 | . . . . . . . 8
⊢ (𝑧 ∈ (((1st
‘𝑧)[,)+∞)
× ℝ) ↔ (𝑧
∈ (V × V) ∧ ((1st ‘𝑧) ∈ ((1st ‘𝑧)[,)+∞) ∧
(2nd ‘𝑧)
∈ ℝ))) | 
| 43 | 40, 41, 42 | 3imtr4i 292 | . . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
(((1st ‘𝑧)[,)+∞) ×
ℝ)) | 
| 44 |  | xp1st 8047 | . . . . . . . 8
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (1st ‘𝑧) ∈ ℝ) | 
| 45 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑒 = (1st ‘𝑧) → (𝑒[,)+∞) = ((1st ‘𝑧)[,)+∞)) | 
| 46 | 45 | xpeq1d 5713 | . . . . . . . . 9
⊢ (𝑒 = (1st ‘𝑧) → ((𝑒[,)+∞) × ℝ) =
(((1st ‘𝑧)[,)+∞) ×
ℝ)) | 
| 47 |  | ovex 7465 | . . . . . . . . . 10
⊢
((1st ‘𝑧)[,)+∞) ∈ V | 
| 48 | 47, 11 | xpex 7774 | . . . . . . . . 9
⊢
(((1st ‘𝑧)[,)+∞) × ℝ) ∈
V | 
| 49 | 46, 3, 48 | fvmpt 7015 | . . . . . . . 8
⊢
((1st ‘𝑧) ∈ ℝ → ((𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧)) = (((1st ‘𝑧)[,)+∞) ×
ℝ)) | 
| 50 | 44, 49 | syl 17 | . . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → ((𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧)) = (((1st ‘𝑧)[,)+∞) ×
ℝ)) | 
| 51 | 43, 50 | eleqtrrd 2843 | . . . . . 6
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
((𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧))) | 
| 52 |  | elfvunirn 6937 | . . . . . 6
⊢ (𝑧 ∈ ((𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))‘(1st ‘𝑧)) → 𝑧 ∈ ∪ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))) | 
| 53 | 51, 52 | syl 17 | . . . . 5
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 ∈
∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ))) | 
| 54 | 53 | ssriv 3986 | . . . 4
⊢ (ℝ
× ℝ) ⊆ ∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) ×
ℝ)) | 
| 55 |  | ssun3 4179 | . . . 4
⊢ ((ℝ
× ℝ) ⊆ ∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) →
(ℝ × ℝ) ⊆ (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞))))) | 
| 56 | 54, 55 | ax-mp 5 | . . 3
⊢ (ℝ
× ℝ) ⊆ (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) | 
| 57 |  | uniun 4929 | . . 3
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = (∪ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ∪ ran (𝑓 ∈ ℝ ↦ (ℝ ×
(𝑓[,)+∞)))) | 
| 58 | 56, 57 | sseqtrri 4032 | . 2
⊢ (ℝ
× ℝ) ⊆ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) | 
| 59 | 33, 58 | eqssi 3999 | 1
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = (ℝ ×
ℝ) |