Description: Define the canonical injection from the generating set I into the base set of the free group. (Contributed by Mario Carneiro, 2-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-vrgp | ⊢ varFGrp = ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ [ 〈“ 〈 𝑗 , ∅ 〉 ”〉 ] ( ~FG ‘ 𝑖 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cvrgp | ⊢ varFGrp | |
1 | vi | ⊢ 𝑖 | |
2 | cvv | ⊢ V | |
3 | vj | ⊢ 𝑗 | |
4 | 1 | cv | ⊢ 𝑖 |
5 | 3 | cv | ⊢ 𝑗 |
6 | c0 | ⊢ ∅ | |
7 | 5 6 | cop | ⊢ 〈 𝑗 , ∅ 〉 |
8 | 7 | cs1 | ⊢ 〈“ 〈 𝑗 , ∅ 〉 ”〉 |
9 | cefg | ⊢ ~FG | |
10 | 4 9 | cfv | ⊢ ( ~FG ‘ 𝑖 ) |
11 | 8 10 | cec | ⊢ [ 〈“ 〈 𝑗 , ∅ 〉 ”〉 ] ( ~FG ‘ 𝑖 ) |
12 | 3 4 11 | cmpt | ⊢ ( 𝑗 ∈ 𝑖 ↦ [ 〈“ 〈 𝑗 , ∅ 〉 ”〉 ] ( ~FG ‘ 𝑖 ) ) |
13 | 1 2 12 | cmpt | ⊢ ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ [ 〈“ 〈 𝑗 , ∅ 〉 ”〉 ] ( ~FG ‘ 𝑖 ) ) ) |
14 | 0 13 | wceq | ⊢ varFGrp = ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ [ 〈“ 〈 𝑗 , ∅ 〉 ”〉 ] ( ~FG ‘ 𝑖 ) ) ) |