xrmaxifle - Intuitionistic Logic Explorer

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

Theorem xrmaxifle 11286

Description: An upper bound for {𝐴, 𝐵} in the extended reals. (Contributed by Jim Kingdon, 26-Apr-2023.)

**Assertion**
Ref	Expression
xrmaxifle	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → 𝐴 ≤ if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))))

**Proof of Theorem xrmaxifle**
Step	Hyp	Ref	Expression
1		pnfge 9819	. . . 4 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ +∞)
2	1	ad2antrr 488	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐵 = +∞) → 𝐴 ≤ +∞)
3		simpr 110	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐵 = +∞) → 𝐵 = +∞)
4	3	iftrued 3556	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = +∞)
5	2, 4	breqtrrd 4046	. 2 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐵 = +∞) → 𝐴 ≤ if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))))
6		xrleid 9830	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ 𝐴)
7	6	ad3antrrr 492	. . . . 5 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐴 ≤ 𝐴)
8		simpr 110	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐵 = -∞)
9	8	iftrued 3556	. . . . 5 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = 𝐴)
10	7, 9	breqtrrd 4046	. . . 4 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐴 ≤ if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))))
11	1	ad4antr 494	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → 𝐴 ≤ +∞)
12		simpr 110	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → 𝐴 = +∞)
13	12	iftrued 3556	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = +∞)
14	11, 13	breqtrrd 4046	. . . . . 6 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → 𝐴 ≤ if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
15		mnfle 9822	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ^* → -∞ ≤ 𝐵)
16	15	ad5antlr 497	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ 𝐴 = -∞) → -∞ ≤ 𝐵)
17		simpr 110	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ 𝐴 = -∞) → 𝐴 = -∞)
18	17	iftrued 3556	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ 𝐴 = -∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = 𝐵)
19	16, 17, 18	3brtr4d 4050	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ 𝐴 = -∞) → 𝐴 ≤ if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))
20		simplr 528	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐴 = +∞)
21		simpr 110	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐴 = -∞)
22		elxr 9806	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
23	22	biimpi 120	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ^* → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
24	23	ad5antr 496	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
25	20, 21, 24	ecase23d 1361	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 ∈ ℝ)
26		simpr 110	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) → ¬ 𝐵 = +∞)
27	26	ad3antrrr 492	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐵 = +∞)
28		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → ¬ 𝐵 = -∞)
29	28	ad2antrr 488	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐵 = -∞)
30		elxr 9806	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
31	30	biimpi 120	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ^* → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
32	31	ad5antlr 497	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
33	27, 29, 32	ecase23d 1361	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐵 ∈ ℝ)
34		maxle1 11252	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ, < ))
35	25, 33, 34	syl2anc 411	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ, < ))
36	21	iffalsed 3559	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = sup({𝐴, 𝐵}, ℝ, < ))
37	35, 36	breqtrrd 4046	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 ≤ if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))
38		xrmnfdc 9873	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ^* → DECID 𝐴 = -∞)
39		exmiddc 837	. . . . . . . . . 10 ⊢ (DECID 𝐴 = -∞ → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
40	38, 39	syl 14	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ^* → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
41	40	ad4antr 494	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
42	19, 37, 41	mpjaodan 799	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → 𝐴 ≤ if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))
43		simpr 110	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → ¬ 𝐴 = +∞)
44	43	iffalsed 3559	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))
45	42, 44	breqtrrd 4046	. . . . . 6 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → 𝐴 ≤ if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
46		xrpnfdc 9872	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ^* → DECID 𝐴 = +∞)
47		exmiddc 837	. . . . . . . 8 ⊢ (DECID 𝐴 = +∞ → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
48	46, 47	syl 14	. . . . . . 7 ⊢ (𝐴 ∈ ℝ^* → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
49	48	ad3antrrr 492	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
50	14, 45, 49	mpjaodan 799	. . . . 5 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → 𝐴 ≤ if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
51	28	iffalsed 3559	. . . . 5 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
52	50, 51	breqtrrd 4046	. . . 4 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → 𝐴 ≤ if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))))
53		xrmnfdc 9873	. . . . . 6 ⊢ (𝐵 ∈ ℝ^* → DECID 𝐵 = -∞)
54		exmiddc 837	. . . . . 6 ⊢ (DECID 𝐵 = -∞ → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
55	53, 54	syl 14	. . . . 5 ⊢ (𝐵 ∈ ℝ^* → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
56	55	ad2antlr 489	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
57	10, 52, 56	mpjaodan 799	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) → 𝐴 ≤ if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))))
58	26	iffalsed 3559	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))))
59	57, 58	breqtrrd 4046	. 2 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐵 = +∞) → 𝐴 ≤ if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))))
60		xrpnfdc 9872	. . . 4 ⊢ (𝐵 ∈ ℝ^* → DECID 𝐵 = +∞)
61		exmiddc 837	. . . 4 ⊢ (DECID 𝐵 = +∞ → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
62	60, 61	syl 14	. . 3 ⊢ (𝐵 ∈ ℝ^* → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
63	62	adantl 277	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
64	5, 59, 63	mpjaodan 799	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → 𝐴 ≤ if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ∨ wo 709 DECID wdc 835 ∨ w3o 979 = wceq 1364 ∈ wcel 2160 ifcif 3549 {cpr 3608 class class class wbr 4018 supcsup 7011 ℝcr 7840 +∞cpnf 8019 -∞cmnf 8020 ℝ^*cxr 8021 < clt 8022 ≤ cle 8023

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 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4192 ax-pr 4227 ax-un 4451 ax-setind 4554 ax-iinf 4605 ax-cnex 7932 ax-resscn 7933 ax-1cn 7934 ax-1re 7935 ax-icn 7936 ax-addcl 7937 ax-addrcl 7938 ax-mulcl 7939 ax-mulrcl 7940 ax-addcom 7941 ax-mulcom 7942 ax-addass 7943 ax-mulass 7944 ax-distr 7945 ax-i2m1 7946 ax-0lt1 7947 ax-1rid 7948 ax-0id 7949 ax-rnegex 7950 ax-precex 7951 ax-cnre 7952 ax-pre-ltirr 7953 ax-pre-ltwlin 7954 ax-pre-lttrn 7955 ax-pre-apti 7956 ax-pre-ltadd 7957 ax-pre-mulgt0 7958 ax-pre-mulext 7959 ax-arch 7960 ax-caucvg 7961

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rmo 2476 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-if 3550 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4311 df-po 4314 df-iso 4315 df-iord 4384 df-on 4386 df-ilim 4387 df-suc 4389 df-iom 4608 df-xp 4650 df-rel 4651 df-cnv 4652 df-co 4653 df-dm 4654 df-rn 4655 df-res 4656 df-ima 4657 df-iota 5196 df-fun 5237 df-fn 5238 df-f 5239 df-f1 5240 df-fo 5241 df-f1o 5242 df-fv 5243 df-riota 5852 df-ov 5899 df-oprab 5900 df-mpo 5901 df-1st 6165 df-2nd 6166 df-recs 6330 df-frec 6416 df-sup 7013 df-pnf 8024 df-mnf 8025 df-xr 8026 df-ltxr 8027 df-le 8028 df-sub 8160 df-neg 8161 df-reap 8562 df-ap 8569 df-div 8660 df-inn 8950 df-2 9008 df-3 9009 df-4 9010 df-n0 9207 df-z 9284 df-uz 9559 df-rp 9684 df-seqfrec 10477 df-exp 10551 df-cj 10883 df-re 10884 df-im 10885 df-rsqrt 11039 df-abs 11040

This theorem is referenced by: xrmaxiflemval 11290 xrmax1sup 11293

W3C validator