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 (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) = ℝ^{2}$

Proof

Step	Hyp	Ref	Expression
1		unissb	$⊢ ⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \subseteq ℝ^{2} \leftrightarrow \forall z \in (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) z \subseteq ℝ^{2}$
2		elun	$⊢ z \in (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \leftrightarrow (z \in ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \lor z \in ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
3		eqid	$⊢ (e \in ℝ ⟼ [e, +∞) \times ℝ) = (e \in ℝ ⟼ [e, +∞) \times ℝ)$
4	3	rnmptss	$⊢ \forall e \in ℝ [e, +∞) \times ℝ \in 𝒫 ℝ^{2} \to ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \subseteq 𝒫 ℝ^{2}$
5		pnfxr	$⊢ +∞ \in ℝ^{*}$
6		icossre	$⊢ (e \in ℝ \land +∞ \in ℝ^{*}) \to [e, +∞) \subseteq ℝ$
7	5 6	mpan2	$⊢ e \in ℝ \to [e, +∞) \subseteq ℝ$
8		xpss1	$⊢ [e, +∞) \subseteq ℝ \to [e, +∞) \times ℝ \subseteq ℝ^{2}$
9	7 8	syl	$⊢ e \in ℝ \to [e, +∞) \times ℝ \subseteq ℝ^{2}$
10		ovex	$⊢ [e, +∞) \in V$
11		reex	$⊢ ℝ \in V$
12	10 11	xpex	$⊢ [e, +∞) \times ℝ \in V$
13	12	elpw	$⊢ [e, +∞) \times ℝ \in 𝒫 ℝ^{2} \leftrightarrow [e, +∞) \times ℝ \subseteq ℝ^{2}$
14	9 13	sylibr	$⊢ e \in ℝ \to [e, +∞) \times ℝ \in 𝒫 ℝ^{2}$
15	4 14	mprg	$⊢ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \subseteq 𝒫 ℝ^{2}$
16	15	sseli	$⊢ z \in ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \to z \in 𝒫 ℝ^{2}$
17	16	elpwid	$⊢ z \in ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \to z \subseteq ℝ^{2}$
18		eqid	$⊢ (f \in ℝ ⟼ ℝ \times [f, +∞)) = (f \in ℝ ⟼ ℝ \times [f, +∞))$
19	18	rnmptss	$⊢ \forall f \in ℝ ℝ \times [f, +∞) \in 𝒫 ℝ^{2} \to ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \subseteq 𝒫 ℝ^{2}$
20		icossre	$⊢ (f \in ℝ \land +∞ \in ℝ^{*}) \to [f, +∞) \subseteq ℝ$
21	5 20	mpan2	$⊢ f \in ℝ \to [f, +∞) \subseteq ℝ$
22		xpss2	$⊢ [f, +∞) \subseteq ℝ \to ℝ \times [f, +∞) \subseteq ℝ^{2}$
23	21 22	syl	$⊢ f \in ℝ \to ℝ \times [f, +∞) \subseteq ℝ^{2}$
24		ovex	$⊢ [f, +∞) \in V$
25	11 24	xpex	$⊢ ℝ \times [f, +∞) \in V$
26	25	elpw	$⊢ ℝ \times [f, +∞) \in 𝒫 ℝ^{2} \leftrightarrow ℝ \times [f, +∞) \subseteq ℝ^{2}$
27	23 26	sylibr	$⊢ f \in ℝ \to ℝ \times [f, +∞) \in 𝒫 ℝ^{2}$
28	19 27	mprg	$⊢ ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \subseteq 𝒫 ℝ^{2}$
29	28	sseli	$⊢ z \in ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \to z \in 𝒫 ℝ^{2}$
30	29	elpwid	$⊢ z \in ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \to z \subseteq ℝ^{2}$
31	17 30	jaoi	$⊢ (z \in ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \lor z \in ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \to z \subseteq ℝ^{2}$
32	2 31	sylbi	$⊢ z \in (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \to z \subseteq ℝ^{2}$
33	1 32	mprgbir	$⊢ ⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \subseteq ℝ^{2}$
34		rexr	$⊢ 1^{st} (z) \in ℝ \to 1^{st} (z) \in ℝ^{*}$
35	5	a1i	$⊢ 1^{st} (z) \in ℝ \to +∞ \in ℝ^{*}$
36		ltpnf	$⊢ 1^{st} (z) \in ℝ \to 1^{st} (z) < +∞$
37		lbico1	$⊢ (1^{st} (z) \in ℝ^{} \land +∞ \in ℝ^{} \land 1^{st} (z) < +∞) \to 1^{st} (z) \in [1^{st} (z), +∞)$
38	34 35 36 37	syl3anc	$⊢ 1^{st} (z) \in ℝ \to 1^{st} (z) \in [1^{st} (z), +∞)$
39	38	anim1i	$⊢ (1^{st} (z) \in ℝ \land 2^{nd} (z) \in ℝ) \to (1^{st} (z) \in [1^{st} (z), +∞) \land 2^{nd} (z) \in ℝ)$
40	39	anim2i	$⊢ (z \in (V \times V) \land (1^{st} (z) \in ℝ \land 2^{nd} (z) \in ℝ)) \to (z \in (V \times V) \land (1^{st} (z) \in [1^{st} (z), +∞) \land 2^{nd} (z) \in ℝ))$
41		elxp7	$⊢ z \in ℝ^{2} \leftrightarrow (z \in (V \times V) \land (1^{st} (z) \in ℝ \land 2^{nd} (z) \in ℝ))$
42		elxp7	$⊢ z \in ([1^{st} (z), +∞) \times ℝ) \leftrightarrow (z \in (V \times V) \land (1^{st} (z) \in [1^{st} (z), +∞) \land 2^{nd} (z) \in ℝ))$
43	40 41 42	3imtr4i	$⊢ z \in ℝ^{2} \to z \in ([1^{st} (z), +∞) \times ℝ)$
44		xp1st	$⊢ z \in ℝ^{2} \to 1^{st} (z) \in ℝ$
45		oveq1	$⊢ e = 1^{st} (z) \to [e, +∞) = [1^{st} (z), +∞)$
46	45	xpeq1d	$⊢ e = 1^{st} (z) \to [e, +∞) \times ℝ = [1^{st} (z), +∞) \times ℝ$
47		ovex	$⊢ [1^{st} (z), +∞) \in V$
48	47 11	xpex	$⊢ [1^{st} (z), +∞) \times ℝ \in V$
49	46 3 48	fvmpt	$⊢ 1^{st} (z) \in ℝ \to (e \in ℝ ⟼ [e, +∞) \times ℝ) (1^{st} (z)) = [1^{st} (z), +∞) \times ℝ$
50	44 49	syl	$⊢ z \in ℝ^{2} \to (e \in ℝ ⟼ [e, +∞) \times ℝ) (1^{st} (z)) = [1^{st} (z), +∞) \times ℝ$
51	43 50	eleqtrrd	$⊢ z \in ℝ^{2} \to z \in (e \in ℝ ⟼ [e, +∞) \times ℝ) (1^{st} (z))$
52		elfvunirn	$⊢ z \in (e \in ℝ ⟼ [e, +∞) \times ℝ) (1^{st} (z)) \to z \in ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ)$
53	51 52	syl	$⊢ z \in ℝ^{2} \to z \in ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ)$
54	53	ssriv	$⊢ ℝ^{2} \subseteq ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ)$
55		ssun3	$⊢ ℝ^{2} \subseteq ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \to ℝ^{2} \subseteq ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ⋃ ran (f \in ℝ ⟼ ℝ \times [f, +∞))$
56	54 55	ax-mp	$⊢ ℝ^{2} \subseteq ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ⋃ ran (f \in ℝ ⟼ ℝ \times [f, +∞))$
57		uniun	$⊢ ⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) = ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ⋃ ran (f \in ℝ ⟼ ℝ \times [f, +∞))$
58	56 57	sseqtrri	$⊢ ℝ^{2} \subseteq ⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
59	33 58	eqssi	$⊢ ⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) = ℝ^{2}$

Metamath Proof Explorer

Theorem sxbrsigalem0

Proof