Step |
Hyp |
Ref |
Expression |
1 |
|
difeq2 |
|- ( x = (/) -> ( A \ x ) = ( A \ (/) ) ) |
2 |
|
dif0 |
|- ( A \ (/) ) = A |
3 |
1 2
|
eqtrdi |
|- ( x = (/) -> ( A \ x ) = A ) |
4 |
3
|
breq1d |
|- ( x = (/) -> ( ( A \ x ) ~~ A <-> A ~~ A ) ) |
5 |
4
|
imbi2d |
|- ( x = (/) -> ( ( _om ~<_ A -> ( A \ x ) ~~ A ) <-> ( _om ~<_ A -> A ~~ A ) ) ) |
6 |
|
difeq2 |
|- ( x = y -> ( A \ x ) = ( A \ y ) ) |
7 |
6
|
breq1d |
|- ( x = y -> ( ( A \ x ) ~~ A <-> ( A \ y ) ~~ A ) ) |
8 |
7
|
imbi2d |
|- ( x = y -> ( ( _om ~<_ A -> ( A \ x ) ~~ A ) <-> ( _om ~<_ A -> ( A \ y ) ~~ A ) ) ) |
9 |
|
difeq2 |
|- ( x = ( y u. { z } ) -> ( A \ x ) = ( A \ ( y u. { z } ) ) ) |
10 |
|
difun1 |
|- ( A \ ( y u. { z } ) ) = ( ( A \ y ) \ { z } ) |
11 |
9 10
|
eqtrdi |
|- ( x = ( y u. { z } ) -> ( A \ x ) = ( ( A \ y ) \ { z } ) ) |
12 |
11
|
breq1d |
|- ( x = ( y u. { z } ) -> ( ( A \ x ) ~~ A <-> ( ( A \ y ) \ { z } ) ~~ A ) ) |
13 |
12
|
imbi2d |
|- ( x = ( y u. { z } ) -> ( ( _om ~<_ A -> ( A \ x ) ~~ A ) <-> ( _om ~<_ A -> ( ( A \ y ) \ { z } ) ~~ A ) ) ) |
14 |
|
difeq2 |
|- ( x = B -> ( A \ x ) = ( A \ B ) ) |
15 |
14
|
breq1d |
|- ( x = B -> ( ( A \ x ) ~~ A <-> ( A \ B ) ~~ A ) ) |
16 |
15
|
imbi2d |
|- ( x = B -> ( ( _om ~<_ A -> ( A \ x ) ~~ A ) <-> ( _om ~<_ A -> ( A \ B ) ~~ A ) ) ) |
17 |
|
reldom |
|- Rel ~<_ |
18 |
17
|
brrelex2i |
|- ( _om ~<_ A -> A e. _V ) |
19 |
|
enrefg |
|- ( A e. _V -> A ~~ A ) |
20 |
18 19
|
syl |
|- ( _om ~<_ A -> A ~~ A ) |
21 |
|
domen2 |
|- ( ( A \ y ) ~~ A -> ( _om ~<_ ( A \ y ) <-> _om ~<_ A ) ) |
22 |
21
|
biimparc |
|- ( ( _om ~<_ A /\ ( A \ y ) ~~ A ) -> _om ~<_ ( A \ y ) ) |
23 |
|
infdifsn |
|- ( _om ~<_ ( A \ y ) -> ( ( A \ y ) \ { z } ) ~~ ( A \ y ) ) |
24 |
22 23
|
syl |
|- ( ( _om ~<_ A /\ ( A \ y ) ~~ A ) -> ( ( A \ y ) \ { z } ) ~~ ( A \ y ) ) |
25 |
|
entr |
|- ( ( ( ( A \ y ) \ { z } ) ~~ ( A \ y ) /\ ( A \ y ) ~~ A ) -> ( ( A \ y ) \ { z } ) ~~ A ) |
26 |
24 25
|
sylancom |
|- ( ( _om ~<_ A /\ ( A \ y ) ~~ A ) -> ( ( A \ y ) \ { z } ) ~~ A ) |
27 |
26
|
ex |
|- ( _om ~<_ A -> ( ( A \ y ) ~~ A -> ( ( A \ y ) \ { z } ) ~~ A ) ) |
28 |
27
|
a2i |
|- ( ( _om ~<_ A -> ( A \ y ) ~~ A ) -> ( _om ~<_ A -> ( ( A \ y ) \ { z } ) ~~ A ) ) |
29 |
28
|
a1i |
|- ( y e. Fin -> ( ( _om ~<_ A -> ( A \ y ) ~~ A ) -> ( _om ~<_ A -> ( ( A \ y ) \ { z } ) ~~ A ) ) ) |
30 |
5 8 13 16 20 29
|
findcard2 |
|- ( B e. Fin -> ( _om ~<_ A -> ( A \ B ) ~~ A ) ) |
31 |
30
|
impcom |
|- ( ( _om ~<_ A /\ B e. Fin ) -> ( A \ B ) ~~ A ) |