Step |
Hyp |
Ref |
Expression |
1 |
|
0ex |
⊢ ∅ ∈ V |
2 |
1 1
|
pm3.2i |
⊢ ( ∅ ∈ V ∧ ∅ ∈ V ) |
3 |
2
|
jctr |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( ∅ ∈ V ∧ ∅ ∈ V ) ) ) |
4 |
3
|
3adant3 |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( ∅ ∈ V ∧ ∅ ∈ V ) ) ) |
5 |
|
satfdm |
⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( ∅ ∈ V ∧ ∅ ∈ V ) ) → ∀ 𝑛 ∈ ω dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) ) |
6 |
4 5
|
syl |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ∀ 𝑛 ∈ ω dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) ) |
7 |
|
fveq2 |
⊢ ( 𝑛 = 𝑁 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) |
8 |
7
|
dmeqd |
⊢ ( 𝑛 = 𝑁 → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) |
9 |
|
fveq2 |
⊢ ( 𝑛 = 𝑁 → ( ( ∅ Sat ∅ ) ‘ 𝑛 ) = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) |
10 |
9
|
dmeqd |
⊢ ( 𝑛 = 𝑁 → dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) |
11 |
8 10
|
eqeq12d |
⊢ ( 𝑛 = 𝑁 → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) ↔ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) |
12 |
11
|
rspcv |
⊢ ( 𝑁 ∈ ω → ( ∀ 𝑛 ∈ ω dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) |
13 |
12
|
3ad2ant3 |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ∀ 𝑛 ∈ ω dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) |
14 |
6 13
|
mpd |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) |
15 |
|
elelsuc |
⊢ ( 𝑁 ∈ ω → 𝑁 ∈ suc ω ) |
16 |
15
|
3ad2ant3 |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → 𝑁 ∈ suc ω ) |
17 |
|
fmlafv |
⊢ ( 𝑁 ∈ suc ω → ( Fmla ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) |
18 |
16 17
|
syl |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( Fmla ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) |
19 |
14 18
|
eqtr4d |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = ( Fmla ‘ 𝑁 ) ) |