Definition df-sup 9458

Description: Define the supremum of class 𝐴. It is meaningful when 𝑅 is a relation that strictly orders 𝐵 and when the supremum exists. For example, 𝑅 could be 'less than', 𝐵 could be the set of real numbers, and 𝐴 could be the set of all positive reals whose square is less than 2; in this case the supremum is defined as the square root of 2 per sqrtval 15430. See dfsup2 9460 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999.)

Assertion

Ref	Expression
df-sup	⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))}

Distinct variable groups:   𝑥,𝑦,𝑧,𝑅   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧

Detailed syntax breakdown of Definition df-sup

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cR	. . 3 class 𝑅
4	1, 2, 3	csup 9456	. 2 class sup(𝐴, 𝐵, 𝑅)
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1569	. . . . . . . 8 class 𝑥
7		vy	. . . . . . . . 9 setvar 𝑦
8	7	cv 1569	. . . . . . . 8 class 𝑦
9	6, 8, 3	wbr 5106	. . . . . . 7 wff 𝑥𝑅𝑦
10	9	wn 3	. . . . . 6 wff ¬ 𝑥𝑅𝑦
11	10, 7, 1	wral 3080	. . . . 5 wff ∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦
12	8, 6, 3	wbr 5106	. . . . . . 7 wff 𝑦𝑅𝑥
13		vz	. . . . . . . . . 10 setvar 𝑧
14	13	cv 1569	. . . . . . . . 9 class 𝑧
15	8, 14, 3	wbr 5106	. . . . . . . 8 wff 𝑦𝑅𝑧
16	15, 13, 1	wrex 3090	. . . . . . 7 wff ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧
17	12, 16	wi 4	. . . . . 6 wff (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧)
18	17, 7, 2	wral 3080	. . . . 5 wff ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧)
19	11, 18	wa 401	. . . 4 wff (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))
20	19, 5, 2	crab 3416	. . 3 class {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))}
21	20	cuni 4870	. 2 class ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))}
22	4, 21	wceq 1570	1 wff sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))}

This definition is used by:  dfsup2  9460  supeq1  9461  supeq2  9464  supeq3  9465  supeq123d  9466  supexd  9469  supval2  9471  sup00  9481  dfinfre  12322  prdsds  17661  supex2g  38862