Step |
Hyp |
Ref |
Expression |
1 |
|
simpllr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝐵 ) → 𝐵 ∈ 𝑊 ) |
2 |
|
eleq1 |
⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝑊 ↔ 𝐵 ∈ 𝑊 ) ) |
3 |
2
|
anbi2d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) ) |
4 |
3
|
anbi1d |
⊢ ( 𝑥 = 𝐵 → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ↔ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ) ) |
5 |
|
breq2 |
⊢ ( 𝑥 = 𝐵 → ( 𝐴 𝐹 𝑥 ↔ 𝐴 𝐹 𝐵 ) ) |
6 |
4 5
|
anbi12d |
⊢ ( 𝑥 = 𝐵 → ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝑥 ) ↔ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝐵 ) ) ) |
7 |
|
eqeq2 |
⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 '''' 𝐴 ) = 𝑥 ↔ ( 𝐹 '''' 𝐴 ) = 𝐵 ) ) |
8 |
6 7
|
imbi12d |
⊢ ( 𝑥 = 𝐵 → ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝑥 ) → ( 𝐹 '''' 𝐴 ) = 𝑥 ) ↔ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝐵 ) → ( 𝐹 '''' 𝐴 ) = 𝐵 ) ) ) |
9 |
|
id |
⊢ ( 𝐴 𝐹 𝑥 → 𝐴 𝐹 𝑥 ) |
10 |
|
funressneu |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 𝐹 𝑥 ) → ∃! 𝑥 𝐴 𝐹 𝑥 ) |
11 |
10
|
3expa |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝑥 ) → ∃! 𝑥 𝐴 𝐹 𝑥 ) |
12 |
|
tz6.12-1-afv2 |
⊢ ( ( 𝐴 𝐹 𝑥 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → ( 𝐹 '''' 𝐴 ) = 𝑥 ) |
13 |
9 11 12
|
syl2an2 |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝑥 ) → ( 𝐹 '''' 𝐴 ) = 𝑥 ) |
14 |
8 13
|
vtoclg |
⊢ ( 𝐵 ∈ 𝑊 → ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝐵 ) → ( 𝐹 '''' 𝐴 ) = 𝐵 ) ) |
15 |
1 14
|
mpcom |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝐵 ) → ( 𝐹 '''' 𝐴 ) = 𝐵 ) |
16 |
15
|
ex |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐴 𝐹 𝐵 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) ) |