Step |
Hyp |
Ref |
Expression |
1 |
|
tskmval |
|- ( A e. V -> ( tarskiMap ` A ) = |^| { x e. Tarski | A e. x } ) |
2 |
1
|
eleq2d |
|- ( A e. V -> ( B e. ( tarskiMap ` A ) <-> B e. |^| { x e. Tarski | A e. x } ) ) |
3 |
|
elex |
|- ( B e. |^| { x e. Tarski | A e. x } -> B e. _V ) |
4 |
3
|
a1i |
|- ( A e. V -> ( B e. |^| { x e. Tarski | A e. x } -> B e. _V ) ) |
5 |
|
tskmid |
|- ( A e. V -> A e. ( tarskiMap ` A ) ) |
6 |
|
tskmcl |
|- ( tarskiMap ` A ) e. Tarski |
7 |
|
eleq2 |
|- ( x = ( tarskiMap ` A ) -> ( A e. x <-> A e. ( tarskiMap ` A ) ) ) |
8 |
|
eleq2 |
|- ( x = ( tarskiMap ` A ) -> ( B e. x <-> B e. ( tarskiMap ` A ) ) ) |
9 |
7 8
|
imbi12d |
|- ( x = ( tarskiMap ` A ) -> ( ( A e. x -> B e. x ) <-> ( A e. ( tarskiMap ` A ) -> B e. ( tarskiMap ` A ) ) ) ) |
10 |
9
|
rspcv |
|- ( ( tarskiMap ` A ) e. Tarski -> ( A. x e. Tarski ( A e. x -> B e. x ) -> ( A e. ( tarskiMap ` A ) -> B e. ( tarskiMap ` A ) ) ) ) |
11 |
6 10
|
ax-mp |
|- ( A. x e. Tarski ( A e. x -> B e. x ) -> ( A e. ( tarskiMap ` A ) -> B e. ( tarskiMap ` A ) ) ) |
12 |
5 11
|
syl5com |
|- ( A e. V -> ( A. x e. Tarski ( A e. x -> B e. x ) -> B e. ( tarskiMap ` A ) ) ) |
13 |
|
elex |
|- ( B e. ( tarskiMap ` A ) -> B e. _V ) |
14 |
12 13
|
syl6 |
|- ( A e. V -> ( A. x e. Tarski ( A e. x -> B e. x ) -> B e. _V ) ) |
15 |
|
elintrabg |
|- ( B e. _V -> ( B e. |^| { x e. Tarski | A e. x } <-> A. x e. Tarski ( A e. x -> B e. x ) ) ) |
16 |
15
|
a1i |
|- ( A e. V -> ( B e. _V -> ( B e. |^| { x e. Tarski | A e. x } <-> A. x e. Tarski ( A e. x -> B e. x ) ) ) ) |
17 |
4 14 16
|
pm5.21ndd |
|- ( A e. V -> ( B e. |^| { x e. Tarski | A e. x } <-> A. x e. Tarski ( A e. x -> B e. x ) ) ) |
18 |
2 17
|
bitrd |
|- ( A e. V -> ( B e. ( tarskiMap ` A ) <-> A. x e. Tarski ( A e. x -> B e. x ) ) ) |