Step | Hyp | Ref
| Expression |
1 | | cF |
. . 3
class 𝐹 |
2 | 1 | cnorec2 33868 |
. 2
class norec2
(𝐹) |
3 | | csur 33606 |
. . . 4
class No |
4 | 3, 3 | cxp 5564 |
. . 3
class ( No × No
) |
5 | | va |
. . . . . . 7
setvar 𝑎 |
6 | 5 | cv 1542 |
. . . . . 6
class 𝑎 |
7 | 6, 4 | wcel 2111 |
. . . . 5
wff 𝑎 ∈ (
No × No ) |
8 | | vb |
. . . . . . 7
setvar 𝑏 |
9 | 8 | cv 1542 |
. . . . . 6
class 𝑏 |
10 | 9, 4 | wcel 2111 |
. . . . 5
wff 𝑏 ∈ (
No × No ) |
11 | | c1st 7778 |
. . . . . . . . 9
class
1^{st} |
12 | 6, 11 | cfv 6398 |
. . . . . . . 8
class
(1^{st} ‘𝑎) |
13 | 9, 11 | cfv 6398 |
. . . . . . . 8
class
(1^{st} ‘𝑏) |
14 | | vc |
. . . . . . . . . . 11
setvar 𝑐 |
15 | 14 | cv 1542 |
. . . . . . . . . 10
class 𝑐 |
16 | | vd |
. . . . . . . . . . . . 13
setvar 𝑑 |
17 | 16 | cv 1542 |
. . . . . . . . . . . 12
class 𝑑 |
18 | | cleft 33792 |
. . . . . . . . . . . 12
class
L |
19 | 17, 18 | cfv 6398 |
. . . . . . . . . . 11
class ( L
‘𝑑) |
20 | | cright 33793 |
. . . . . . . . . . . 12
class
R |
21 | 17, 20 | cfv 6398 |
. . . . . . . . . . 11
class ( R
‘𝑑) |
22 | 19, 21 | cun 3879 |
. . . . . . . . . 10
class (( L
‘𝑑) ∪ ( R
‘𝑑)) |
23 | 15, 22 | wcel 2111 |
. . . . . . . . 9
wff 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑)) |
24 | 23, 14, 16 | copab 5130 |
. . . . . . . 8
class
{⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} |
25 | 12, 13, 24 | wbr 5068 |
. . . . . . 7
wff
(1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) |
26 | 12, 13 | wceq 1543 |
. . . . . . 7
wff
(1^{st} ‘𝑎) = (1^{st} ‘𝑏) |
27 | 25, 26 | wo 847 |
. . . . . 6
wff
((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) |
28 | | c2nd 7779 |
. . . . . . . . 9
class
2^{nd} |
29 | 6, 28 | cfv 6398 |
. . . . . . . 8
class
(2^{nd} ‘𝑎) |
30 | 9, 28 | cfv 6398 |
. . . . . . . 8
class
(2^{nd} ‘𝑏) |
31 | 29, 30, 24 | wbr 5068 |
. . . . . . 7
wff
(2^{nd} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) |
32 | 29, 30 | wceq 1543 |
. . . . . . 7
wff
(2^{nd} ‘𝑎) = (2^{nd} ‘𝑏) |
33 | 31, 32 | wo 847 |
. . . . . 6
wff
((2^{nd} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) |
34 | 6, 9 | wne 2941 |
. . . . . 6
wff 𝑎 ≠ 𝑏 |
35 | 27, 33, 34 | w3a 1089 |
. . . . 5
wff
(((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏) |
36 | 7, 10, 35 | w3a 1089 |
. . . 4
wff (𝑎 ∈ (
No × No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏)) |
37 | 36, 5, 8 | copab 5130 |
. . 3
class
{⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (
No × No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} |
38 | 4, 37, 1 | cfrecs 8043 |
. 2
class
frecs({⟨𝑎,
𝑏⟩ ∣ (𝑎 ∈ (
No × No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No
× No ), 𝐹) |
39 | 2, 38 | wceq 1543 |
1
wff norec2
(𝐹) = frecs({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No
× No ), 𝐹) |