Description: Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | hstrlem2.1 | ⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) | |
Assertion | hstrlem2 | ⊢ ( 𝐶 ∈ Cℋ → ( 𝑆 ‘ 𝐶 ) = ( ( projℎ ‘ 𝐶 ) ‘ 𝑢 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hstrlem2.1 | ⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) | |
2 | fveq2 | ⊢ ( 𝑥 = 𝐶 → ( projℎ ‘ 𝑥 ) = ( projℎ ‘ 𝐶 ) ) | |
3 | 2 | fveq1d | ⊢ ( 𝑥 = 𝐶 → ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) = ( ( projℎ ‘ 𝐶 ) ‘ 𝑢 ) ) |
4 | fvex | ⊢ ( ( projℎ ‘ 𝐶 ) ‘ 𝑢 ) ∈ V | |
5 | 3 1 4 | fvmpt | ⊢ ( 𝐶 ∈ Cℋ → ( 𝑆 ‘ 𝐶 ) = ( ( projℎ ‘ 𝐶 ) ‘ 𝑢 ) ) |