Step |
Hyp |
Ref |
Expression |
1 |
|
pwssnf1o.y |
⊢ 𝑌 = ( 𝑅 ↑s { 𝐼 } ) |
2 |
|
pwssnf1o.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
3 |
|
pwssnf1o.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( { 𝐼 } × { 𝑥 } ) ) |
4 |
|
pwssnf1o.c |
⊢ 𝐶 = ( Base ‘ 𝑌 ) |
5 |
2
|
fvexi |
⊢ 𝐵 ∈ V |
6 |
|
simpr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐼 ∈ 𝑊 ) |
7 |
3
|
mapsnf1o |
⊢ ( ( 𝐵 ∈ V ∧ 𝐼 ∈ 𝑊 ) → 𝐹 : 𝐵 –1-1-onto→ ( 𝐵 ↑m { 𝐼 } ) ) |
8 |
5 6 7
|
sylancr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 : 𝐵 –1-1-onto→ ( 𝐵 ↑m { 𝐼 } ) ) |
9 |
|
snex |
⊢ { 𝐼 } ∈ V |
10 |
1 2
|
pwsbas |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ { 𝐼 } ∈ V ) → ( 𝐵 ↑m { 𝐼 } ) = ( Base ‘ 𝑌 ) ) |
11 |
9 10
|
mpan2 |
⊢ ( 𝑅 ∈ 𝑉 → ( 𝐵 ↑m { 𝐼 } ) = ( Base ‘ 𝑌 ) ) |
12 |
11
|
adantr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐵 ↑m { 𝐼 } ) = ( Base ‘ 𝑌 ) ) |
13 |
4 12
|
eqtr4id |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐶 = ( 𝐵 ↑m { 𝐼 } ) ) |
14 |
13
|
f1oeq3d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ 𝐹 : 𝐵 –1-1-onto→ ( 𝐵 ↑m { 𝐼 } ) ) ) |
15 |
8 14
|
mpbird |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) |