Metamath Proof Explorer

Theorem 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 ( 𝐴 ⊆ ℝ* → ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 df-pr ⊢ { +∞ , -∞ } = ( { +∞ } ∪ { -∞ } )
2 1 ineq2i ⊢ ( 𝐴 ∩ { +∞ , -∞ } ) = ( 𝐴 ∩ ( { +∞ } ∪ { -∞ } ) )
3 indi ⊢ ( 𝐴 ∩ ( { +∞ } ∪ { -∞ } ) ) = ( ( 𝐴 ∩ { +∞ } ) ∪ ( 𝐴 ∩ { -∞ } ) )
4 2 3 eqtri ⊢ ( 𝐴 ∩ { +∞ , -∞ } ) = ( ( 𝐴 ∩ { +∞ } ) ∪ ( 𝐴 ∩ { -∞ } ) )
5 disjsn ⊢ ( ( 𝐴 ∩ { +∞ } ) = ∅ ↔ ¬ +∞ ∈ 𝐴 )
6 disjsn ⊢ ( ( 𝐴 ∩ { -∞ } ) = ∅ ↔ ¬ -∞ ∈ 𝐴 )
7 5 6 anbi12i ⊢ ( ( ( 𝐴 ∩ { +∞ } ) = ∅ ∧ ( 𝐴 ∩ { -∞ } ) = ∅ ) ↔ ( ¬ +∞ ∈ 𝐴 ∧ ¬ -∞ ∈ 𝐴 ) )
8 7 biimpri ⊢ ( ( ¬ +∞ ∈ 𝐴 ∧ ¬ -∞ ∈ 𝐴 ) → ( ( 𝐴 ∩ { +∞ } ) = ∅ ∧ ( 𝐴 ∩ { -∞ } ) = ∅ ) )
9 pm4.56 ⊢ ( ( ¬ +∞ ∈ 𝐴 ∧ ¬ -∞ ∈ 𝐴 ) ↔ ¬ ( +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) )
10 un00 ⊢ ( ( ( 𝐴 ∩ { +∞ } ) = ∅ ∧ ( 𝐴 ∩ { -∞ } ) = ∅ ) ↔ ( ( 𝐴 ∩ { +∞ } ) ∪ ( 𝐴 ∩ { -∞ } ) ) = ∅ )
11 8 9 10 3imtr3i ⊢ ( ¬ ( +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) → ( ( 𝐴 ∩ { +∞ } ) ∪ ( 𝐴 ∩ { -∞ } ) ) = ∅ )
12 4 11 eqtrid ⊢ ( ¬ ( +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) → ( 𝐴 ∩ { +∞ , -∞ } ) = ∅ )
13 reldisj ⊢ ( 𝐴 ⊆ ( ℝ ∪ { +∞ , -∞ } ) → ( ( 𝐴 ∩ { +∞ , -∞ } ) = ∅ ↔ 𝐴 ⊆ ( ( ℝ ∪ { +∞ , -∞ } ) ∖ { +∞ , -∞ } ) ) )
14 renfdisj ⊢ ( ℝ ∩ { +∞ , -∞ } ) = ∅
15 disj3 ⊢ ( ( ℝ ∩ { +∞ , -∞ } ) = ∅ ↔ ℝ = ( ℝ ∖ { +∞ , -∞ } ) )
16 14 15 mpbi ⊢ ℝ = ( ℝ ∖ { +∞ , -∞ } )
17 difun2 ⊢ ( ( ℝ ∪ { +∞ , -∞ } ) ∖ { +∞ , -∞ } ) = ( ℝ ∖ { +∞ , -∞ } )
18 16 17 eqtr4i ⊢ ℝ = ( ( ℝ ∪ { +∞ , -∞ } ) ∖ { +∞ , -∞ } )
19 18 sseq2i ⊢ ( 𝐴 ⊆ ℝ ↔ 𝐴 ⊆ ( ( ℝ ∪ { +∞ , -∞ } ) ∖ { +∞ , -∞ } ) )
20 13 19 bitr4di ⊢ ( 𝐴 ⊆ ( ℝ ∪ { +∞ , -∞ } ) → ( ( 𝐴 ∩ { +∞ , -∞ } ) = ∅ ↔ 𝐴 ⊆ ℝ ) )
21 12 20 syl5ib ⊢ ( 𝐴 ⊆ ( ℝ ∪ { +∞ , -∞ } ) → ( ¬ ( +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) → 𝐴 ⊆ ℝ ) )
22 21 orrd ⊢ ( 𝐴 ⊆ ( ℝ ∪ { +∞ , -∞ } ) → ( ( +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ∨ 𝐴 ⊆ ℝ ) )
23 df-xr ⊢ ℝ* = ( ℝ ∪ { +∞ , -∞ } )
24 23 sseq2i ⊢ ( 𝐴 ⊆ ℝ* ↔ 𝐴 ⊆ ( ℝ ∪ { +∞ , -∞ } ) )
25 3orrot ⊢ ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ↔ ( +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ∨ 𝐴 ⊆ ℝ ) )
26 df-3or ⊢ ( ( +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ∨ 𝐴 ⊆ ℝ ) ↔ ( ( +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ∨ 𝐴 ⊆ ℝ ) )
27 25 26 bitri ⊢ ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ↔ ( ( +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ∨ 𝐴 ⊆ ℝ ) )
28 22 24 27 3imtr4i ⊢ ( 𝐴 ⊆ ℝ* → ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) )