| Step |
Hyp |
Ref |
Expression |
| 1 |
|
resslem.r |
⊢ 𝑅 = ( 𝑊 ↾s 𝐴 ) |
| 2 |
|
resslem.e |
⊢ 𝐶 = ( 𝐸 ‘ 𝑊 ) |
| 3 |
|
resslem.f |
⊢ 𝐸 = Slot 𝑁 |
| 4 |
|
resslem.n |
⊢ 𝑁 ∈ ℕ |
| 5 |
|
resslem.b |
⊢ 1 < 𝑁 |
| 6 |
|
eqid |
⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) |
| 7 |
1 6
|
ressid2 |
⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = 𝑊 ) |
| 8 |
7
|
fveq2d |
⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) |
| 9 |
8
|
3expib |
⊢ ( ( Base ‘ 𝑊 ) ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) ) |
| 10 |
1 6
|
ressval2 |
⊢ ( ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) ) |
| 11 |
10
|
fveq2d |
⊢ ( ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) ) ) |
| 12 |
3 4
|
ndxid |
⊢ 𝐸 = Slot ( 𝐸 ‘ ndx ) |
| 13 |
3 4
|
ndxarg |
⊢ ( 𝐸 ‘ ndx ) = 𝑁 |
| 14 |
|
1re |
⊢ 1 ∈ ℝ |
| 15 |
14 5
|
gtneii |
⊢ 𝑁 ≠ 1 |
| 16 |
13 15
|
eqnetri |
⊢ ( 𝐸 ‘ ndx ) ≠ 1 |
| 17 |
|
basendx |
⊢ ( Base ‘ ndx ) = 1 |
| 18 |
16 17
|
neeqtrri |
⊢ ( 𝐸 ‘ ndx ) ≠ ( Base ‘ ndx ) |
| 19 |
12 18
|
setsnid |
⊢ ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) ) |
| 20 |
11 19
|
eqtr4di |
⊢ ( ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) |
| 21 |
20
|
3expib |
⊢ ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) ) |
| 22 |
9 21
|
pm2.61i |
⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) |
| 23 |
|
reldmress |
⊢ Rel dom ↾s |
| 24 |
23
|
ovprc1 |
⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 ↾s 𝐴 ) = ∅ ) |
| 25 |
1 24
|
syl5eq |
⊢ ( ¬ 𝑊 ∈ V → 𝑅 = ∅ ) |
| 26 |
25
|
fveq2d |
⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ ∅ ) ) |
| 27 |
3
|
str0 |
⊢ ∅ = ( 𝐸 ‘ ∅ ) |
| 28 |
26 27
|
eqtr4di |
⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ∅ ) |
| 29 |
|
fvprc |
⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ∅ ) |
| 30 |
28 29
|
eqtr4d |
⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) |
| 31 |
30
|
adantr |
⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) |
| 32 |
22 31
|
pm2.61ian |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) |
| 33 |
2 32
|
eqtr4id |
⊢ ( 𝐴 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑅 ) ) |