Step |
Hyp |
Ref |
Expression |
1 |
|
peano1 |
⊢ ∅ ∈ ω |
2 |
|
elelsuc |
⊢ ( ∅ ∈ ω → ∅ ∈ suc ω ) |
3 |
|
fmlafv |
⊢ ( ∅ ∈ suc ω → ( Fmla ‘ ∅ ) = dom ( ( ∅ Sat ∅ ) ‘ ∅ ) ) |
4 |
1 2 3
|
mp2b |
⊢ ( Fmla ‘ ∅ ) = dom ( ( ∅ Sat ∅ ) ‘ ∅ ) |
5 |
|
satf00 |
⊢ ( ( ∅ Sat ∅ ) ‘ ∅ ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } |
6 |
5
|
dmeqi |
⊢ dom ( ( ∅ Sat ∅ ) ‘ ∅ ) = dom { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } |
7 |
|
0ex |
⊢ ∅ ∈ V |
8 |
7
|
isseti |
⊢ ∃ 𝑦 𝑦 = ∅ |
9 |
|
19.41v |
⊢ ( ∃ 𝑦 ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ( ∃ 𝑦 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) ) |
10 |
8 9
|
mpbiran |
⊢ ( ∃ 𝑦 ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) |
11 |
10
|
abbii |
⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } = { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } |
12 |
|
dmopab |
⊢ dom { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } |
13 |
|
rabab |
⊢ { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } = { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } |
14 |
11 12 13
|
3eqtr4i |
⊢ dom { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } = { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } |
15 |
4 6 14
|
3eqtri |
⊢ ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } |