Step |
Hyp |
Ref |
Expression |
1 |
|
vrgpfval.r |
⊢ ∼ = ( ~FG ‘ 𝐼 ) |
2 |
|
vrgpfval.u |
⊢ 𝑈 = ( varFGrp ‘ 𝐼 ) |
3 |
|
vrgpf.m |
⊢ 𝐺 = ( freeGrp ‘ 𝐼 ) |
4 |
|
vrgpf.x |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
5 |
1 2
|
vrgpfval |
⊢ ( 𝐼 ∈ 𝑉 → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ [ 〈“ 〈 𝑗 , ∅ 〉 ”〉 ] ∼ ) ) |
6 |
|
0ex |
⊢ ∅ ∈ V |
7 |
6
|
prid1 |
⊢ ∅ ∈ { ∅ , 1o } |
8 |
|
df2o3 |
⊢ 2o = { ∅ , 1o } |
9 |
7 8
|
eleqtrri |
⊢ ∅ ∈ 2o |
10 |
|
opelxpi |
⊢ ( ( 𝑗 ∈ 𝐼 ∧ ∅ ∈ 2o ) → 〈 𝑗 , ∅ 〉 ∈ ( 𝐼 × 2o ) ) |
11 |
9 10
|
mpan2 |
⊢ ( 𝑗 ∈ 𝐼 → 〈 𝑗 , ∅ 〉 ∈ ( 𝐼 × 2o ) ) |
12 |
11
|
adantl |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐼 ) → 〈 𝑗 , ∅ 〉 ∈ ( 𝐼 × 2o ) ) |
13 |
12
|
s1cld |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐼 ) → 〈“ 〈 𝑗 , ∅ 〉 ”〉 ∈ Word ( 𝐼 × 2o ) ) |
14 |
|
2on |
⊢ 2o ∈ On |
15 |
|
xpexg |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V ) |
16 |
14 15
|
mpan2 |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × 2o ) ∈ V ) |
17 |
16
|
adantr |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐼 ) → ( 𝐼 × 2o ) ∈ V ) |
18 |
|
wrdexg |
⊢ ( ( 𝐼 × 2o ) ∈ V → Word ( 𝐼 × 2o ) ∈ V ) |
19 |
|
fvi |
⊢ ( Word ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) ) |
20 |
17 18 19
|
3syl |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐼 ) → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) ) |
21 |
13 20
|
eleqtrrd |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐼 ) → 〈“ 〈 𝑗 , ∅ 〉 ”〉 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ) |
22 |
|
eqid |
⊢ ( I ‘ Word ( 𝐼 × 2o ) ) = ( I ‘ Word ( 𝐼 × 2o ) ) |
23 |
3 1 22 4
|
frgpeccl |
⊢ ( 〈“ 〈 𝑗 , ∅ 〉 ”〉 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) → [ 〈“ 〈 𝑗 , ∅ 〉 ”〉 ] ∼ ∈ 𝑋 ) |
24 |
21 23
|
syl |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐼 ) → [ 〈“ 〈 𝑗 , ∅ 〉 ”〉 ] ∼ ∈ 𝑋 ) |
25 |
5 24
|
fmpt3d |
⊢ ( 𝐼 ∈ 𝑉 → 𝑈 : 𝐼 ⟶ 𝑋 ) |