Step | Hyp | Ref
| Expression |
1 | | cslt 27134 |
. 2
class
<s |
2 | | vf |
. . . . . . 7
setvar 𝑓 |
3 | 2 | cv 1541 |
. . . . . 6
class 𝑓 |
4 | | csur 27133 |
. . . . . 6
class No |
5 | 3, 4 | wcel 2107 |
. . . . 5
wff 𝑓 ∈
No |
6 | | vg |
. . . . . . 7
setvar 𝑔 |
7 | 6 | cv 1541 |
. . . . . 6
class 𝑔 |
8 | 7, 4 | wcel 2107 |
. . . . 5
wff 𝑔 ∈
No |
9 | 5, 8 | wa 397 |
. . . 4
wff (𝑓 ∈
No ∧ 𝑔 ∈
No ) |
10 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
11 | 10 | cv 1541 |
. . . . . . . . 9
class 𝑦 |
12 | 11, 3 | cfv 6541 |
. . . . . . . 8
class (𝑓‘𝑦) |
13 | 11, 7 | cfv 6541 |
. . . . . . . 8
class (𝑔‘𝑦) |
14 | 12, 13 | wceq 1542 |
. . . . . . 7
wff (𝑓‘𝑦) = (𝑔‘𝑦) |
15 | | vx |
. . . . . . . 8
setvar 𝑥 |
16 | 15 | cv 1541 |
. . . . . . 7
class 𝑥 |
17 | 14, 10, 16 | wral 3062 |
. . . . . 6
wff
∀𝑦 ∈
𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) |
18 | 16, 3 | cfv 6541 |
. . . . . . 7
class (𝑓‘𝑥) |
19 | 16, 7 | cfv 6541 |
. . . . . . 7
class (𝑔‘𝑥) |
20 | | c1o 8456 |
. . . . . . . . 9
class
1o |
21 | | c0 4322 |
. . . . . . . . 9
class
∅ |
22 | 20, 21 | cop 4634 |
. . . . . . . 8
class
⟨1o, ∅⟩ |
23 | | c2o 8457 |
. . . . . . . . 9
class
2o |
24 | 20, 23 | cop 4634 |
. . . . . . . 8
class
⟨1o, 2o⟩ |
25 | 21, 23 | cop 4634 |
. . . . . . . 8
class
⟨∅, 2o⟩ |
26 | 22, 24, 25 | ctp 4632 |
. . . . . . 7
class
{⟨1o, ∅⟩, ⟨1o,
2o⟩, ⟨∅, 2o⟩} |
27 | 18, 19, 26 | wbr 5148 |
. . . . . 6
wff (𝑓‘𝑥){⟨1o, ∅⟩,
⟨1o, 2o⟩, ⟨∅, 2o⟩}
(𝑔‘𝑥) |
28 | 17, 27 | wa 397 |
. . . . 5
wff
(∀𝑦 ∈
𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩,
⟨1o, 2o⟩, ⟨∅, 2o⟩}
(𝑔‘𝑥)) |
29 | | con0 6362 |
. . . . 5
class
On |
30 | 28, 15, 29 | wrex 3071 |
. . . 4
wff
∃𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩,
⟨1o, 2o⟩, ⟨∅, 2o⟩}
(𝑔‘𝑥)) |
31 | 9, 30 | wa 397 |
. . 3
wff ((𝑓 ∈
No ∧ 𝑔 ∈
No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩,
⟨1o, 2o⟩, ⟨∅, 2o⟩}
(𝑔‘𝑥))) |
32 | 31, 2, 6 | copab 5210 |
. 2
class
{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈
No ∧ 𝑔 ∈
No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩,
⟨1o, 2o⟩, ⟨∅, 2o⟩}
(𝑔‘𝑥)))} |
33 | 1, 32 | wceq 1542 |
1
wff <s =
{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈
No ∧ 𝑔 ∈
No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩,
⟨1o, 2o⟩, ⟨∅, 2o⟩}
(𝑔‘𝑥)))} |