Definition df-sup

Description: Define the supremum of class A . It is meaningful when R is a relation that strictly orders B and when the supremum exists. For example, R could be 'less than', B could be the set of real numbers, and A 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 . See dfsup2 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2		cR	⊢ 𝑅
3	0 1 2	csup	⊢ sup ( 𝐴 , 𝐵 , 𝑅 )
4		vx	⊢ 𝑥
5		vy	⊢ 𝑦
6	4	cv	⊢ 𝑥
7	5	cv	⊢ 𝑦
8	6 7 2	wbr	⊢ 𝑥 𝑅 𝑦
9	8	wn	⊢ ¬ 𝑥 𝑅 𝑦
10	9 5 0	wral	⊢ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦
11	7 6 2	wbr	⊢ 𝑦 𝑅 𝑥
12		vz	⊢ 𝑧
13	12	cv	⊢ 𝑧
14	7 13 2	wbr	⊢ 𝑦 𝑅 𝑧
15	14 12 0	wrex	⊢ ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧
16	11 15	wi	⊢ ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 )
17	16 5 1	wral	⊢ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 )
18	10 17	wa	⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) )
19	18 4 1	crab	⊢ { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) }
20	19	cuni	⊢ ∪ { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) }
21	3 20	wceq	⊢ sup ( 𝐴 , 𝐵 , 𝑅 ) = ∪ { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) }