Step |
Hyp |
Ref |
Expression |
0 |
|
csslt |
⊢ <<s |
1 |
|
va |
⊢ 𝑎 |
2 |
|
vb |
⊢ 𝑏 |
3 |
1
|
cv |
⊢ 𝑎 |
4 |
|
csur |
⊢ No |
5 |
3 4
|
wss |
⊢ 𝑎 ⊆ No |
6 |
2
|
cv |
⊢ 𝑏 |
7 |
6 4
|
wss |
⊢ 𝑏 ⊆ No |
8 |
|
vx |
⊢ 𝑥 |
9 |
|
vy |
⊢ 𝑦 |
10 |
8
|
cv |
⊢ 𝑥 |
11 |
|
cslt |
⊢ <s |
12 |
9
|
cv |
⊢ 𝑦 |
13 |
10 12 11
|
wbr |
⊢ 𝑥 <s 𝑦 |
14 |
13 9 6
|
wral |
⊢ ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 |
15 |
14 8 3
|
wral |
⊢ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 |
16 |
5 7 15
|
w3a |
⊢ ( 𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ) |
17 |
16 1 2
|
copab |
⊢ { 〈 𝑎 , 𝑏 〉 ∣ ( 𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ) } |
18 |
0 17
|
wceq |
⊢ <<s = { 〈 𝑎 , 𝑏 〉 ∣ ( 𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ) } |