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		rexr	⊢ ( ( 1^st ‘ 𝑧 ) ∈ ℝ → ( 1^st ‘ 𝑧 ) ∈ ℝ^* )
35	5	a1i	⊢ ( ( 1^st ‘ 𝑧 ) ∈ ℝ → +∞ ∈ ℝ^* )
36		ltpnf	⊢ ( ( 1^st ‘ 𝑧 ) ∈ ℝ → ( 1^st ‘ 𝑧 ) < +∞ )
37		lbico1	⊢ ( ( ( 1^st ‘ 𝑧 ) ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ ( 1^st ‘ 𝑧 ) < +∞ ) → ( 1^st ‘ 𝑧 ) ∈ ( ( 1^st ‘ 𝑧 ) [,) +∞ ) )
38	34 35 36 37	syl3anc	⊢ ( ( 1^st ‘ 𝑧 ) ∈ ℝ → ( 1^st ‘ 𝑧 ) ∈ ( ( 1^st ‘ 𝑧 ) [,) +∞ ) )
39	38	anim1i	⊢ ( ( ( 1^st ‘ 𝑧 ) ∈ ℝ ∧ ( 2^nd ‘ 𝑧 ) ∈ ℝ ) → ( ( 1^st ‘ 𝑧 ) ∈ ( ( 1^st ‘ 𝑧 ) [,) +∞ ) ∧ ( 2^nd ‘ 𝑧 ) ∈ ℝ ) )
40	39	anim2i	⊢ ( ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ ℝ ∧ ( 2^nd ‘ 𝑧 ) ∈ ℝ ) ) → ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ ( ( 1^st ‘ 𝑧 ) [,) +∞ ) ∧ ( 2^nd ‘ 𝑧 ) ∈ ℝ ) ) )
41		elxp7	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) ↔ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ ℝ ∧ ( 2^nd ‘ 𝑧 ) ∈ ℝ ) ) )
42		elxp7	⊢ ( 𝑧 ∈ ( ( ( 1^st ‘ 𝑧 ) [,) +∞ ) × ℝ ) ↔ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑧 ) ∈ ( ( 1^st ‘ 𝑧 ) [,) +∞ ) ∧ ( 2^nd ‘ 𝑧 ) ∈ ℝ ) ) )
43	40 41 42	3imtr4i	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → 𝑧 ∈ ( ( ( 1^st ‘ 𝑧 ) [,) +∞ ) × ℝ ) )
44		xp1st	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 1^st ‘ 𝑧 ) ∈ ℝ )
45		oveq1	⊢ ( 𝑒 = ( 1^st ‘ 𝑧 ) → ( 𝑒 [,) +∞ ) = ( ( 1^st ‘ 𝑧 ) [,) +∞ ) )
46	45	xpeq1d	⊢ ( 𝑒 = ( 1^st ‘ 𝑧 ) → ( ( 𝑒 [,) +∞ ) × ℝ ) = ( ( ( 1^st ‘ 𝑧 ) [,) +∞ ) × ℝ ) )
47		ovex	⊢ ( ( 1^st ‘ 𝑧 ) [,) +∞ ) ∈ V
48	47 11	xpex	⊢ ( ( ( 1^st ‘ 𝑧 ) [,) +∞ ) × ℝ ) ∈ V
49	46 3 48	fvmpt	⊢ ( ( 1^st ‘ 𝑧 ) ∈ ℝ → ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ ( 1^st ‘ 𝑧 ) ) = ( ( ( 1^st ‘ 𝑧 ) [,) +∞ ) × ℝ ) )
50	44 49	syl	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ ( 1^st ‘ 𝑧 ) ) = ( ( ( 1^st ‘ 𝑧 ) [,) +∞ ) × ℝ ) )
51	43 50	eleqtrrd	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → 𝑧 ∈ ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ ( 1^st ‘ 𝑧 ) ) )
52		elfvunirn	⊢ ( 𝑧 ∈ ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ ( 1^st ‘ 𝑧 ) ) → 𝑧 ∈ ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) )
53	51 52	syl	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → 𝑧 ∈ ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) )
54	53	ssriv	⊢ ( ℝ × ℝ ) ⊆ ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) )
55		ssun3	⊢ ( ( ℝ × ℝ ) ⊆ ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) → ( ℝ × ℝ ) ⊆ ( ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) )
56	54 55	ax-mp	⊢ ( ℝ × ℝ ) ⊆ ( ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) )
57		uniun	⊢ ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ( ∪ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) )
58	56 57	sseqtrri	⊢ ( ℝ × ℝ ) ⊆ ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) )
59	33 58	eqssi	⊢ ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ( ℝ × ℝ )

Metamath Proof Explorer

Theorem sxbrsigalem0

Proof