ssxr

Description: The three (non-exclusive) possibilities implied by a subset of extended reals. (Contributed by NM, 25-Oct-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

		Ref	Expression
	Assertion	ssxr	$⊢ A \subseteq ℝ^{*} \to (A \subseteq ℝ \lor +∞ \in A \lor −∞ \in A)$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$⊢ \{+∞, −∞\} = \{+∞\} \cup \{−∞\}$
2	1	ineq2i	$⊢ A \cap \{+∞, −∞\} = A \cap (\{+∞\} \cup \{−∞\})$
3		indi	$⊢ A \cap (\{+∞\} \cup \{−∞\}) = (A \cap \{+∞\}) \cup (A \cap \{−∞\})$
4	2 3	eqtri	$⊢ A \cap \{+∞, −∞\} = (A \cap \{+∞\}) \cup (A \cap \{−∞\})$
5		disjsn	$⊢ A \cap \{+∞\} = \emptyset \leftrightarrow \neg +∞ \in A$
6		disjsn	$⊢ A \cap \{−∞\} = \emptyset \leftrightarrow \neg −∞ \in A$
7	5 6	anbi12i	$⊢ (A \cap \{+∞\} = \emptyset \land A \cap \{−∞\} = \emptyset) \leftrightarrow (\neg +∞ \in A \land \neg −∞ \in A)$
8	7	biimpri	$⊢ (\neg +∞ \in A \land \neg −∞ \in A) \to (A \cap \{+∞\} = \emptyset \land A \cap \{−∞\} = \emptyset)$
9		pm4.56	$⊢ (\neg +∞ \in A \land \neg −∞ \in A) \leftrightarrow \neg (+∞ \in A \lor −∞ \in A)$
10		un00	$⊢ (A \cap \{+∞\} = \emptyset \land A \cap \{−∞\} = \emptyset) \leftrightarrow (A \cap \{+∞\}) \cup (A \cap \{−∞\}) = \emptyset$
11	8 9 10	3imtr3i	$⊢ \neg (+∞ \in A \lor −∞ \in A) \to (A \cap \{+∞\}) \cup (A \cap \{−∞\}) = \emptyset$
12	4 11	eqtrid	$⊢ \neg (+∞ \in A \lor −∞ \in A) \to A \cap \{+∞, −∞\} = \emptyset$
13		reldisj	$⊢ A \subseteq ℝ \cup \{+∞, −∞\} \to (A \cap \{+∞, −∞\} = \emptyset \leftrightarrow A \subseteq (ℝ \cup \{+∞, −∞\}) ∖ \{+∞, −∞\})$
14		renfdisj	$⊢ ℝ \cap \{+∞, −∞\} = \emptyset$
15		disj3	$⊢ ℝ \cap \{+∞, −∞\} = \emptyset \leftrightarrow ℝ = ℝ ∖ \{+∞, −∞\}$
16	14 15	mpbi	$⊢ ℝ = ℝ ∖ \{+∞, −∞\}$
17		difun2	$⊢ (ℝ \cup \{+∞, −∞\}) ∖ \{+∞, −∞\} = ℝ ∖ \{+∞, −∞\}$
18	16 17	eqtr4i	$⊢ ℝ = (ℝ \cup \{+∞, −∞\}) ∖ \{+∞, −∞\}$
19	18	sseq2i	$⊢ A \subseteq ℝ \leftrightarrow A \subseteq (ℝ \cup \{+∞, −∞\}) ∖ \{+∞, −∞\}$
20	13 19	bitr4di	$⊢ A \subseteq ℝ \cup \{+∞, −∞\} \to (A \cap \{+∞, −∞\} = \emptyset \leftrightarrow A \subseteq ℝ)$
21	12 20	imbitrid	$⊢ A \subseteq ℝ \cup \{+∞, −∞\} \to (\neg (+∞ \in A \lor −∞ \in A) \to A \subseteq ℝ)$
22	21	orrd	$⊢ A \subseteq ℝ \cup \{+∞, −∞\} \to ((+∞ \in A \lor −∞ \in A) \lor A \subseteq ℝ)$
23		df-xr	$⊢ ℝ^{*} = ℝ \cup \{+∞, −∞\}$
24	23	sseq2i	$⊢ A \subseteq ℝ^{*} \leftrightarrow A \subseteq ℝ \cup \{+∞, −∞\}$
25		3orrot	$⊢ (A \subseteq ℝ \lor +∞ \in A \lor −∞ \in A) \leftrightarrow (+∞ \in A \lor −∞ \in A \lor A \subseteq ℝ)$
26		df-3or	$⊢ (+∞ \in A \lor −∞ \in A \lor A \subseteq ℝ) \leftrightarrow ((+∞ \in A \lor −∞ \in A) \lor A \subseteq ℝ)$
27	25 26	bitri	$⊢ (A \subseteq ℝ \lor +∞ \in A \lor −∞ \in A) \leftrightarrow ((+∞ \in A \lor −∞ \in A) \lor A \subseteq ℝ)$
28	22 24 27	3imtr4i	$⊢ A \subseteq ℝ^{*} \to (A \subseteq ℝ \lor +∞ \in A \lor −∞ \in A)$

Metamath Proof Explorer

Theorem ssxr

Proof