| Step | Hyp | Ref
| Expression |
| 1 | | unss 4190 |
. . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) ↔ (𝐴 ∪ 𝐵) ⊆
ℝ*) |
| 2 | 1 | biimpi 216 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐴 ∪ 𝐵) ⊆
ℝ*) |
| 3 | 2 | 3adant3 1133 |
. 2
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ* ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
→ (𝐴 ∪ 𝐵) ⊆
ℝ*) |
| 4 | | supxrcl 13357 |
. . 3
⊢ (𝐵 ⊆ ℝ*
→ sup(𝐵,
ℝ*, < ) ∈ ℝ*) |
| 5 | 4 | 3ad2ant2 1135 |
. 2
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ* ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
→ sup(𝐵,
ℝ*, < ) ∈ ℝ*) |
| 6 | | elun 4153 |
. . . 4
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) |
| 7 | | xrltso 13183 |
. . . . . . . . 9
⊢ < Or
ℝ* |
| 8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ*
→ < Or ℝ*) |
| 9 | | xrsupss 13351 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ*
→ ∃𝑦 ∈
ℝ* (∀𝑧 ∈ 𝐴 ¬ 𝑦 < 𝑧 ∧ ∀𝑧 ∈ ℝ* (𝑧 < 𝑦 → ∃𝑤 ∈ 𝐴 𝑧 < 𝑤))) |
| 10 | 8, 9 | supub 9499 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ*
→ (𝑥 ∈ 𝐴 → ¬ sup(𝐴, ℝ*, < )
< 𝑥)) |
| 11 | 10 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ* ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
→ (𝑥 ∈ 𝐴 → ¬ sup(𝐴, ℝ*, < )
< 𝑥)) |
| 12 | | supxrcl 13357 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ ℝ*
→ sup(𝐴,
ℝ*, < ) ∈ ℝ*) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) ∧ 𝑥 ∈ 𝐴) → sup(𝐴, ℝ*, < ) ∈
ℝ*) |
| 14 | 4 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) ∧ 𝑥 ∈ 𝐴) → sup(𝐵, ℝ*, < ) ∈
ℝ*) |
| 15 | | ssel2 3978 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ*) |
| 16 | 15 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ*) |
| 17 | | xrlelttr 13198 |
. . . . . . . . . . . 12
⊢
((sup(𝐴,
ℝ*, < ) ∈ ℝ* ∧ sup(𝐵, ℝ*, < )
∈ ℝ* ∧ 𝑥 ∈ ℝ*) →
((sup(𝐴,
ℝ*, < ) ≤ sup(𝐵, ℝ*, < ) ∧
sup(𝐵, ℝ*,
< ) < 𝑥) →
sup(𝐴, ℝ*,
< ) < 𝑥)) |
| 18 | 13, 14, 16, 17 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) ∧ 𝑥 ∈ 𝐴) → ((sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < )
∧ sup(𝐵,
ℝ*, < ) < 𝑥) → sup(𝐴, ℝ*, < ) < 𝑥)) |
| 19 | 18 | expdimp 452 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) ∧ 𝑥 ∈ 𝐴) ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
→ (sup(𝐵,
ℝ*, < ) < 𝑥 → sup(𝐴, ℝ*, < ) < 𝑥)) |
| 20 | 19 | con3d 152 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) ∧ 𝑥 ∈ 𝐴) ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
→ (¬ sup(𝐴,
ℝ*, < ) < 𝑥 → ¬ sup(𝐵, ℝ*, < ) < 𝑥)) |
| 21 | 20 | exp41 434 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ*
→ (𝐵 ⊆
ℝ* → (𝑥 ∈ 𝐴 → (sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < )
→ (¬ sup(𝐴,
ℝ*, < ) < 𝑥 → ¬ sup(𝐵, ℝ*, < ) < 𝑥))))) |
| 22 | 21 | com34 91 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ*
→ (𝐵 ⊆
ℝ* → (sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < )
→ (𝑥 ∈ 𝐴 → (¬ sup(𝐴, ℝ*, < )
< 𝑥 → ¬
sup(𝐵, ℝ*,
< ) < 𝑥))))) |
| 23 | 22 | 3imp 1111 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ* ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
→ (𝑥 ∈ 𝐴 → (¬ sup(𝐴, ℝ*, < )
< 𝑥 → ¬
sup(𝐵, ℝ*,
< ) < 𝑥))) |
| 24 | 11, 23 | mpdd 43 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ* ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
→ (𝑥 ∈ 𝐴 → ¬ sup(𝐵, ℝ*, < )
< 𝑥)) |
| 25 | 7 | a1i 11 |
. . . . . . 7
⊢ (𝐵 ⊆ ℝ*
→ < Or ℝ*) |
| 26 | | xrsupss 13351 |
. . . . . . 7
⊢ (𝐵 ⊆ ℝ*
→ ∃𝑦 ∈
ℝ* (∀𝑧 ∈ 𝐵 ¬ 𝑦 < 𝑧 ∧ ∀𝑧 ∈ ℝ* (𝑧 < 𝑦 → ∃𝑤 ∈ 𝐵 𝑧 < 𝑤))) |
| 27 | 25, 26 | supub 9499 |
. . . . . 6
⊢ (𝐵 ⊆ ℝ*
→ (𝑥 ∈ 𝐵 → ¬ sup(𝐵, ℝ*, < )
< 𝑥)) |
| 28 | 27 | 3ad2ant2 1135 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ* ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
→ (𝑥 ∈ 𝐵 → ¬ sup(𝐵, ℝ*, < )
< 𝑥)) |
| 29 | 24, 28 | jaod 860 |
. . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ* ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
→ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → ¬ sup(𝐵, ℝ*, < ) < 𝑥)) |
| 30 | 6, 29 | biimtrid 242 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ* ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
→ (𝑥 ∈ (𝐴 ∪ 𝐵) → ¬ sup(𝐵, ℝ*, < ) < 𝑥)) |
| 31 | 30 | ralrimiv 3145 |
. 2
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ* ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
→ ∀𝑥 ∈
(𝐴 ∪ 𝐵) ¬ sup(𝐵, ℝ*, < ) < 𝑥) |
| 32 | | rexr 11307 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
| 33 | | xrsupss 13351 |
. . . . . . . 8
⊢ (𝐵 ⊆ ℝ*
→ ∃𝑥 ∈
ℝ* (∀𝑧 ∈ 𝐵 ¬ 𝑥 < 𝑧 ∧ ∀𝑧 ∈ ℝ* (𝑧 < 𝑥 → ∃𝑦 ∈ 𝐵 𝑧 < 𝑦))) |
| 34 | 25, 33 | suplub 9500 |
. . . . . . 7
⊢ (𝐵 ⊆ ℝ*
→ ((𝑥 ∈
ℝ* ∧ 𝑥
< sup(𝐵,
ℝ*, < )) → ∃𝑦 ∈ 𝐵 𝑥 < 𝑦)) |
| 35 | 32, 34 | sylani 604 |
. . . . . 6
⊢ (𝐵 ⊆ ℝ*
→ ((𝑥 ∈ ℝ
∧ 𝑥 < sup(𝐵, ℝ*, < ))
→ ∃𝑦 ∈
𝐵 𝑥 < 𝑦)) |
| 36 | | elun2 4183 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ (𝐴 ∪ 𝐵)) |
| 37 | 36 | anim1i 615 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 < 𝑦) → (𝑦 ∈ (𝐴 ∪ 𝐵) ∧ 𝑥 < 𝑦)) |
| 38 | 37 | reximi2 3079 |
. . . . . 6
⊢
(∃𝑦 ∈
𝐵 𝑥 < 𝑦 → ∃𝑦 ∈ (𝐴 ∪ 𝐵)𝑥 < 𝑦) |
| 39 | 35, 38 | syl6 35 |
. . . . 5
⊢ (𝐵 ⊆ ℝ*
→ ((𝑥 ∈ ℝ
∧ 𝑥 < sup(𝐵, ℝ*, < ))
→ ∃𝑦 ∈
(𝐴 ∪ 𝐵)𝑥 < 𝑦)) |
| 40 | 39 | expd 415 |
. . . 4
⊢ (𝐵 ⊆ ℝ*
→ (𝑥 ∈ ℝ
→ (𝑥 < sup(𝐵, ℝ*, < )
→ ∃𝑦 ∈
(𝐴 ∪ 𝐵)𝑥 < 𝑦))) |
| 41 | 40 | ralrimiv 3145 |
. . 3
⊢ (𝐵 ⊆ ℝ*
→ ∀𝑥 ∈
ℝ (𝑥 < sup(𝐵, ℝ*, < )
→ ∃𝑦 ∈
(𝐴 ∪ 𝐵)𝑥 < 𝑦)) |
| 42 | 41 | 3ad2ant2 1135 |
. 2
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ* ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
→ ∀𝑥 ∈
ℝ (𝑥 < sup(𝐵, ℝ*, < )
→ ∃𝑦 ∈
(𝐴 ∪ 𝐵)𝑥 < 𝑦)) |
| 43 | | supxr 13355 |
. 2
⊢ ((((𝐴 ∪ 𝐵) ⊆ ℝ* ∧
sup(𝐵, ℝ*,
< ) ∈ ℝ*) ∧ (∀𝑥 ∈ (𝐴 ∪ 𝐵) ¬ sup(𝐵, ℝ*, < ) < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < sup(𝐵, ℝ*, < ) →
∃𝑦 ∈ (𝐴 ∪ 𝐵)𝑥 < 𝑦))) → sup((𝐴 ∪ 𝐵), ℝ*, < ) = sup(𝐵, ℝ*, <
)) |
| 44 | 3, 5, 31, 42, 43 | syl22anc 839 |
1
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ* ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
→ sup((𝐴 ∪ 𝐵), ℝ*, < ) =
sup(𝐵, ℝ*,
< )) |