Step |
Hyp |
Ref |
Expression |
1 |
|
ovex |
⊢ ( 1 -aryF 𝑋 ) ∈ V |
2 |
1
|
mptex |
⊢ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ) ) ∈ V |
3 |
2
|
a1i |
⊢ ( 𝑋 ∈ V → ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ) ) ∈ V ) |
4 |
|
eqid |
⊢ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ) ) = ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ) ) |
5 |
4
|
1arymaptf1o |
⊢ ( 𝑋 ∈ V → ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ) ) : ( 1 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m 𝑋 ) ) |
6 |
|
f1oeq1 |
⊢ ( ℎ = ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ) ) → ( ℎ : ( 1 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m 𝑋 ) ↔ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ) ) : ( 1 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m 𝑋 ) ) ) |
7 |
3 5 6
|
spcedv |
⊢ ( 𝑋 ∈ V → ∃ ℎ ℎ : ( 1 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m 𝑋 ) ) |
8 |
|
bren |
⊢ ( ( 1 -aryF 𝑋 ) ≈ ( 𝑋 ↑m 𝑋 ) ↔ ∃ ℎ ℎ : ( 1 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m 𝑋 ) ) |
9 |
7 8
|
sylibr |
⊢ ( 𝑋 ∈ V → ( 1 -aryF 𝑋 ) ≈ ( 𝑋 ↑m 𝑋 ) ) |
10 |
|
0ex |
⊢ ∅ ∈ V |
11 |
10
|
enref |
⊢ ∅ ≈ ∅ |
12 |
11
|
a1i |
⊢ ( ¬ 𝑋 ∈ V → ∅ ≈ ∅ ) |
13 |
|
df-naryf |
⊢ -aryF = ( 𝑛 ∈ ℕ0 , 𝑥 ∈ V ↦ ( 𝑥 ↑m ( 𝑥 ↑m ( 0 ..^ 𝑛 ) ) ) ) |
14 |
13
|
reldmmpo |
⊢ Rel dom -aryF |
15 |
14
|
ovprc2 |
⊢ ( ¬ 𝑋 ∈ V → ( 1 -aryF 𝑋 ) = ∅ ) |
16 |
|
reldmmap |
⊢ Rel dom ↑m |
17 |
16
|
ovprc1 |
⊢ ( ¬ 𝑋 ∈ V → ( 𝑋 ↑m 𝑋 ) = ∅ ) |
18 |
12 15 17
|
3brtr4d |
⊢ ( ¬ 𝑋 ∈ V → ( 1 -aryF 𝑋 ) ≈ ( 𝑋 ↑m 𝑋 ) ) |
19 |
9 18
|
pm2.61i |
⊢ ( 1 -aryF 𝑋 ) ≈ ( 𝑋 ↑m 𝑋 ) |