ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xrmaxiflemcom GIF version

Theorem xrmaxiflemcom 11241
Description: Lemma for xrmaxif 11243. Commutativity of an expression which we will later show to be the supremum. (Contributed by Jim Kingdon, 29-Apr-2023.)
Assertion
Ref Expression
xrmaxiflemcom ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))

Proof of Theorem xrmaxiflemcom
StepHypRef Expression
1 simpr 110 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → 𝐵 = +∞)
21iftrued 3541 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = +∞)
3 xrpnfdc 9829 . . . . . . 7 (𝐴 ∈ ℝ*DECID 𝐴 = +∞)
43ad2antrr 488 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → DECID 𝐴 = +∞)
5 exmiddc 836 . . . . . 6 (DECID 𝐴 = +∞ → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
64, 5syl 14 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
7 eqid 2177 . . . . . . . 8 +∞ = +∞
87biantru 302 . . . . . . 7 (𝐴 = +∞ ↔ (𝐴 = +∞ ∧ +∞ = +∞))
98a1i 9 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (𝐴 = +∞ ↔ (𝐴 = +∞ ∧ +∞ = +∞)))
10 xrmnfdc 9830 . . . . . . . . . . 11 (𝐴 ∈ ℝ*DECID 𝐴 = -∞)
1110ad2antrr 488 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → DECID 𝐴 = -∞)
12 exmiddc 836 . . . . . . . . . 10 (DECID 𝐴 = -∞ → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
1311, 12syl 14 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
14 iba 300 . . . . . . . . . . . 12 (+∞ = 𝐵 → (𝐴 = -∞ ↔ (𝐴 = -∞ ∧ +∞ = 𝐵)))
1514eqcoms 2180 . . . . . . . . . . 11 (𝐵 = +∞ → (𝐴 = -∞ ↔ (𝐴 = -∞ ∧ +∞ = 𝐵)))
1615adantl 277 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (𝐴 = -∞ ↔ (𝐴 = -∞ ∧ +∞ = 𝐵)))
171iftrued 3541 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))) = +∞)
1817eqcomd 2183 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))
1918biantrud 304 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (¬ 𝐴 = -∞ ↔ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
2016, 19orbi12d 793 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → ((𝐴 = -∞ ∨ ¬ 𝐴 = -∞) ↔ ((𝐴 = -∞ ∧ +∞ = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
2113, 20mpbid 147 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → ((𝐴 = -∞ ∧ +∞ = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
22 eqifdc 3568 . . . . . . . . 9 (DECID 𝐴 = -∞ → (+∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) ↔ ((𝐴 = -∞ ∧ +∞ = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
2311, 22syl 14 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (+∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) ↔ ((𝐴 = -∞ ∧ +∞ = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
2421, 23mpbird 167 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
2524biantrud 304 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (¬ 𝐴 = +∞ ↔ (¬ 𝐴 = +∞ ∧ +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
269, 25orbi12d 793 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → ((𝐴 = +∞ ∨ ¬ 𝐴 = +∞) ↔ ((𝐴 = +∞ ∧ +∞ = +∞) ∨ (¬ 𝐴 = +∞ ∧ +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))))
276, 26mpbid 147 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → ((𝐴 = +∞ ∧ +∞ = +∞) ∨ (¬ 𝐴 = +∞ ∧ +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
28 eqifdc 3568 . . . . 5 (DECID 𝐴 = +∞ → (+∞ = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))) ↔ ((𝐴 = +∞ ∧ +∞ = +∞) ∨ (¬ 𝐴 = +∞ ∧ +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))))
294, 28syl 14 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (+∞ = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))) ↔ ((𝐴 = +∞ ∧ +∞ = +∞) ∨ (¬ 𝐴 = +∞ ∧ +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))))
3027, 29mpbird 167 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → +∞ = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
312, 30eqtrd 2210 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
323, 5syl 14 . . . . . . . 8 (𝐴 ∈ ℝ* → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
3332ad3antrrr 492 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
34 pm4.24 395 . . . . . . . . 9 (𝐴 = +∞ ↔ (𝐴 = +∞ ∧ 𝐴 = +∞))
3534a1i 9 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = +∞ ↔ (𝐴 = +∞ ∧ 𝐴 = +∞)))
3610ad3antrrr 492 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → DECID 𝐴 = -∞)
3736, 12syl 14 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
38 simpr 110 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐵 = -∞)
3938eqeq2d 2189 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = 𝐵𝐴 = -∞))
4039anbi2d 464 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ↔ (𝐴 = -∞ ∧ 𝐴 = -∞)))
41 anidm 396 . . . . . . . . . . . . 13 ((𝐴 = -∞ ∧ 𝐴 = -∞) ↔ 𝐴 = -∞)
4240, 41bitr2di 197 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = -∞ ↔ (𝐴 = -∞ ∧ 𝐴 = 𝐵)))
43 eqid 2177 . . . . . . . . . . . . . 14 𝐴 = 𝐴
4443biantru 302 . . . . . . . . . . . . 13 𝐴 = -∞ ↔ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴))
4544a1i 9 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (¬ 𝐴 = -∞ ↔ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴)))
4642, 45orbi12d 793 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = -∞ ∨ ¬ 𝐴 = -∞) ↔ ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴))))
4737, 46mpbid 147 . . . . . . . . . 10 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴)))
48 eqifdc 3568 . . . . . . . . . . 11 (DECID 𝐴 = -∞ → (𝐴 = if(𝐴 = -∞, 𝐵, 𝐴) ↔ ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴))))
4936, 48syl 14 . . . . . . . . . 10 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = if(𝐴 = -∞, 𝐵, 𝐴) ↔ ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴))))
5047, 49mpbird 167 . . . . . . . . 9 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴))
5150biantrud 304 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (¬ 𝐴 = +∞ ↔ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴))))
5235, 51orbi12d 793 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = +∞ ∨ ¬ 𝐴 = +∞) ↔ ((𝐴 = +∞ ∧ 𝐴 = +∞) ∨ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴)))))
5333, 52mpbid 147 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = +∞ ∧ 𝐴 = +∞) ∨ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴))))
543ad3antrrr 492 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → DECID 𝐴 = +∞)
55 eqifdc 3568 . . . . . . 7 (DECID 𝐴 = +∞ → (𝐴 = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, 𝐴)) ↔ ((𝐴 = +∞ ∧ 𝐴 = +∞) ∨ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴)))))
5654, 55syl 14 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, 𝐴)) ↔ ((𝐴 = +∞ ∧ 𝐴 = +∞) ∨ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴)))))
5753, 56mpbird 167 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐴 = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, 𝐴)))
5838iftrued 3541 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = 𝐴)
5938iftrued 3541 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )) = 𝐴)
6059ifeq2d 3552 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐴 = -∞, 𝐵, 𝐴))
6160ifeq2d 3552 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, 𝐴)))
6257, 58, 613eqtr4d 2220 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
63 simpr 110 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → ¬ 𝐵 = -∞)
6463iffalsed 3544 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
6563iffalsed 3544 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )) = sup({𝐵, 𝐴}, ℝ, < ))
6665ifeq2d 3552 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < )))
6766ifeq2d 3552 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < ))))
68 maxcom 11196 . . . . . . 7 sup({𝐵, 𝐴}, ℝ, < ) = sup({𝐴, 𝐵}, ℝ, < )
69 ifeq2 3538 . . . . . . 7 (sup({𝐵, 𝐴}, ℝ, < ) = sup({𝐴, 𝐵}, ℝ, < ) → if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < )) = if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))
70 ifeq2 3538 . . . . . . 7 (if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < )) = if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
7168, 69, 70mp2b 8 . . . . . 6 if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))
7267, 71eqtrdi 2226 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
7364, 72eqtr4d 2213 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
74 xrmnfdc 9830 . . . . . 6 (𝐵 ∈ ℝ*DECID 𝐵 = -∞)
75 exmiddc 836 . . . . . 6 (DECID 𝐵 = -∞ → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
7674, 75syl 14 . . . . 5 (𝐵 ∈ ℝ* → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
7776ad2antlr 489 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
7862, 73, 77mpjaodan 798 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
79 simpr 110 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → ¬ 𝐵 = +∞)
8079iffalsed 3544 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))))
8179iffalsed 3544 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))
8281ifeq2d 3552 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) = if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))
8382ifeq2d 3552 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
8478, 80, 833eqtr4d 2220 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
85 xrpnfdc 9829 . . . 4 (𝐵 ∈ ℝ*DECID 𝐵 = +∞)
86 exmiddc 836 . . . 4 (DECID 𝐵 = +∞ → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
8785, 86syl 14 . . 3 (𝐵 ∈ ℝ* → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
8887adantl 277 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
8931, 84, 88mpjaodan 798 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  DECID wdc 834   = wceq 1353  wcel 2148  ifcif 3534  {cpr 3592  supcsup 6975  cr 7801  +∞cpnf 7979  -∞cmnf 7980  *cxr 7981   < clt 7982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-un 4430  ax-setind 4533  ax-cnex 7893  ax-resscn 7894
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-uni 3808  df-sup 6977  df-pnf 7984  df-mnf 7985  df-xr 7986
This theorem is referenced by:  xrmaxiflemval  11242
  Copyright terms: Public domain W3C validator