Proof of Theorem prunioo
Step | Hyp | Ref
| Expression |
1 | | simp3 1137 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ≤ 𝐵) |
2 | | xrleloe 12878 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
3 | 2 | 3adant3 1131 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
4 | | df-pr 4564 |
. . . . . . . . . . 11
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
5 | 4 | uneq2i 4094 |
. . . . . . . . . 10
⊢ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = ((𝐴(,)𝐵) ∪ ({𝐴} ∪ {𝐵})) |
6 | | unass 4100 |
. . . . . . . . . 10
⊢ (((𝐴(,)𝐵) ∪ {𝐴}) ∪ {𝐵}) = ((𝐴(,)𝐵) ∪ ({𝐴} ∪ {𝐵})) |
7 | 5, 6 | eqtr4i 2769 |
. . . . . . . . 9
⊢ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (((𝐴(,)𝐵) ∪ {𝐴}) ∪ {𝐵}) |
8 | | uncom 4087 |
. . . . . . . . . . 11
⊢ ((𝐴(,)𝐵) ∪ {𝐴}) = ({𝐴} ∪ (𝐴(,)𝐵)) |
9 | | snunioo 13210 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵)) |
10 | 8, 9 | eqtrid 2790 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴}) = (𝐴[,)𝐵)) |
11 | 10 | uneq1d 4096 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → (((𝐴(,)𝐵) ∪ {𝐴}) ∪ {𝐵}) = ((𝐴[,)𝐵) ∪ {𝐵})) |
12 | 7, 11 | eqtrid 2790 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = ((𝐴[,)𝐵) ∪ {𝐵})) |
13 | 12 | 3expa 1117 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = ((𝐴[,)𝐵) ∪ {𝐵})) |
14 | 13 | 3adantl3 1167 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = ((𝐴[,)𝐵) ∪ {𝐵})) |
15 | | snunico 13211 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → ((𝐴[,)𝐵) ∪ {𝐵}) = (𝐴[,]𝐵)) |
16 | 15 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐴 < 𝐵) → ((𝐴[,)𝐵) ∪ {𝐵}) = (𝐴[,]𝐵)) |
17 | 14, 16 | eqtrd 2778 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) |
18 | 17 | ex 413 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐴 < 𝐵 → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))) |
19 | | iccid 13124 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ (𝐴[,]𝐴) = {𝐴}) |
20 | 19 | 3ad2ant1 1132 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐴[,]𝐴) = {𝐴}) |
21 | 20 | eqcomd 2744 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → {𝐴} = (𝐴[,]𝐴)) |
22 | | uncom 4087 |
. . . . . . . 8
⊢ (∅
∪ {𝐴}) = ({𝐴} ∪
∅) |
23 | | un0 4324 |
. . . . . . . 8
⊢ ({𝐴} ∪ ∅) = {𝐴} |
24 | 22, 23 | eqtri 2766 |
. . . . . . 7
⊢ (∅
∪ {𝐴}) = {𝐴} |
25 | | iooid 13107 |
. . . . . . . . 9
⊢ (𝐴(,)𝐴) = ∅ |
26 | | oveq2 7283 |
. . . . . . . . 9
⊢ (𝐴 = 𝐵 → (𝐴(,)𝐴) = (𝐴(,)𝐵)) |
27 | 25, 26 | eqtr3id 2792 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 → ∅ = (𝐴(,)𝐵)) |
28 | | dfsn2 4574 |
. . . . . . . . 9
⊢ {𝐴} = {𝐴, 𝐴} |
29 | | preq2 4670 |
. . . . . . . . 9
⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵}) |
30 | 28, 29 | eqtrid 2790 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 → {𝐴} = {𝐴, 𝐵}) |
31 | 27, 30 | uneq12d 4098 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → (∅ ∪ {𝐴}) = ((𝐴(,)𝐵) ∪ {𝐴, 𝐵})) |
32 | 24, 31 | eqtr3id 2792 |
. . . . . 6
⊢ (𝐴 = 𝐵 → {𝐴} = ((𝐴(,)𝐵) ∪ {𝐴, 𝐵})) |
33 | | oveq2 7283 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐴[,]𝐴) = (𝐴[,]𝐵)) |
34 | 32, 33 | eqeq12d 2754 |
. . . . 5
⊢ (𝐴 = 𝐵 → ({𝐴} = (𝐴[,]𝐴) ↔ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))) |
35 | 21, 34 | syl5ibcom 244 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐴 = 𝐵 → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))) |
36 | 18, 35 | jaod 856 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))) |
37 | 3, 36 | sylbid 239 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐴 ≤ 𝐵 → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))) |
38 | 1, 37 | mpd 15 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) |