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		funmpt	$⊢ Fun (e \in ℝ ⟼ [e, +∞) \times ℝ)$
35		rexr	$⊢ 1^{st} (z) \in ℝ \to 1^{st} (z) \in ℝ^{*}$
36	5	a1i	$⊢ 1^{st} (z) \in ℝ \to +∞ \in ℝ^{*}$
37		ltpnf	$⊢ 1^{st} (z) \in ℝ \to 1^{st} (z) < +∞$
38		lbico1	$⊢ (1^{st} (z) \in ℝ^{} \land +∞ \in ℝ^{} \land 1^{st} (z) < +∞) \to 1^{st} (z) \in [1^{st} (z), +∞)$
39	35 36 37 38	syl3anc	$⊢ 1^{st} (z) \in ℝ \to 1^{st} (z) \in [1^{st} (z), +∞)$
40	39	anim1i	$⊢ (1^{st} (z) \in ℝ \land 2^{nd} (z) \in ℝ) \to (1^{st} (z) \in [1^{st} (z), +∞) \land 2^{nd} (z) \in ℝ)$
41	40	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 ℝ))$
42		elxp7	$⊢ z \in ℝ^{2} \leftrightarrow (z \in (V \times V) \land (1^{st} (z) \in ℝ \land 2^{nd} (z) \in ℝ))$
43		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 ℝ))$
44	41 42 43	3imtr4i	$⊢ z \in ℝ^{2} \to z \in ([1^{st} (z), +∞) \times ℝ)$
45		xp1st	$⊢ z \in ℝ^{2} \to 1^{st} (z) \in ℝ$
46		oveq1	$⊢ e = 1^{st} (z) \to [e, +∞) = [1^{st} (z), +∞)$
47	46	xpeq1d	$⊢ e = 1^{st} (z) \to [e, +∞) \times ℝ = [1^{st} (z), +∞) \times ℝ$
48		ovex	$⊢ [1^{st} (z), +∞) \in V$
49	48 11	xpex	$⊢ [1^{st} (z), +∞) \times ℝ \in V$
50	47 3 49	fvmpt	$⊢ 1^{st} (z) \in ℝ \to (e \in ℝ ⟼ [e, +∞) \times ℝ) (1^{st} (z)) = [1^{st} (z), +∞) \times ℝ$
51	45 50	syl	$⊢ z \in ℝ^{2} \to (e \in ℝ ⟼ [e, +∞) \times ℝ) (1^{st} (z)) = [1^{st} (z), +∞) \times ℝ$
52	44 51	eleqtrrd	$⊢ z \in ℝ^{2} \to z \in (e \in ℝ ⟼ [e, +∞) \times ℝ) (1^{st} (z))$
53		elunirn2	$⊢ (Fun (e \in ℝ ⟼ [e, +∞) \times ℝ) \land z \in (e \in ℝ ⟼ [e, +∞) \times ℝ) (1^{st} (z))) \to z \in ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ)$
54	34 52 53	sylancr	$⊢ z \in ℝ^{2} \to z \in ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ)$
55	54	ssriv	$⊢ ℝ^{2} \subseteq ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ)$
56		ssun3	$⊢ ℝ^{2} \subseteq ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \to ℝ^{2} \subseteq ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ⋃ ran (f \in ℝ ⟼ ℝ \times [f, +∞))$
57	55 56	ax-mp	$⊢ ℝ^{2} \subseteq ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ⋃ ran (f \in ℝ ⟼ ℝ \times [f, +∞))$
58		uniun	$⊢ ⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) = ⋃ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ⋃ ran (f \in ℝ ⟼ ℝ \times [f, +∞))$
59	57 58	sseqtrri	$⊢ ℝ^{2} \subseteq ⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
60	33 59	eqssi	$⊢ ⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) = ℝ^{2}$

Metamath Proof Explorer

Theorem sxbrsigalem0

Proof