| Step |
Hyp |
Ref |
Expression |
| 1 |
|
unfilem1.1 |
⊢ 𝐴 ∈ ω |
| 2 |
|
unfilem1.2 |
⊢ 𝐵 ∈ ω |
| 3 |
|
unfilem1.3 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) |
| 4 |
|
ovex |
⊢ ( 𝐴 +o 𝑥 ) ∈ V |
| 5 |
4 3
|
fnmpti |
⊢ 𝐹 Fn 𝐵 |
| 6 |
1 2 3
|
unfilem1 |
⊢ ran 𝐹 = ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) |
| 7 |
|
df-fo |
⊢ ( 𝐹 : 𝐵 –onto→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ↔ ( 𝐹 Fn 𝐵 ∧ ran 𝐹 = ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) ) |
| 8 |
5 6 7
|
mpbir2an |
⊢ 𝐹 : 𝐵 –onto→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) |
| 9 |
|
fof |
⊢ ( 𝐹 : 𝐵 –onto→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) → 𝐹 : 𝐵 ⟶ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) |
| 10 |
8 9
|
ax-mp |
⊢ 𝐹 : 𝐵 ⟶ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) |
| 11 |
|
oveq2 |
⊢ ( 𝑥 = 𝑧 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑧 ) ) |
| 12 |
|
ovex |
⊢ ( 𝐴 +o 𝑧 ) ∈ V |
| 13 |
11 3 12
|
fvmpt |
⊢ ( 𝑧 ∈ 𝐵 → ( 𝐹 ‘ 𝑧 ) = ( 𝐴 +o 𝑧 ) ) |
| 14 |
|
oveq2 |
⊢ ( 𝑥 = 𝑤 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑤 ) ) |
| 15 |
|
ovex |
⊢ ( 𝐴 +o 𝑤 ) ∈ V |
| 16 |
14 3 15
|
fvmpt |
⊢ ( 𝑤 ∈ 𝐵 → ( 𝐹 ‘ 𝑤 ) = ( 𝐴 +o 𝑤 ) ) |
| 17 |
13 16
|
eqeqan12d |
⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐴 +o 𝑧 ) = ( 𝐴 +o 𝑤 ) ) ) |
| 18 |
|
elnn |
⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝐵 ∈ ω ) → 𝑧 ∈ ω ) |
| 19 |
2 18
|
mpan2 |
⊢ ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ω ) |
| 20 |
|
elnn |
⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝐵 ∈ ω ) → 𝑤 ∈ ω ) |
| 21 |
2 20
|
mpan2 |
⊢ ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ω ) |
| 22 |
|
nnacan |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) → ( ( 𝐴 +o 𝑧 ) = ( 𝐴 +o 𝑤 ) ↔ 𝑧 = 𝑤 ) ) |
| 23 |
1 19 21 22
|
mp3an3an |
⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝐴 +o 𝑧 ) = ( 𝐴 +o 𝑤 ) ↔ 𝑧 = 𝑤 ) ) |
| 24 |
17 23
|
bitrd |
⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ 𝑧 = 𝑤 ) ) |
| 25 |
24
|
biimpd |
⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) |
| 26 |
25
|
rgen2 |
⊢ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) |
| 27 |
|
dff13 |
⊢ ( 𝐹 : 𝐵 –1-1→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ↔ ( 𝐹 : 𝐵 ⟶ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) ) |
| 28 |
10 26 27
|
mpbir2an |
⊢ 𝐹 : 𝐵 –1-1→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) |
| 29 |
|
df-f1o |
⊢ ( 𝐹 : 𝐵 –1-1-onto→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ↔ ( 𝐹 : 𝐵 –1-1→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ∧ 𝐹 : 𝐵 –onto→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) ) |
| 30 |
28 8 29
|
mpbir2an |
⊢ 𝐹 : 𝐵 –1-1-onto→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) |