Theorem xrmaxiflemcom 11021

Description: Lemma for xrmaxif 11023. 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

Step	Hyp	Ref	Expression
1		simpr 109	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → 𝐵 = +∞)
2	1	iftrued 3481	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = +∞)
3		xrpnfdc 9628	. . . . . . 7 ⊢ (𝐴 ∈ ℝ* → DECID 𝐴 = +∞)
4	3	ad2antrr 479	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → DECID 𝐴 = +∞)
5		exmiddc 821	. . . . . 6 ⊢ (DECID 𝐴 = +∞ → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
6	4, 5	syl 14	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
7		eqid 2139	. . . . . . . 8 ⊢ +∞ = +∞
8	7	biantru 300	. . . . . . 7 ⊢ (𝐴 = +∞ ↔ (𝐴 = +∞ ∧ +∞ = +∞))
9	8	a1i 9	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (𝐴 = +∞ ↔ (𝐴 = +∞ ∧ +∞ = +∞)))
10		xrmnfdc 9629	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ* → DECID 𝐴 = -∞)
11	10	ad2antrr 479	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → DECID 𝐴 = -∞)
12		exmiddc 821	. . . . . . . . . 10 ⊢ (DECID 𝐴 = -∞ → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
13	11, 12	syl 14	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
14		iba 298	. . . . . . . . . . . 12 ⊢ (+∞ = 𝐵 → (𝐴 = -∞ ↔ (𝐴 = -∞ ∧ +∞ = 𝐵)))
15	14	eqcoms 2142	. . . . . . . . . . 11 ⊢ (𝐵 = +∞ → (𝐴 = -∞ ↔ (𝐴 = -∞ ∧ +∞ = 𝐵)))
16	15	adantl 275	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (𝐴 = -∞ ↔ (𝐴 = -∞ ∧ +∞ = 𝐵)))
17	1	iftrued 3481	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))) = +∞)
18	17	eqcomd 2145	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))
19	18	biantrud 302	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (¬ 𝐴 = -∞ ↔ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
20	16, 19	orbi12d 782	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → ((𝐴 = -∞ ∨ ¬ 𝐴 = -∞) ↔ ((𝐴 = -∞ ∧ +∞ = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
21	13, 20	mpbid 146	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → ((𝐴 = -∞ ∧ +∞ = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
22		eqifdc 3506	. . . . . . . . 9 ⊢ (DECID 𝐴 = -∞ → (+∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) ↔ ((𝐴 = -∞ ∧ +∞ = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
23	11, 22	syl 14	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (+∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) ↔ ((𝐴 = -∞ ∧ +∞ = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ +∞ = if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
24	21, 23	mpbird 166	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
25	24	biantrud 302	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (¬ 𝐴 = +∞ ↔ (¬ 𝐴 = +∞ ∧ +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
26	9, 25	orbi12d 782	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → ((𝐴 = +∞ ∨ ¬ 𝐴 = +∞) ↔ ((𝐴 = +∞ ∧ +∞ = +∞) ∨ (¬ 𝐴 = +∞ ∧ +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))))
27	6, 26	mpbid 146	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → ((𝐴 = +∞ ∧ +∞ = +∞) ∨ (¬ 𝐴 = +∞ ∧ +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))))
28		eqifdc 3506	. . . . 5 ⊢ (DECID 𝐴 = +∞ → (+∞ = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))) ↔ ((𝐴 = +∞ ∧ +∞ = +∞) ∨ (¬ 𝐴 = +∞ ∧ +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))))
29	4, 28	syl 14	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → (+∞ = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))) ↔ ((𝐴 = +∞ ∧ +∞ = +∞) ∨ (¬ 𝐴 = +∞ ∧ +∞ = if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))))
30	27, 29	mpbird 166	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → +∞ = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
31	2, 30	eqtrd 2172	. 2 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
32	3, 5	syl 14	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
33	32	ad3antrrr 483	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
34		pm4.24 392	. . . . . . . . 9 ⊢ (𝐴 = +∞ ↔ (𝐴 = +∞ ∧ 𝐴 = +∞))
35	34	a1i 9	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = +∞ ↔ (𝐴 = +∞ ∧ 𝐴 = +∞)))
36	10	ad3antrrr 483	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → DECID 𝐴 = -∞)
37	36, 12	syl 14	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
38		simpr 109	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐵 = -∞)
39	38	eqeq2d 2151	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = 𝐵 ↔ 𝐴 = -∞))
40	39	anbi2d 459	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ↔ (𝐴 = -∞ ∧ 𝐴 = -∞)))
41		anidm 393	. . . . . . . . . . . . 13 ⊢ ((𝐴 = -∞ ∧ 𝐴 = -∞) ↔ 𝐴 = -∞)
42	40, 41	syl6rbb 196	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = -∞ ↔ (𝐴 = -∞ ∧ 𝐴 = 𝐵)))
43		eqid 2139	. . . . . . . . . . . . . 14 ⊢ 𝐴 = 𝐴
44	43	biantru 300	. . . . . . . . . . . . 13 ⊢ (¬ 𝐴 = -∞ ↔ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴))
45	44	a1i 9	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (¬ 𝐴 = -∞ ↔ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴)))
46	42, 45	orbi12d 782	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = -∞ ∨ ¬ 𝐴 = -∞) ↔ ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴))))
47	37, 46	mpbid 146	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴)))
48		eqifdc 3506	. . . . . . . . . . 11 ⊢ (DECID 𝐴 = -∞ → (𝐴 = if(𝐴 = -∞, 𝐵, 𝐴) ↔ ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴))))
49	36, 48	syl 14	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = if(𝐴 = -∞, 𝐵, 𝐴) ↔ ((𝐴 = -∞ ∧ 𝐴 = 𝐵) ∨ (¬ 𝐴 = -∞ ∧ 𝐴 = 𝐴))))
50	47, 49	mpbird 166	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴))
51	50	biantrud 302	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (¬ 𝐴 = +∞ ↔ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴))))
52	35, 51	orbi12d 782	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = +∞ ∨ ¬ 𝐴 = +∞) ↔ ((𝐴 = +∞ ∧ 𝐴 = +∞) ∨ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴)))))
53	33, 52	mpbid 146	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ((𝐴 = +∞ ∧ 𝐴 = +∞) ∨ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴))))
54	3	ad3antrrr 483	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → DECID 𝐴 = +∞)
55		eqifdc 3506	. . . . . . 7 ⊢ (DECID 𝐴 = +∞ → (𝐴 = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, 𝐴)) ↔ ((𝐴 = +∞ ∧ 𝐴 = +∞) ∨ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴)))))
56	54, 55	syl 14	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → (𝐴 = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, 𝐴)) ↔ ((𝐴 = +∞ ∧ 𝐴 = +∞) ∨ (¬ 𝐴 = +∞ ∧ 𝐴 = if(𝐴 = -∞, 𝐵, 𝐴)))))
57	53, 56	mpbird 166	. . . . 5 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐴 = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, 𝐴)))
58	38	iftrued 3481	. . . . 5 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = 𝐴)
59	38	iftrued 3481	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )) = 𝐴)
60	59	ifeq2d 3490	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐴 = -∞, 𝐵, 𝐴))
61	60	ifeq2d 3490	. . . . 5 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, 𝐴)))
62	57, 58, 61	3eqtr4d 2182	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
63		simpr 109	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → ¬ 𝐵 = -∞)
64	63	iffalsed 3484	. . . . 5 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
65	63	iffalsed 3484	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )) = sup({𝐵, 𝐴}, ℝ, < ))
66	65	ifeq2d 3490	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < )))
67	66	ifeq2d 3490	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < ))))
68		maxcom 10978	. . . . . . 7 ⊢ sup({𝐵, 𝐴}, ℝ, < ) = sup({𝐴, 𝐵}, ℝ, < )
69		ifeq2 3478	. . . . . . 7 ⊢ (sup({𝐵, 𝐴}, ℝ, < ) = sup({𝐴, 𝐵}, ℝ, < ) → if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < )) = if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))
70		ifeq2 3478	. . . . . . 7 ⊢ (if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < )) = if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
71	68, 69, 70	mp2b 8	. . . . . 6 ⊢ if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))
72	67, 71	syl6eq 2188	. . . . 5 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
73	64, 72	eqtr4d 2175	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
74		xrmnfdc 9629	. . . . . 6 ⊢ (𝐵 ∈ ℝ* → DECID 𝐵 = -∞)
75		exmiddc 821	. . . . . 6 ⊢ (DECID 𝐵 = -∞ → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
76	74, 75	syl 14	. . . . 5 ⊢ (𝐵 ∈ ℝ* → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
77	76	ad2antlr 480	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
78	62, 73, 77	mpjaodan 787	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
79		simpr 109	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → ¬ 𝐵 = +∞)
80	79	iffalsed 3484	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))))
81	79	iffalsed 3484	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))) = if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))
82	81	ifeq2d 3490	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))) = if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))
83	82	ifeq2d 3490	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < )))))
84	78, 80, 83	3eqtr4d 2182	. 2 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))
85		xrpnfdc 9628	. . . 4 ⊢ (𝐵 ∈ ℝ* → DECID 𝐵 = +∞)
86		exmiddc 821	. . . 4 ⊢ (DECID 𝐵 = +∞ → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
87	85, 86	syl 14	. . 3 ⊢ (𝐵 ∈ ℝ* → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
88	87	adantl 275	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
89	31, 84, 88	mpjaodan 787	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, sup({𝐵, 𝐴}, ℝ, < ))))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697  DECID wdc 819   = wceq 1331   ∈ wcel 1480  ifcif 3474  {cpr 3528  supcsup 6869  ℝcr 7622  +∞cpnf 7800  -∞cmnf 7801  ℝ^*cxr 7802   < clt 7803

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-un 4355  ax-setind 4452  ax-cnex 7714  ax-resscn 7715

This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-rab 2425  df-v 2688  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-uni 3737  df-sup 6871  df-pnf 7805  df-mnf 7806  df-xr 7807

This theorem is referenced by:  xrmaxiflemval  11022