Step | Hyp | Ref
| Expression |
1 | | cnadd 33587 |
. 2
class
+no |
2 | | con0 6231 |
. . . 4
class
On |
3 | 2, 2 | cxp 5564 |
. . 3
class (On
× On) |
4 | | vx |
. . . . . . 7
setvar 𝑥 |
5 | 4 | cv 1542 |
. . . . . 6
class 𝑥 |
6 | 5, 3 | wcel 2111 |
. . . . 5
wff 𝑥 ∈ (On ×
On) |
7 | | vy |
. . . . . . 7
setvar 𝑦 |
8 | 7 | cv 1542 |
. . . . . 6
class 𝑦 |
9 | 8, 3 | wcel 2111 |
. . . . 5
wff 𝑦 ∈ (On ×
On) |
10 | | c1st 7778 |
. . . . . . . . 9
class
1^{st} |
11 | 5, 10 | cfv 6398 |
. . . . . . . 8
class
(1^{st} ‘𝑥) |
12 | 8, 10 | cfv 6398 |
. . . . . . . 8
class
(1^{st} ‘𝑦) |
13 | | cep 5474 |
. . . . . . . 8
class
E |
14 | 11, 12, 13 | wbr 5068 |
. . . . . . 7
wff
(1^{st} ‘𝑥) E (1^{st} ‘𝑦) |
15 | 11, 12 | wceq 1543 |
. . . . . . 7
wff
(1^{st} ‘𝑥) = (1^{st} ‘𝑦) |
16 | 14, 15 | wo 847 |
. . . . . 6
wff
((1^{st} ‘𝑥) E (1^{st} ‘𝑦) ∨ (1^{st} ‘𝑥) = (1^{st} ‘𝑦)) |
17 | | c2nd 7779 |
. . . . . . . . 9
class
2^{nd} |
18 | 5, 17 | cfv 6398 |
. . . . . . . 8
class
(2^{nd} ‘𝑥) |
19 | 8, 17 | cfv 6398 |
. . . . . . . 8
class
(2^{nd} ‘𝑦) |
20 | 18, 19, 13 | wbr 5068 |
. . . . . . 7
wff
(2^{nd} ‘𝑥) E (2^{nd} ‘𝑦) |
21 | 18, 19 | wceq 1543 |
. . . . . . 7
wff
(2^{nd} ‘𝑥) = (2^{nd} ‘𝑦) |
22 | 20, 21 | wo 847 |
. . . . . 6
wff
((2^{nd} ‘𝑥) E (2^{nd} ‘𝑦) ∨ (2^{nd} ‘𝑥) = (2^{nd} ‘𝑦)) |
23 | 5, 8 | wne 2941 |
. . . . . 6
wff 𝑥 ≠ 𝑦 |
24 | 16, 22, 23 | w3a 1089 |
. . . . 5
wff
(((1^{st} ‘𝑥) E (1^{st} ‘𝑦) ∨ (1^{st} ‘𝑥) = (1^{st} ‘𝑦)) ∧ ((2^{nd}
‘𝑥) E (2^{nd}
‘𝑦) ∨
(2^{nd} ‘𝑥) =
(2^{nd} ‘𝑦))
∧ 𝑥 ≠ 𝑦) |
25 | 6, 9, 24 | w3a 1089 |
. . . 4
wff (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1^{st} ‘𝑥) E (1^{st} ‘𝑦) ∨ (1^{st} ‘𝑥) = (1^{st} ‘𝑦)) ∧ ((2^{nd}
‘𝑥) E (2^{nd}
‘𝑦) ∨
(2^{nd} ‘𝑥) =
(2^{nd} ‘𝑦))
∧ 𝑥 ≠ 𝑦)) |
26 | 25, 4, 7 | copab 5130 |
. . 3
class
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1^{st} ‘𝑥) E (1^{st} ‘𝑦) ∨ (1^{st} ‘𝑥) = (1^{st} ‘𝑦)) ∧ ((2^{nd}
‘𝑥) E (2^{nd}
‘𝑦) ∨
(2^{nd} ‘𝑥) =
(2^{nd} ‘𝑦))
∧ 𝑥 ≠ 𝑦))} |
27 | | vz |
. . . 4
setvar 𝑧 |
28 | | va |
. . . 4
setvar 𝑎 |
29 | | cvv 3421 |
. . . 4
class
V |
30 | 28 | cv 1542 |
. . . . . . . . 9
class 𝑎 |
31 | 27 | cv 1542 |
. . . . . . . . . . . 12
class 𝑧 |
32 | 31, 10 | cfv 6398 |
. . . . . . . . . . 11
class
(1^{st} ‘𝑧) |
33 | 32 | csn 4556 |
. . . . . . . . . 10
class
{(1^{st} ‘𝑧)} |
34 | 31, 17 | cfv 6398 |
. . . . . . . . . 10
class
(2^{nd} ‘𝑧) |
35 | 33, 34 | cxp 5564 |
. . . . . . . . 9
class
({(1^{st} ‘𝑧)} × (2^{nd} ‘𝑧)) |
36 | 30, 35 | cima 5569 |
. . . . . . . 8
class (𝑎 “ ({(1^{st}
‘𝑧)} ×
(2^{nd} ‘𝑧))) |
37 | | vw |
. . . . . . . . 9
setvar 𝑤 |
38 | 37 | cv 1542 |
. . . . . . . 8
class 𝑤 |
39 | 36, 38 | wss 3881 |
. . . . . . 7
wff (𝑎 “ ({(1^{st}
‘𝑧)} ×
(2^{nd} ‘𝑧)))
⊆ 𝑤 |
40 | 34 | csn 4556 |
. . . . . . . . . 10
class
{(2^{nd} ‘𝑧)} |
41 | 32, 40 | cxp 5564 |
. . . . . . . . 9
class
((1^{st} ‘𝑧) × {(2^{nd} ‘𝑧)}) |
42 | 30, 41 | cima 5569 |
. . . . . . . 8
class (𝑎 “ ((1^{st}
‘𝑧) ×
{(2^{nd} ‘𝑧)})) |
43 | 42, 38 | wss 3881 |
. . . . . . 7
wff (𝑎 “ ((1^{st}
‘𝑧) ×
{(2^{nd} ‘𝑧)})) ⊆ 𝑤 |
44 | 39, 43 | wa 399 |
. . . . . 6
wff ((𝑎 “ ({(1^{st}
‘𝑧)} ×
(2^{nd} ‘𝑧)))
⊆ 𝑤 ∧ (𝑎 “ ((1^{st}
‘𝑧) ×
{(2^{nd} ‘𝑧)})) ⊆ 𝑤) |
45 | 44, 37, 2 | crab 3066 |
. . . . 5
class {𝑤 ∈ On ∣ ((𝑎 “ ({(1^{st}
‘𝑧)} ×
(2^{nd} ‘𝑧)))
⊆ 𝑤 ∧ (𝑎 “ ((1^{st}
‘𝑧) ×
{(2^{nd} ‘𝑧)})) ⊆ 𝑤)} |
46 | 45 | cint 4874 |
. . . 4
class ∩ {𝑤
∈ On ∣ ((𝑎
“ ({(1^{st} ‘𝑧)} × (2^{nd} ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1^{st} ‘𝑧) × {(2^{nd}
‘𝑧)})) ⊆ 𝑤)} |
47 | 27, 28, 29, 29, 46 | cmpo 7234 |
. . 3
class (𝑧 ∈ V, 𝑎 ∈ V ↦ ∩ {𝑤
∈ On ∣ ((𝑎
“ ({(1^{st} ‘𝑧)} × (2^{nd} ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1^{st} ‘𝑧) × {(2^{nd}
‘𝑧)})) ⊆ 𝑤)}) |
48 | 3, 26, 47 | cfrecs 8043 |
. 2
class
frecs({⟨𝑥,
𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1^{st} ‘𝑥) E (1^{st} ‘𝑦) ∨ (1^{st} ‘𝑥) = (1^{st} ‘𝑦)) ∧ ((2^{nd}
‘𝑥) E (2^{nd}
‘𝑦) ∨
(2^{nd} ‘𝑥) =
(2^{nd} ‘𝑦))
∧ 𝑥 ≠ 𝑦))}, (On × On), (𝑧 ∈ V, 𝑎 ∈ V ↦ ∩ {𝑤
∈ On ∣ ((𝑎
“ ({(1^{st} ‘𝑧)} × (2^{nd} ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1^{st} ‘𝑧) × {(2^{nd}
‘𝑧)})) ⊆ 𝑤)})) |
49 | 1, 48 | wceq 1543 |
1
wff +no =
frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1^{st} ‘𝑥) E (1^{st} ‘𝑦) ∨ (1^{st} ‘𝑥) = (1^{st} ‘𝑦)) ∧ ((2^{nd}
‘𝑥) E (2^{nd}
‘𝑦) ∨
(2^{nd} ‘𝑥) =
(2^{nd} ‘𝑦))
∧ 𝑥 ≠ 𝑦))}, (On × On), (𝑧 ∈ V, 𝑎 ∈ V ↦ ∩ {𝑤
∈ On ∣ ((𝑎
“ ({(1^{st} ‘𝑧)} × (2^{nd} ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1^{st} ‘𝑧) × {(2^{nd}
‘𝑧)})) ⊆ 𝑤)})) |