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