Metamath Proof Explorer


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 ( 𝐴 , 𝐵 , 𝑅 ) = { 𝑥𝐵 ∣ ( ∀ 𝑦𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐴 𝑦 𝑅 𝑧 ) ) }