| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | difssd 4136 | . . . . . . . 8
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝐴}) ⊆ (𝐴(,)𝐵)) | 
| 2 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵)) | 
| 3 |  | lbioo 13419 | . . . . . . . . . . . 12
⊢  ¬
𝐴 ∈ (𝐴(,)𝐵) | 
| 4 |  | eleq1 2828 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝐴 → (𝑥 ∈ (𝐴(,)𝐵) ↔ 𝐴 ∈ (𝐴(,)𝐵))) | 
| 5 | 4 | biimpcd 249 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴(,)𝐵) → (𝑥 = 𝐴 → 𝐴 ∈ (𝐴(,)𝐵))) | 
| 6 | 3, 5 | mtoi 199 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ¬ 𝑥 = 𝐴) | 
| 7 | 6 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ¬ 𝑥 = 𝐴) | 
| 8 |  | velsn 4641 | . . . . . . . . . 10
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | 
| 9 | 7, 8 | sylnibr 329 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ¬ 𝑥 ∈ {𝐴}) | 
| 10 | 2, 9 | eldifd 3961 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ((𝐴(,)𝐵) ∖ {𝐴})) | 
| 11 | 1, 10 | eqelssd 4004 | . . . . . . 7
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝐴}) = (𝐴(,)𝐵)) | 
| 12 | 11 | ineq2d 4219 | . . . . . 6
⊢ (𝜑 → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐴})) = ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵))) | 
| 13 | 12 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐴})) = ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵))) | 
| 14 |  | simplrl 776 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → 𝑎 ∈ ℝ*) | 
| 15 |  | simplrr 777 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → 𝑏 ∈ ℝ*) | 
| 16 |  | lptioo1.2 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 17 | 16 | rexrd 11312 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 18 |  | lptioo1.3 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 19 | 17, 18 | jca 511 | . . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) | 
| 20 | 19 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) | 
| 21 |  | iooin 13422 | . . . . . . 7
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
→ ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) | 
| 22 | 14, 15, 20, 21 | syl21anc 837 | . . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) | 
| 23 |  | elioo3g 13417 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (𝑎(,)𝑏) ↔ ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) ∧ (𝑎 < 𝐴 ∧ 𝐴 < 𝑏))) | 
| 24 | 23 | biimpi 216 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑎(,)𝑏) → ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) ∧ (𝑎 < 𝐴 ∧ 𝐴 < 𝑏))) | 
| 25 | 24 | simpld 494 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑎(,)𝑏) → (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝐴 ∈
ℝ*)) | 
| 26 | 25 | simp1d 1142 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑎(,)𝑏) → 𝑎 ∈ ℝ*) | 
| 27 | 25 | simp3d 1144 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑎(,)𝑏) → 𝐴 ∈
ℝ*) | 
| 28 | 24 | simprd 495 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑎(,)𝑏) → (𝑎 < 𝐴 ∧ 𝐴 < 𝑏)) | 
| 29 | 28 | simpld 494 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑎(,)𝑏) → 𝑎 < 𝐴) | 
| 30 | 26, 27, 29 | xrltled 13193 | . . . . . . . . . 10
⊢ (𝐴 ∈ (𝑎(,)𝑏) → 𝑎 ≤ 𝐴) | 
| 31 | 30 | iftrued 4532 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝑎(,)𝑏) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝐴) | 
| 32 | 31 | adantl 481 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝐴) | 
| 33 | 28 | simprd 495 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑎(,)𝑏) → 𝐴 < 𝑏) | 
| 34 | 33 | ad2antlr 727 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ 𝑏 ≤ 𝐵) → 𝐴 < 𝑏) | 
| 35 |  | iftrue 4530 | . . . . . . . . . . . 12
⊢ (𝑏 ≤ 𝐵 → if(𝑏 ≤ 𝐵, 𝑏, 𝐵) = 𝑏) | 
| 36 | 35 | eqcomd 2742 | . . . . . . . . . . 11
⊢ (𝑏 ≤ 𝐵 → 𝑏 = if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) | 
| 37 | 36 | adantl 481 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ 𝑏 ≤ 𝐵) → 𝑏 = if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) | 
| 38 | 34, 37 | breqtrd 5168 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ 𝑏 ≤ 𝐵) → 𝐴 < if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) | 
| 39 |  | lptioo1.4 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 < 𝐵) | 
| 40 | 39 | ad3antrrr 730 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑏 ≤ 𝐵) → 𝐴 < 𝐵) | 
| 41 |  | iffalse 4533 | . . . . . . . . . . . 12
⊢ (¬
𝑏 ≤ 𝐵 → if(𝑏 ≤ 𝐵, 𝑏, 𝐵) = 𝐵) | 
| 42 | 41 | eqcomd 2742 | . . . . . . . . . . 11
⊢ (¬
𝑏 ≤ 𝐵 → 𝐵 = if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) | 
| 43 | 42 | adantl 481 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑏 ≤ 𝐵) → 𝐵 = if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) | 
| 44 | 40, 43 | breqtrd 5168 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑏 ≤ 𝐵) → 𝐴 < if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) | 
| 45 | 38, 44 | pm2.61dan 812 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → 𝐴 < if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) | 
| 46 | 32, 45 | eqbrtrd 5164 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) | 
| 47 | 17 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ 𝑎 ≤ 𝐴) → 𝐴 ∈
ℝ*) | 
| 48 | 14 | adantr 480 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑎 ≤ 𝐴) → 𝑎 ∈ ℝ*) | 
| 49 | 47, 48 | ifclda 4560 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) ∈
ℝ*) | 
| 50 | 15 | adantr 480 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ 𝑏 ≤ 𝐵) → 𝑏 ∈ ℝ*) | 
| 51 | 18 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑏 ≤ 𝐵) → 𝐵 ∈
ℝ*) | 
| 52 | 50, 51 | ifclda 4560 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → if(𝑏 ≤ 𝐵, 𝑏, 𝐵) ∈
ℝ*) | 
| 53 |  | ioon0 13414 | . . . . . . . 8
⊢
((if(𝑎 ≤ 𝐴, 𝐴, 𝑎) ∈ ℝ* ∧ if(𝑏 ≤ 𝐵, 𝑏, 𝐵) ∈ ℝ*) →
((if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) ≠ ∅ ↔ if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) | 
| 54 | 49, 52, 53 | syl2anc 584 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → ((if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) ≠ ∅ ↔ if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) | 
| 55 | 46, 54 | mpbird 257 | . . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) ≠ ∅) | 
| 56 | 22, 55 | eqnetrd 3007 | . . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵)) ≠ ∅) | 
| 57 | 13, 56 | eqnetrd 3007 | . . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐴})) ≠ ∅) | 
| 58 | 57 | ex 412 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
→ (𝐴 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐴})) ≠ ∅)) | 
| 59 | 58 | ralrimivva 3201 | . 2
⊢ (𝜑 → ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐴 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐴})) ≠ ∅)) | 
| 60 |  | lptioo1.1 | . . 3
⊢ 𝐽 = (topGen‘ran
(,)) | 
| 61 |  | ioossre 13449 | . . . 4
⊢ (𝐴(,)𝐵) ⊆ ℝ | 
| 62 | 61 | a1i 11 | . . 3
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) | 
| 63 | 60, 62, 16 | islptre 45639 | . 2
⊢ (𝜑 → (𝐴 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵)) ↔ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐴 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐴})) ≠ ∅))) | 
| 64 | 59, 63 | mpbird 257 | 1
⊢ (𝜑 → 𝐴 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵))) |