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

Theorem xrmaxiflemcom 11049
 Description: Lemma for xrmaxif 11051. 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 109 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → 𝐵 = +∞)
21iftrued 3485 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = +∞)
3 xrpnfdc 9654 . . . . . . 7 (𝐴 ∈ ℝ*DECID 𝐴 = +∞)
43ad2antrr 480 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → DECID 𝐴 = +∞)
5 exmiddc 822 . . . . . 6 (DECID 𝐴 = +∞ → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
64, 5syl 14 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
7 eqid 2140 . . . . . . . 8 +∞ = +∞
87biantru 300 . . . . . . 7 (𝐴 = +∞ ↔ (𝐴 = +∞ ∧ +∞ = +∞))
98a1i 9 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (𝐴 = +∞ ↔ (𝐴 = +∞ ∧ +∞ = +∞)))
10 xrmnfdc 9655 . . . . . . . . . . 11 (𝐴 ∈ ℝ*DECID 𝐴 = -∞)
1110ad2antrr 480 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → DECID 𝐴 = -∞)
12 exmiddc 822 . . . . . . . . . 10 (DECID 𝐴 = -∞ → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
1311, 12syl 14 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
14 iba 298 . . . . . . . . . . . 12 (+∞ = 𝐵 → (𝐴 = -∞ ↔ (𝐴 = -∞ ∧ +∞ = 𝐵)))
1514eqcoms 2143 . . . . . . . . . . 11 (𝐵 = +∞ → (𝐴 = -∞ ↔ (𝐴 = -∞ ∧ +∞ = 𝐵)))
1615adantl 275 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (𝐴 = -∞ ↔ (𝐴 = -∞ ∧ +∞ = 𝐵)))
171iftrued 3485 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))) = +∞)
1817eqcomd 2146 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))
1918biantrud 302 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (¬ 𝐴 = -∞ ↔ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
2016, 19orbi12d 783 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → ((𝐴 = -∞ ∨ ¬ 𝐴 = -∞) ↔ ((𝐴 = -∞ ∧ +∞ = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
2113, 20mpbid 146 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → ((𝐴 = -∞ ∧ +∞ = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
22 eqifdc 3510 . . . . . . . . 9 (DECID 𝐴 = -∞ → (+∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) ↔ ((𝐴 = -∞ ∧ +∞ = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
2311, 22syl 14 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (+∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) ↔ ((𝐴 = -∞ ∧ +∞ = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
2421, 23mpbird 166 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
2524biantrud 302 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (¬ 𝐴 = +∞ ↔ (¬ 𝐴 = +∞ ∧ +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
269, 25orbi12d 783 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → ((𝐴 = +∞ ∨ ¬ 𝐴 = +∞) ↔ ((𝐴 = +∞ ∧ +∞ = +∞) ∨ (¬ 𝐴 = +∞ ∧ +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))))
276, 26mpbid 146 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → ((𝐴 = +∞ ∧ +∞ = +∞) ∨ (¬ 𝐴 = +∞ ∧ +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
28 eqifdc 3510 . . . . 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 166 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → +∞ = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
312, 30eqtrd 2173 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
323, 5syl 14 . . . . . . . 8 (𝐴 ∈ ℝ* → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
3332ad3antrrr 484 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
34 pm4.24 393 . . . . . . . . 9 (𝐴 = +∞ ↔ (𝐴 = +∞ ∧ 𝐴 = +∞))
3534a1i 9 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = +∞ ↔ (𝐴 = +∞ ∧ 𝐴 = +∞)))
3610ad3antrrr 484 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → DECID 𝐴 = -∞)
3736, 12syl 14 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
38 simpr 109 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐵 = -∞)
3938eqeq2d 2152 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = 𝐵𝐴 = -∞))
4039anbi2d 460 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ↔ (𝐴 = -∞ ∧ 𝐴 = -∞)))
41 anidm 394 . . . . . . . . . . . . 13 ((𝐴 = -∞ ∧ 𝐴 = -∞) ↔ 𝐴 = -∞)
4240, 41syl6rbb 196 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = -∞ ↔ (𝐴 = -∞ ∧ 𝐴 = 𝐵)))
43 eqid 2140 . . . . . . . . . . . . . 14 𝐴 = 𝐴
4443biantru 300 . . . . . . . . . . . . 13 𝐴 = -∞ ↔ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴))
4544a1i 9 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (¬ 𝐴 = -∞ ↔ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴)))
4642, 45orbi12d 783 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = -∞ ∨ ¬ 𝐴 = -∞) ↔ ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴))))
4737, 46mpbid 146 . . . . . . . . . 10 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴)))
48 eqifdc 3510 . . . . . . . . . . 11 (DECID 𝐴 = -∞ → (𝐴 = if(𝐴 = -∞, 𝐵, 𝐴) ↔ ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴))))
4936, 48syl 14 . . . . . . . . . 10 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = if(𝐴 = -∞, 𝐵, 𝐴) ↔ ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴))))
5047, 49mpbird 166 . . . . . . . . 9 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴))
5150biantrud 302 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (¬ 𝐴 = +∞ ↔ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴))))
5235, 51orbi12d 783 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = +∞ ∨ ¬ 𝐴 = +∞) ↔ ((𝐴 = +∞ ∧ 𝐴 = +∞) ∨ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴)))))
5333, 52mpbid 146 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = +∞ ∧ 𝐴 = +∞) ∨ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴))))
543ad3antrrr 484 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → DECID 𝐴 = +∞)
55 eqifdc 3510 . . . . . . 7 (DECID 𝐴 = +∞ → (𝐴 = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, 𝐴)) ↔ ((𝐴 = +∞ ∧ 𝐴 = +∞) ∨ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴)))))
5654, 55syl 14 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, 𝐴)) ↔ ((𝐴 = +∞ ∧ 𝐴 = +∞) ∨ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴)))))
5753, 56mpbird 166 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐴 = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, 𝐴)))
5838iftrued 3485 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = 𝐴)
5938iftrued 3485 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )) = 𝐴)
6059ifeq2d 3494 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐴 = -∞, 𝐵, 𝐴))
6160ifeq2d 3494 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, 𝐴)))
6257, 58, 613eqtr4d 2183 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
63 simpr 109 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → ¬ 𝐵 = -∞)
6463iffalsed 3488 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
6563iffalsed 3488 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )) = sup({𝐵, 𝐴}, ℝ, < ))
6665ifeq2d 3494 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < )))
6766ifeq2d 3494 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < ))))
68 maxcom 11006 . . . . . . 7 sup({𝐵, 𝐴}, ℝ, < ) = sup({𝐴, 𝐵}, ℝ, < )
69 ifeq2 3482 . . . . . . 7 (sup({𝐵, 𝐴}, ℝ, < ) = sup({𝐴, 𝐵}, ℝ, < ) → if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < )) = if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))
70 ifeq2 3482 . . . . . . 7 (if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < )) = if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
7168, 69, 70mp2b 8 . . . . . 6 if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))
7267, 71eqtrdi 2189 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
7364, 72eqtr4d 2176 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
74 xrmnfdc 9655 . . . . . 6 (𝐵 ∈ ℝ*DECID 𝐵 = -∞)
75 exmiddc 822 . . . . . 6 (DECID 𝐵 = -∞ → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
7674, 75syl 14 . . . . 5 (𝐵 ∈ ℝ* → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
7776ad2antlr 481 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
7862, 73, 77mpjaodan 788 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
79 simpr 109 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → ¬ 𝐵 = +∞)
8079iffalsed 3488 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))))
8179iffalsed 3488 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))
8281ifeq2d 3494 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) = if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))
8382ifeq2d 3494 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
8478, 80, 833eqtr4d 2183 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
85 xrpnfdc 9654 . . . 4 (𝐵 ∈ ℝ*DECID 𝐵 = +∞)
86 exmiddc 822 . . . 4 (DECID 𝐵 = +∞ → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
8785, 86syl 14 . . 3 (𝐵 ∈ ℝ* → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
8887adantl 275 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
8931, 84, 88mpjaodan 788 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 820   = wceq 1332   ∈ wcel 1481  ifcif 3478  {cpr 3532  supcsup 6876  ℝcr 7642  +∞cpnf 7820  -∞cmnf 7821  ℝ*cxr 7822   < clt 7823 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-pow 4105  ax-un 4362  ax-setind 4459  ax-cnex 7734  ax-resscn 7735 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2691  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-if 3479  df-pw 3516  df-sn 3537  df-pr 3538  df-uni 3744  df-sup 6878  df-pnf 7825  df-mnf 7826  df-xr 7827 This theorem is referenced by:  xrmaxiflemval  11050
 Copyright terms: Public domain W3C validator