Step | Hyp | Ref
| Expression |
1 | | cadds 33886 |
. 2
class
+s |
2 | | vx |
. . . 4
setvar 𝑥 |
3 | | va |
. . . 4
setvar 𝑎 |
4 | | cvv 3423 |
. . . 4
class
V |
5 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
6 | 5 | cv 1542 |
. . . . . . . . 9
class 𝑦 |
7 | | vl |
. . . . . . . . . . 11
setvar 𝑙 |
8 | 7 | cv 1542 |
. . . . . . . . . 10
class 𝑙 |
9 | 2 | cv 1542 |
. . . . . . . . . . 11
class 𝑥 |
10 | | c2nd 7781 |
. . . . . . . . . . 11
class
2^{nd} |
11 | 9, 10 | cfv 6400 |
. . . . . . . . . 10
class
(2^{nd} ‘𝑥) |
12 | 3 | cv 1542 |
. . . . . . . . . 10
class 𝑎 |
13 | 8, 11, 12 | co 7234 |
. . . . . . . . 9
class (𝑙𝑎(2^{nd} ‘𝑥)) |
14 | 6, 13 | wceq 1543 |
. . . . . . . 8
wff 𝑦 = (𝑙𝑎(2^{nd} ‘𝑥)) |
15 | | c1st 7780 |
. . . . . . . . . 10
class
1^{st} |
16 | 9, 15 | cfv 6400 |
. . . . . . . . 9
class
(1^{st} ‘𝑥) |
17 | | cleft 33799 |
. . . . . . . . 9
class
L |
18 | 16, 17 | cfv 6400 |
. . . . . . . 8
class ( L
‘(1^{st} ‘𝑥)) |
19 | 14, 7, 18 | wrex 3065 |
. . . . . . 7
wff
∃𝑙 ∈ ( L
‘(1^{st} ‘𝑥))𝑦 = (𝑙𝑎(2^{nd} ‘𝑥)) |
20 | 19, 5 | cab 2716 |
. . . . . 6
class {𝑦 ∣ ∃𝑙 ∈ ( L
‘(1^{st} ‘𝑥))𝑦 = (𝑙𝑎(2^{nd} ‘𝑥))} |
21 | | vz |
. . . . . . . . . 10
setvar 𝑧 |
22 | 21 | cv 1542 |
. . . . . . . . 9
class 𝑧 |
23 | 16, 8, 12 | co 7234 |
. . . . . . . . 9
class
((1^{st} ‘𝑥)𝑎𝑙) |
24 | 22, 23 | wceq 1543 |
. . . . . . . 8
wff 𝑧 = ((1^{st} ‘𝑥)𝑎𝑙) |
25 | 11, 17 | cfv 6400 |
. . . . . . . 8
class ( L
‘(2^{nd} ‘𝑥)) |
26 | 24, 7, 25 | wrex 3065 |
. . . . . . 7
wff
∃𝑙 ∈ ( L
‘(2^{nd} ‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑙) |
27 | 26, 21 | cab 2716 |
. . . . . 6
class {𝑧 ∣ ∃𝑙 ∈ ( L
‘(2^{nd} ‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑙)} |
28 | 20, 27 | cun 3881 |
. . . . 5
class ({𝑦 ∣ ∃𝑙 ∈ ( L
‘(1^{st} ‘𝑥))𝑦 = (𝑙𝑎(2^{nd} ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2^{nd}
‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑙)}) |
29 | | vr |
. . . . . . . . . . 11
setvar 𝑟 |
30 | 29 | cv 1542 |
. . . . . . . . . 10
class 𝑟 |
31 | 30, 11, 12 | co 7234 |
. . . . . . . . 9
class (𝑟𝑎(2^{nd} ‘𝑥)) |
32 | 6, 31 | wceq 1543 |
. . . . . . . 8
wff 𝑦 = (𝑟𝑎(2^{nd} ‘𝑥)) |
33 | | cright 33800 |
. . . . . . . . 9
class
R |
34 | 16, 33 | cfv 6400 |
. . . . . . . 8
class ( R
‘(1^{st} ‘𝑥)) |
35 | 32, 29, 34 | wrex 3065 |
. . . . . . 7
wff
∃𝑟 ∈ ( R
‘(1^{st} ‘𝑥))𝑦 = (𝑟𝑎(2^{nd} ‘𝑥)) |
36 | 35, 5 | cab 2716 |
. . . . . 6
class {𝑦 ∣ ∃𝑟 ∈ ( R
‘(1^{st} ‘𝑥))𝑦 = (𝑟𝑎(2^{nd} ‘𝑥))} |
37 | 16, 30, 12 | co 7234 |
. . . . . . . . 9
class
((1^{st} ‘𝑥)𝑎𝑟) |
38 | 22, 37 | wceq 1543 |
. . . . . . . 8
wff 𝑧 = ((1^{st} ‘𝑥)𝑎𝑟) |
39 | 11, 33 | cfv 6400 |
. . . . . . . 8
class ( R
‘(2^{nd} ‘𝑥)) |
40 | 38, 29, 39 | wrex 3065 |
. . . . . . 7
wff
∃𝑟 ∈ ( R
‘(2^{nd} ‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑟) |
41 | 40, 21 | cab 2716 |
. . . . . 6
class {𝑧 ∣ ∃𝑟 ∈ ( R
‘(2^{nd} ‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑟)} |
42 | 36, 41 | cun 3881 |
. . . . 5
class ({𝑦 ∣ ∃𝑟 ∈ ( R
‘(1^{st} ‘𝑥))𝑦 = (𝑟𝑎(2^{nd} ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2^{nd}
‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑟)}) |
43 | | cscut 33747 |
. . . . 5
class
|s |
44 | 28, 42, 43 | co 7234 |
. . . 4
class (({𝑦 ∣ ∃𝑙 ∈ ( L
‘(1^{st} ‘𝑥))𝑦 = (𝑙𝑎(2^{nd} ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2^{nd}
‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1^{st}
‘𝑥))𝑦 = (𝑟𝑎(2^{nd} ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2^{nd}
‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑟)})) |
45 | 2, 3, 4, 4, 44 | cmpo 7236 |
. . 3
class (𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1^{st}
‘𝑥))𝑦 = (𝑙𝑎(2^{nd} ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2^{nd}
‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1^{st}
‘𝑥))𝑦 = (𝑟𝑎(2^{nd} ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2^{nd}
‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑟)}))) |
46 | 45 | cnorec2 33875 |
. 2
class norec2
((𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L
‘(1^{st} ‘𝑥))𝑦 = (𝑙𝑎(2^{nd} ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2^{nd}
‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1^{st}
‘𝑥))𝑦 = (𝑟𝑎(2^{nd} ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2^{nd}
‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑟)})))) |
47 | 1, 46 | wceq 1543 |
1
wff +s =
norec2 ((𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L
‘(1^{st} ‘𝑥))𝑦 = (𝑙𝑎(2^{nd} ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2^{nd}
‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1^{st}
‘𝑥))𝑦 = (𝑟𝑎(2^{nd} ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2^{nd}
‘𝑥))𝑧 = ((1^{st} ‘𝑥)𝑎𝑟)})))) |