Step |
Hyp |
Ref |
Expression |
1 |
|
pi1xfr.p |
⊢ 𝑃 = ( 𝐽 π1 ( 𝐹 ‘ 0 ) ) |
2 |
|
pi1xfr.q |
⊢ 𝑄 = ( 𝐽 π1 ( 𝐹 ‘ 1 ) ) |
3 |
|
pi1xfr.b |
⊢ 𝐵 = ( Base ‘ 𝑃 ) |
4 |
|
pi1xfr.g |
⊢ 𝐺 = ran ( 𝑔 ∈ ∪ 𝐵 ↦ 〈 [ 𝑔 ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) 〉 ) |
5 |
|
pi1xfr.j |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
6 |
|
pi1xfr.f |
⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) ) |
7 |
|
pi1xfrval.i |
⊢ ( 𝜑 → 𝐼 ∈ ( II Cn 𝐽 ) ) |
8 |
|
pi1xfrval.1 |
⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐼 ‘ 0 ) ) |
9 |
|
pi1xfrval.2 |
⊢ ( 𝜑 → ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) |
10 |
|
pi1xfrval.a |
⊢ ( 𝜑 → 𝐴 ∈ ∪ 𝐵 ) |
11 |
|
fvex |
⊢ ( ≃ph ‘ 𝐽 ) ∈ V |
12 |
|
ecexg |
⊢ ( ( ≃ph ‘ 𝐽 ) ∈ V → [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ∈ V ) |
13 |
11 12
|
mp1i |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ∈ V ) |
14 |
|
ecexg |
⊢ ( ( ≃ph ‘ 𝐽 ) ∈ V → [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) ∈ V ) |
15 |
11 14
|
mp1i |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) ∈ V ) |
16 |
|
eceq1 |
⊢ ( 𝑔 = 𝐴 → [ 𝑔 ] ( ≃ph ‘ 𝐽 ) = [ 𝐴 ] ( ≃ph ‘ 𝐽 ) ) |
17 |
|
oveq1 |
⊢ ( 𝑔 = 𝐴 → ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) = ( 𝐴 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) |
18 |
17
|
oveq2d |
⊢ ( 𝑔 = 𝐴 → ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) = ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝐴 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ) |
19 |
18
|
eceq1d |
⊢ ( 𝑔 = 𝐴 → [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) = [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝐴 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) ) |
20 |
1 2 3 4 5 6 7 8 9
|
pi1xfrf |
⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ ( Base ‘ 𝑄 ) ) |
21 |
20
|
ffund |
⊢ ( 𝜑 → Fun 𝐺 ) |
22 |
4 13 15 16 19 21
|
fliftval |
⊢ ( ( 𝜑 ∧ 𝐴 ∈ ∪ 𝐵 ) → ( 𝐺 ‘ [ 𝐴 ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝐴 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) ) |
23 |
10 22
|
mpdan |
⊢ ( 𝜑 → ( 𝐺 ‘ [ 𝐴 ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝐴 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) ) |