Step | Hyp | Ref
| Expression |
1 | | peano1 7830 |
. . . 4
⊢ ∅
∈ ω |
2 | | elelsuc 6395 |
. . . 4
⊢ (∅
∈ ω → ∅ ∈ suc ω) |
3 | 1, 2 | mp1i 13 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ∅ ∈ suc
ω) |
4 | | satfv0.s |
. . . 4
⊢ 𝑆 = (𝑀 Sat 𝐸) |
5 | 4 | satfvsucom 33991 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ suc ω) →
(𝑆‘∅) =
(rec((𝑓 ∈ V ↦
(𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})‘∅)) |
6 | 3, 5 | mpd3an3 1463 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})‘∅)) |
7 | | goelel3xp 33982 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖∈𝑔𝑗) ∈ (ω ×
(ω × ω))) |
8 | | eleq1 2826 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑖∈𝑔𝑗) → (𝑥 ∈ (ω × (ω ×
ω)) ↔ (𝑖∈𝑔𝑗) ∈ (ω × (ω ×
ω)))) |
9 | 7, 8 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑥 = (𝑖∈𝑔𝑗) → 𝑥 ∈ (ω × (ω ×
ω)))) |
10 | 9 | adantrd 493 |
. . . . . . . 8
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑥 ∈ (ω × (ω ×
ω)))) |
11 | 10 | pm4.71d 563 |
. . . . . . 7
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω ×
ω))))) |
12 | 11 | 2rexbiia 3210 |
. . . . . 6
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω ×
ω)))) |
13 | | r19.41vv 3218 |
. . . . . 6
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω ×
ω))) ↔ (∃𝑖
∈ ω ∃𝑗
∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω ×
ω)))) |
14 | | ancom 462 |
. . . . . 6
⊢
((∃𝑖 ∈
ω ∃𝑗 ∈
ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω ×
ω))) ↔ (𝑥 ∈
(ω × (ω × ω)) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))) |
15 | 12, 13, 14 | 3bitri 297 |
. . . . 5
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ (𝑥 ∈ (ω × (ω ×
ω)) ∧ ∃𝑖
∈ ω ∃𝑗
∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))) |
16 | 15 | opabbii 5177 |
. . . 4
⊢
{⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (ω × (ω ×
ω)) ∧ ∃𝑖
∈ ω ∃𝑗
∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))} |
17 | | omex 9586 |
. . . . 5
⊢ ω
∈ V |
18 | 17, 17 | xpex 7692 |
. . . . 5
⊢ (ω
× ω) ∈ V |
19 | | xpexg 7689 |
. . . . . 6
⊢ ((ω
∈ V ∧ (ω × ω) ∈ V) → (ω ×
(ω × ω)) ∈ V) |
20 | | oveq1 7369 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑚 → (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑗)) |
21 | 20 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑚 → (𝑥 = (𝑖∈𝑔𝑗) ↔ 𝑥 = (𝑚∈𝑔𝑗))) |
22 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑚 → (𝑎‘𝑖) = (𝑎‘𝑚)) |
23 | 22 | breq1d 5120 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑚 → ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ↔ (𝑎‘𝑚)𝐸(𝑎‘𝑗))) |
24 | 23 | rabbidv 3418 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑚 → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)}) |
25 | 24 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑚 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)})) |
26 | 21, 25 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑚 → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ (𝑥 = (𝑚∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)}))) |
27 | | oveq2 7370 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑛 → (𝑚∈𝑔𝑗) = (𝑚∈𝑔𝑛)) |
28 | 27 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑛 → (𝑥 = (𝑚∈𝑔𝑗) ↔ 𝑥 = (𝑚∈𝑔𝑛))) |
29 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑛 → (𝑎‘𝑗) = (𝑎‘𝑛)) |
30 | 29 | breq2d 5122 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑛 → ((𝑎‘𝑚)𝐸(𝑎‘𝑗) ↔ (𝑎‘𝑚)𝐸(𝑎‘𝑛))) |
31 | 30 | rabbidv 3418 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑛 → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) |
32 | 31 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑛 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)})) |
33 | 28, 32 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑛 → ((𝑥 = (𝑚∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)}) ↔ (𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}))) |
34 | 26, 33 | cbvrex2vw 3231 |
. . . . . . . . . . 11
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)})) |
35 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑖∈𝑔𝑗) → (𝑥 = (𝑚∈𝑔𝑛) ↔ (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛))) |
36 | 35 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → (𝑥 = (𝑚∈𝑔𝑛) ↔ (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛))) |
37 | | goeleq12bg 33983 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛) ↔ (𝑖 = 𝑚 ∧ 𝑗 = 𝑛))) |
38 | 22 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = 𝑚 → (𝑎‘𝑚) = (𝑎‘𝑖)) |
39 | 29 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 𝑛 → (𝑎‘𝑛) = (𝑎‘𝑗)) |
40 | 38, 39 | breqan12d 5126 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑖 = 𝑚 ∧ 𝑗 = 𝑛) → ((𝑎‘𝑚)𝐸(𝑎‘𝑛) ↔ (𝑎‘𝑖)𝐸(𝑎‘𝑗))) |
41 | 40 | rabbidv 3418 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 = 𝑚 ∧ 𝑗 = 𝑛) → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) |
42 | 37, 41 | syl6bi 253 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛) → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) |
43 | 42 | imp 408 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛)) → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) |
44 | | eqeq12 2754 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (𝑦 = 𝑧 ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) |
45 | 43, 44 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛)) → ((𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑦 = 𝑧)) |
46 | 45 | exp4b 432 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → 𝑦 = 𝑧)))) |
47 | 46 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → ((𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → 𝑦 = 𝑧)))) |
48 | 36, 47 | sylbid 239 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → (𝑥 = (𝑚∈𝑔𝑛) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → 𝑦 = 𝑧)))) |
49 | 48 | impd 412 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → 𝑦 = 𝑧))) |
50 | 49 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → 𝑦 = 𝑧))) |
51 | 50 | expimpd 455 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → 𝑦 = 𝑧))) |
52 | 51 | rexlimdvva 3206 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) →
(∃𝑖 ∈ ω
∃𝑗 ∈ ω
(𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → 𝑦 = 𝑧))) |
53 | 52 | com23 86 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑦 = 𝑧))) |
54 | 53 | rexlimivv 3197 |
. . . . . . . . . . 11
⊢
(∃𝑚 ∈
ω ∃𝑛 ∈
ω (𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑦 = 𝑧)) |
55 | 34, 54 | sylbi 216 |
. . . . . . . . . 10
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑦 = 𝑧)) |
56 | 55 | imp 408 |
. . . . . . . . 9
⊢
((∃𝑖 ∈
ω ∃𝑗 ∈
ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → 𝑦 = 𝑧) |
57 | 56 | gen2 1799 |
. . . . . . . 8
⊢
∀𝑦∀𝑧((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → 𝑦 = 𝑧) |
58 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) |
59 | 58 | anbi2d 630 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))) |
60 | 59 | 2rexbidv 3214 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))) |
61 | 60 | mo4 2565 |
. . . . . . . 8
⊢
(∃*𝑦∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ∀𝑦∀𝑧((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → 𝑦 = 𝑧)) |
62 | 57, 61 | mpbir 230 |
. . . . . . 7
⊢
∃*𝑦∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) |
63 | | moabex 5421 |
. . . . . . 7
⊢
(∃*𝑦∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → {𝑦 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} ∈ V) |
64 | 62, 63 | mp1i 13 |
. . . . . 6
⊢
(((ω ∈ V ∧ (ω × ω) ∈ V) ∧
𝑥 ∈ (ω ×
(ω × ω))) → {𝑦 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} ∈ V) |
65 | 19, 64 | opabex3d 7903 |
. . . . 5
⊢ ((ω
∈ V ∧ (ω × ω) ∈ V) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (ω × (ω ×
ω)) ∧ ∃𝑖
∈ ω ∃𝑗
∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))} ∈ V) |
66 | 17, 18, 65 | mp2an 691 |
. . . 4
⊢
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (ω ×
(ω × ω)) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))} ∈ V |
67 | 16, 66 | eqeltri 2834 |
. . 3
⊢
{⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} ∈ V |
68 | 67 | rdg0 8372 |
. 2
⊢
(rec((𝑓 ∈ V
↦ (𝑓 ∪
{⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} |
69 | 6, 68 | eqtrdi 2793 |
1
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}) |