Proof of Theorem prunioo
Step | Hyp | Ref
| Expression |
1 | | simp3 1056 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ≤ 𝐵) |
2 | | xrleloe 11853 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
3 | 2 | 3adant3 1074 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
4 | | df-pr 4128 |
. . . . . . . . . . 11
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
5 | 4 | uneq2i 3726 |
. . . . . . . . . 10
⊢ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = ((𝐴(,)𝐵) ∪ ({𝐴} ∪ {𝐵})) |
6 | | unass 3732 |
. . . . . . . . . 10
⊢ (((𝐴(,)𝐵) ∪ {𝐴}) ∪ {𝐵}) = ((𝐴(,)𝐵) ∪ ({𝐴} ∪ {𝐵})) |
7 | 5, 6 | eqtr4i 2635 |
. . . . . . . . 9
⊢ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (((𝐴(,)𝐵) ∪ {𝐴}) ∪ {𝐵}) |
8 | | uncom 3719 |
. . . . . . . . . . 11
⊢ ((𝐴(,)𝐵) ∪ {𝐴}) = ({𝐴} ∪ (𝐴(,)𝐵)) |
9 | | snunioo 12169 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵)) |
10 | 8, 9 | syl5eq 2656 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴}) = (𝐴[,)𝐵)) |
11 | 10 | uneq1d 3728 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → (((𝐴(,)𝐵) ∪ {𝐴}) ∪ {𝐵}) = ((𝐴[,)𝐵) ∪ {𝐵})) |
12 | 7, 11 | syl5eq 2656 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = ((𝐴[,)𝐵) ∪ {𝐵})) |
13 | 12 | 3expa 1257 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = ((𝐴[,)𝐵) ∪ {𝐵})) |
14 | 13 | 3adantl3 1212 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = ((𝐴[,)𝐵) ∪ {𝐵})) |
15 | | snunico 12170 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → ((𝐴[,)𝐵) ∪ {𝐵}) = (𝐴[,]𝐵)) |
16 | 15 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐴 < 𝐵) → ((𝐴[,)𝐵) ∪ {𝐵}) = (𝐴[,]𝐵)) |
17 | 14, 16 | eqtrd 2644 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) |
18 | 17 | ex 449 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐴 < 𝐵 → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))) |
19 | | iccid 12091 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ (𝐴[,]𝐴) = {𝐴}) |
20 | 19 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐴[,]𝐴) = {𝐴}) |
21 | 20 | eqcomd 2616 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → {𝐴} = (𝐴[,]𝐴)) |
22 | | uncom 3719 |
. . . . . . . 8
⊢ (∅
∪ {𝐴}) = ({𝐴} ∪
∅) |
23 | | un0 3919 |
. . . . . . . 8
⊢ ({𝐴} ∪ ∅) = {𝐴} |
24 | 22, 23 | eqtri 2632 |
. . . . . . 7
⊢ (∅
∪ {𝐴}) = {𝐴} |
25 | | iooid 12074 |
. . . . . . . . 9
⊢ (𝐴(,)𝐴) = ∅ |
26 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝐴 = 𝐵 → (𝐴(,)𝐴) = (𝐴(,)𝐵)) |
27 | 25, 26 | syl5eqr 2658 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 → ∅ = (𝐴(,)𝐵)) |
28 | | dfsn2 4138 |
. . . . . . . . 9
⊢ {𝐴} = {𝐴, 𝐴} |
29 | | preq2 4213 |
. . . . . . . . 9
⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵}) |
30 | 28, 29 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 → {𝐴} = {𝐴, 𝐵}) |
31 | 27, 30 | uneq12d 3730 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → (∅ ∪ {𝐴}) = ((𝐴(,)𝐵) ∪ {𝐴, 𝐵})) |
32 | 24, 31 | syl5eqr 2658 |
. . . . . 6
⊢ (𝐴 = 𝐵 → {𝐴} = ((𝐴(,)𝐵) ∪ {𝐴, 𝐵})) |
33 | | oveq2 6557 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐴[,]𝐴) = (𝐴[,]𝐵)) |
34 | 32, 33 | eqeq12d 2625 |
. . . . 5
⊢ (𝐴 = 𝐵 → ({𝐴} = (𝐴[,]𝐴) ↔ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))) |
35 | 21, 34 | syl5ibcom 234 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐴 = 𝐵 → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))) |
36 | 18, 35 | jaod 394 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))) |
37 | 3, 36 | sylbid 229 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐴 ≤ 𝐵 → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))) |
38 | 1, 37 | mpd 15 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) |