This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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