Step |
Hyp |
Ref |
Expression |
1 |
|
0ex |
⊢ ∅ ∈ V |
2 |
|
satf |
⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ) → ( ∅ Sat ∅ ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } ) ↾ suc ω ) ) |
3 |
1 1 2
|
mp2an |
⊢ ( ∅ Sat ∅ ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } ) ↾ suc ω ) |
4 |
|
peano1 |
⊢ ∅ ∈ ω |
5 |
4
|
ne0ii |
⊢ ω ≠ ∅ |
6 |
|
map0b |
⊢ ( ω ≠ ∅ → ( ∅ ↑m ω ) = ∅ ) |
7 |
5 6
|
ax-mp |
⊢ ( ∅ ↑m ω ) = ∅ |
8 |
7
|
difeq1i |
⊢ ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) = ( ∅ ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) |
9 |
|
0dif |
⊢ ( ∅ ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) = ∅ |
10 |
8 9
|
eqtri |
⊢ ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) = ∅ |
11 |
10
|
eqeq2i |
⊢ ( 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ↔ 𝑦 = ∅ ) |
12 |
11
|
anbi2i |
⊢ ( ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ↔ ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ) |
13 |
12
|
rexbii |
⊢ ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ↔ ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ) |
14 |
|
r19.41v |
⊢ ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ↔ ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ) |
15 |
13 14
|
bitri |
⊢ ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ↔ ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ) |
16 |
7
|
rabeqi |
⊢ { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } = { 𝑎 ∈ ∅ ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } |
17 |
|
rab0 |
⊢ { 𝑎 ∈ ∅ ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } = ∅ |
18 |
16 17
|
eqtri |
⊢ { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } = ∅ |
19 |
18
|
eqeq2i |
⊢ ( 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ↔ 𝑦 = ∅ ) |
20 |
19
|
anbi2i |
⊢ ( ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ↔ ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) |
21 |
20
|
rexbii |
⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ↔ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) |
22 |
|
r19.41v |
⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ↔ ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) |
23 |
21 22
|
bitri |
⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ↔ ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) |
24 |
15 23
|
orbi12i |
⊢ ( ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ∨ ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) ) |
25 |
24
|
rexbii |
⊢ ( ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑢 ∈ 𝑓 ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ∨ ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) ) |
26 |
|
andir |
⊢ ( ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ∧ 𝑦 = ∅ ) ↔ ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ∨ ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) ) |
27 |
26
|
bicomi |
⊢ ( ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ∨ ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) ↔ ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ∧ 𝑦 = ∅ ) ) |
28 |
27
|
rexbii |
⊢ ( ∃ 𝑢 ∈ 𝑓 ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ∨ ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) ↔ ∃ 𝑢 ∈ 𝑓 ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ∧ 𝑦 = ∅ ) ) |
29 |
|
r19.41v |
⊢ ( ∃ 𝑢 ∈ 𝑓 ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ∧ 𝑦 = ∅ ) ↔ ( ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ∧ 𝑦 = ∅ ) ) |
30 |
25 28 29
|
3bitri |
⊢ ( ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ( ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ∧ 𝑦 = ∅ ) ) |
31 |
30
|
biancomi |
⊢ ( ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) ) |
32 |
31
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } |
33 |
32
|
uneq2i |
⊢ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) = ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) |
34 |
33
|
mpteq2i |
⊢ ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ) = ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) |
35 |
7
|
rabeqi |
⊢ { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } = { 𝑎 ∈ ∅ ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } |
36 |
|
rab0 |
⊢ { 𝑎 ∈ ∅ ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } = ∅ |
37 |
35 36
|
eqtri |
⊢ { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } = ∅ |
38 |
37
|
eqeq2i |
⊢ ( 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ↔ 𝑦 = ∅ ) |
39 |
38
|
anbi2i |
⊢ ( ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) ↔ ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = ∅ ) ) |
40 |
39
|
2rexbii |
⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = ∅ ) ) |
41 |
|
r19.41vv |
⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = ∅ ) ↔ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = ∅ ) ) |
42 |
40 41
|
bitri |
⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) ↔ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = ∅ ) ) |
43 |
42
|
biancomi |
⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) ↔ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) ) |
44 |
43
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } |
45 |
|
rdgeq12 |
⊢ ( ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ) = ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) ∧ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) → rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } ) = rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) ) |
46 |
34 44 45
|
mp2an |
⊢ rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } ) = rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) |
47 |
46
|
reseq1i |
⊢ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } ) ↾ suc ω ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) ↾ suc ω ) |
48 |
3 47
|
eqtri |
⊢ ( ∅ Sat ∅ ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) ↾ suc ω ) |