Theorem sxbrsigalem0

Description: The closed half-spaces of ( RR X. RR ) cover ( RR X. RR ) . (Contributed by Thierry Arnoux, 11-Oct-2017)

	Ref	Expression
Assertion	sxbrsigalem0	⊢ ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ( ℝ × ℝ )

Proof

Step	Hyp	Ref	Expression
1		unissb	⊢ ( ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ⊆ ( ℝ × ℝ ) ↔ ∀ 𝑧 ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) 𝑧 ⊆ ( ℝ × ℝ ) )
2		elun	⊢ ( 𝑧 ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ↔ ( 𝑧 ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∨ 𝑧 ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) )
3		eqid	⊢ ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) = ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) )
4	3	rnmptss	⊢ ( ∀ 𝑒 ∈ ℝ ( ( 𝑒 [,) +∞ ) × ℝ ) ∈ 𝒫 ( ℝ × ℝ ) → ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ⊆ 𝒫 ( ℝ × ℝ ) )
5		pnfxr	⊢ +∞ ∈ ℝ*
6		icossre	⊢ ( ( 𝑒 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 𝑒 [,) +∞ ) ⊆ ℝ )
7	5 6	mpan2	⊢ ( 𝑒 ∈ ℝ → ( 𝑒 [,) +∞ ) ⊆ ℝ )
8		xpss1	⊢ ( ( 𝑒 [,) +∞ ) ⊆ ℝ → ( ( 𝑒 [,) +∞ ) × ℝ ) ⊆ ( ℝ × ℝ ) )
9	7 8	syl	⊢ ( 𝑒 ∈ ℝ → ( ( 𝑒 [,) +∞ ) × ℝ ) ⊆ ( ℝ × ℝ ) )
10		ovex	⊢ ( 𝑒 [,) +∞ ) ∈ V
11		reex	⊢ ℝ ∈ V
12	10 11	xpex	⊢ ( ( 𝑒 [,) +∞ ) × ℝ ) ∈ V
13	12	elpw	⊢ ( ( ( 𝑒 [,) +∞ ) × ℝ ) ∈ 𝒫 ( ℝ × ℝ ) ↔ ( ( 𝑒 [,) +∞ ) × ℝ ) ⊆ ( ℝ × ℝ ) )
14	9 13	sylibr	⊢ ( 𝑒 ∈ ℝ → ( ( 𝑒 [,) +∞ ) × ℝ ) ∈ 𝒫 ( ℝ × ℝ ) )
15	4 14	mprg	⊢ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ⊆ 𝒫 ( ℝ × ℝ )
16	15	sseli	⊢ ( 𝑧 ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) → 𝑧 ∈ 𝒫 ( ℝ × ℝ ) )
17	16	elpwid	⊢ ( 𝑧 ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) → 𝑧 ⊆ ( ℝ × ℝ ) )
18		eqid	⊢ ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) = ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) )
19	18	rnmptss	⊢ ( ∀ 𝑓 ∈ ℝ ( ℝ × ( 𝑓 [,) +∞ ) ) ∈ 𝒫 ( ℝ × ℝ ) → ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ⊆ 𝒫 ( ℝ × ℝ ) )
20		icossre	⊢ ( ( 𝑓 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 𝑓 [,) +∞ ) ⊆ ℝ )
21	5 20	mpan2	⊢ ( 𝑓 ∈ ℝ → ( 𝑓 [,) +∞ ) ⊆ ℝ )
22		xpss2	⊢ ( ( 𝑓 [,) +∞ ) ⊆ ℝ → ( ℝ × ( 𝑓 [,) +∞ ) ) ⊆ ( ℝ × ℝ ) )
23	21 22	syl	⊢ ( 𝑓 ∈ ℝ → ( ℝ × ( 𝑓 [,) +∞ ) ) ⊆ ( ℝ × ℝ ) )
24		ovex	⊢ ( 𝑓 [,) +∞ ) ∈ V
25	11 24	xpex	⊢ ( ℝ × ( 𝑓 [,) +∞ ) ) ∈ V
26	25	elpw	⊢ ( ( ℝ × ( 𝑓 [,) +∞ ) ) ∈ 𝒫 ( ℝ × ℝ ) ↔ ( ℝ × ( 𝑓 [,) +∞ ) ) ⊆ ( ℝ × ℝ ) )
27	23 26	sylibr	⊢ ( 𝑓 ∈ ℝ → ( ℝ × ( 𝑓 [,) +∞ ) ) ∈ 𝒫 ( ℝ × ℝ ) )
28	19 27	mprg	⊢ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ⊆ 𝒫 ( ℝ × ℝ )
29	28	sseli	⊢ ( 𝑧 ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) → 𝑧 ∈ 𝒫 ( ℝ × ℝ ) )
30	29	elpwid	⊢ ( 𝑧 ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) → 𝑧 ⊆ ( ℝ × ℝ ) )
31	17 30	jaoi	⊢ ( ( 𝑧 ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∨ 𝑧 ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) → 𝑧 ⊆ ( ℝ × ℝ ) )
32	2 31	sylbi	⊢ ( 𝑧 ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) → 𝑧 ⊆ ( ℝ × ℝ ) )
33	1 32	mprgbir	⊢ ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ⊆ ( ℝ × ℝ )
34		funmpt	⊢ Fun ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) )
35		rexr	⊢ ( ( 1st ‘ 𝑧 ) ∈ ℝ → ( 1st ‘ 𝑧 ) ∈ ℝ* )
36	5	a1i	⊢ ( ( 1st ‘ 𝑧 ) ∈ ℝ → +∞ ∈ ℝ* )
37		ltpnf	⊢ ( ( 1st ‘ 𝑧 ) ∈ ℝ → ( 1st ‘ 𝑧 ) < +∞ )
38		lbico1	⊢ ( ( ( 1st ‘ 𝑧 ) ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 1st ‘ 𝑧 ) < +∞ ) → ( 1st ‘ 𝑧 ) ∈ ( ( 1st ‘ 𝑧 ) [,) +∞ ) )
39	35 36 37 38	syl3anc	⊢ ( ( 1st ‘ 𝑧 ) ∈ ℝ → ( 1st ‘ 𝑧 ) ∈ ( ( 1st ‘ 𝑧 ) [,) +∞ ) )
40	39	anim1i	⊢ ( ( ( 1st ‘ 𝑧 ) ∈ ℝ ∧ ( 2nd ‘ 𝑧 ) ∈ ℝ ) → ( ( 1st ‘ 𝑧 ) ∈ ( ( 1st ‘ 𝑧 ) [,) +∞ ) ∧ ( 2nd ‘ 𝑧 ) ∈ ℝ ) )
41	40	anim2i	⊢ ( ( 𝑧 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑧 ) ∈ ℝ ∧ ( 2nd ‘ 𝑧 ) ∈ ℝ ) ) → ( 𝑧 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑧 ) ∈ ( ( 1st ‘ 𝑧 ) [,) +∞ ) ∧ ( 2nd ‘ 𝑧 ) ∈ ℝ ) ) )
42		elxp7	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) ↔ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑧 ) ∈ ℝ ∧ ( 2nd ‘ 𝑧 ) ∈ ℝ ) ) )
43		elxp7	⊢ ( 𝑧 ∈ ( ( ( 1st ‘ 𝑧 ) [,) +∞ ) × ℝ ) ↔ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑧 ) ∈ ( ( 1st ‘ 𝑧 ) [,) +∞ ) ∧ ( 2nd ‘ 𝑧 ) ∈ ℝ ) ) )
44	41 42 43	3imtr4i	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → 𝑧 ∈ ( ( ( 1st ‘ 𝑧 ) [,) +∞ ) × ℝ ) )
45		xp1st	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 1st ‘ 𝑧 ) ∈ ℝ )
46		oveq1	⊢ ( 𝑒 = ( 1st ‘ 𝑧 ) → ( 𝑒 [,) +∞ ) = ( ( 1st ‘ 𝑧 ) [,) +∞ ) )
47	46	xpeq1d	⊢ ( 𝑒 = ( 1st ‘ 𝑧 ) → ( ( 𝑒 [,) +∞ ) × ℝ ) = ( ( ( 1st ‘ 𝑧 ) [,) +∞ ) × ℝ ) )
48		ovex	⊢ ( ( 1st ‘ 𝑧 ) [,) +∞ ) ∈ V
49	48 11	xpex	⊢ ( ( ( 1st ‘ 𝑧 ) [,) +∞ ) × ℝ ) ∈ V
50	47 3 49	fvmpt	⊢ ( ( 1st ‘ 𝑧 ) ∈ ℝ → ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ ( 1st ‘ 𝑧 ) ) = ( ( ( 1st ‘ 𝑧 ) [,) +∞ ) × ℝ ) )
51	45 50	syl	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ ( 1st ‘ 𝑧 ) ) = ( ( ( 1st ‘ 𝑧 ) [,) +∞ ) × ℝ ) )
52	44 51	eleqtrrd	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → 𝑧 ∈ ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ ( 1st ‘ 𝑧 ) ) )
53		elunirn2	⊢ ( ( Fun ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∧ 𝑧 ∈ ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ ( 1st ‘ 𝑧 ) ) ) → 𝑧 ∈ ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) )
54	34 52 53	sylancr	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → 𝑧 ∈ ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) )
55	54	ssriv	⊢ ( ℝ × ℝ ) ⊆ ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) )
56		ssun3	⊢ ( ( ℝ × ℝ ) ⊆ ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) → ( ℝ × ℝ ) ⊆ ( ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) )
57	55 56	ax-mp	⊢ ( ℝ × ℝ ) ⊆ ( ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) )
58		uniun	⊢ ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ( ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) )
59	57 58	sseqtrri	⊢ ( ℝ × ℝ ) ⊆ ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) )
60	33 59	eqssi	⊢ ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ( ℝ × ℝ )