Step |
Hyp |
Ref |
Expression |
1 |
|
ptbas.1 |
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } |
2 |
1
|
elpt |
|- ( X e. B <-> E. a ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ X = X_ y e. A ( a ` y ) ) ) |
3 |
1
|
elpt |
|- ( Y e. B <-> E. b ( ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) /\ Y = X_ y e. A ( b ` y ) ) ) |
4 |
2 3
|
anbi12i |
|- ( ( X e. B /\ Y e. B ) <-> ( E. a ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ X = X_ y e. A ( a ` y ) ) /\ E. b ( ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) /\ Y = X_ y e. A ( b ` y ) ) ) ) |
5 |
|
exdistrv |
|- ( E. a E. b ( ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ X = X_ y e. A ( a ` y ) ) /\ ( ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) /\ Y = X_ y e. A ( b ` y ) ) ) <-> ( E. a ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ X = X_ y e. A ( a ` y ) ) /\ E. b ( ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) /\ Y = X_ y e. A ( b ` y ) ) ) ) |
6 |
4 5
|
bitr4i |
|- ( ( X e. B /\ Y e. B ) <-> E. a E. b ( ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ X = X_ y e. A ( a ` y ) ) /\ ( ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) /\ Y = X_ y e. A ( b ` y ) ) ) ) |
7 |
|
an4 |
|- ( ( ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ X = X_ y e. A ( a ` y ) ) /\ ( ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) /\ Y = X_ y e. A ( b ` y ) ) ) <-> ( ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) /\ ( X = X_ y e. A ( a ` y ) /\ Y = X_ y e. A ( b ` y ) ) ) ) |
8 |
|
an6 |
|- ( ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) <-> ( ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) /\ ( E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) |
9 |
|
df-3an |
|- ( ( ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) /\ ( E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) <-> ( ( ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) |
10 |
8 9
|
bitri |
|- ( ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) <-> ( ( ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) |
11 |
|
reeanv |
|- ( E. c e. Fin E. d e. Fin ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) <-> ( E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) |
12 |
|
fveq2 |
|- ( y = k -> ( a ` y ) = ( a ` k ) ) |
13 |
|
fveq2 |
|- ( y = k -> ( b ` y ) = ( b ` k ) ) |
14 |
12 13
|
ineq12d |
|- ( y = k -> ( ( a ` y ) i^i ( b ` y ) ) = ( ( a ` k ) i^i ( b ` k ) ) ) |
15 |
14
|
cbvixpv |
|- X_ y e. A ( ( a ` y ) i^i ( b ` y ) ) = X_ k e. A ( ( a ` k ) i^i ( b ` k ) ) |
16 |
|
simpl1l |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) -> A e. V ) |
17 |
|
unfi |
|- ( ( c e. Fin /\ d e. Fin ) -> ( c u. d ) e. Fin ) |
18 |
17
|
ad2antrl |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) -> ( c u. d ) e. Fin ) |
19 |
|
simpl1r |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) -> F : A --> Top ) |
20 |
19
|
ffvelrnda |
|- ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) /\ k e. A ) -> ( F ` k ) e. Top ) |
21 |
|
simpl3l |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) -> A. y e. A ( a ` y ) e. ( F ` y ) ) |
22 |
|
fveq2 |
|- ( y = k -> ( F ` y ) = ( F ` k ) ) |
23 |
12 22
|
eleq12d |
|- ( y = k -> ( ( a ` y ) e. ( F ` y ) <-> ( a ` k ) e. ( F ` k ) ) ) |
24 |
23
|
rspccva |
|- ( ( A. y e. A ( a ` y ) e. ( F ` y ) /\ k e. A ) -> ( a ` k ) e. ( F ` k ) ) |
25 |
21 24
|
sylan |
|- ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) /\ k e. A ) -> ( a ` k ) e. ( F ` k ) ) |
26 |
|
simpl3r |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) -> A. y e. A ( b ` y ) e. ( F ` y ) ) |
27 |
13 22
|
eleq12d |
|- ( y = k -> ( ( b ` y ) e. ( F ` y ) <-> ( b ` k ) e. ( F ` k ) ) ) |
28 |
27
|
rspccva |
|- ( ( A. y e. A ( b ` y ) e. ( F ` y ) /\ k e. A ) -> ( b ` k ) e. ( F ` k ) ) |
29 |
26 28
|
sylan |
|- ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) /\ k e. A ) -> ( b ` k ) e. ( F ` k ) ) |
30 |
|
inopn |
|- ( ( ( F ` k ) e. Top /\ ( a ` k ) e. ( F ` k ) /\ ( b ` k ) e. ( F ` k ) ) -> ( ( a ` k ) i^i ( b ` k ) ) e. ( F ` k ) ) |
31 |
20 25 29 30
|
syl3anc |
|- ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) /\ k e. A ) -> ( ( a ` k ) i^i ( b ` k ) ) e. ( F ` k ) ) |
32 |
|
simprrl |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) -> A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) |
33 |
|
ssun1 |
|- c C_ ( c u. d ) |
34 |
|
sscon |
|- ( c C_ ( c u. d ) -> ( A \ ( c u. d ) ) C_ ( A \ c ) ) |
35 |
33 34
|
ax-mp |
|- ( A \ ( c u. d ) ) C_ ( A \ c ) |
36 |
35
|
sseli |
|- ( k e. ( A \ ( c u. d ) ) -> k e. ( A \ c ) ) |
37 |
22
|
unieqd |
|- ( y = k -> U. ( F ` y ) = U. ( F ` k ) ) |
38 |
12 37
|
eqeq12d |
|- ( y = k -> ( ( a ` y ) = U. ( F ` y ) <-> ( a ` k ) = U. ( F ` k ) ) ) |
39 |
38
|
rspccva |
|- ( ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ k e. ( A \ c ) ) -> ( a ` k ) = U. ( F ` k ) ) |
40 |
32 36 39
|
syl2an |
|- ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) /\ k e. ( A \ ( c u. d ) ) ) -> ( a ` k ) = U. ( F ` k ) ) |
41 |
|
simprrr |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) -> A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) |
42 |
|
ssun2 |
|- d C_ ( c u. d ) |
43 |
|
sscon |
|- ( d C_ ( c u. d ) -> ( A \ ( c u. d ) ) C_ ( A \ d ) ) |
44 |
42 43
|
ax-mp |
|- ( A \ ( c u. d ) ) C_ ( A \ d ) |
45 |
44
|
sseli |
|- ( k e. ( A \ ( c u. d ) ) -> k e. ( A \ d ) ) |
46 |
13 37
|
eqeq12d |
|- ( y = k -> ( ( b ` y ) = U. ( F ` y ) <-> ( b ` k ) = U. ( F ` k ) ) ) |
47 |
46
|
rspccva |
|- ( ( A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) /\ k e. ( A \ d ) ) -> ( b ` k ) = U. ( F ` k ) ) |
48 |
41 45 47
|
syl2an |
|- ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) /\ k e. ( A \ ( c u. d ) ) ) -> ( b ` k ) = U. ( F ` k ) ) |
49 |
40 48
|
ineq12d |
|- ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) /\ k e. ( A \ ( c u. d ) ) ) -> ( ( a ` k ) i^i ( b ` k ) ) = ( U. ( F ` k ) i^i U. ( F ` k ) ) ) |
50 |
|
inidm |
|- ( U. ( F ` k ) i^i U. ( F ` k ) ) = U. ( F ` k ) |
51 |
49 50
|
eqtrdi |
|- ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) /\ k e. ( A \ ( c u. d ) ) ) -> ( ( a ` k ) i^i ( b ` k ) ) = U. ( F ` k ) ) |
52 |
1 16 18 31 51
|
elptr2 |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) -> X_ k e. A ( ( a ` k ) i^i ( b ` k ) ) e. B ) |
53 |
15 52
|
eqeltrid |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( ( c e. Fin /\ d e. Fin ) /\ ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) -> X_ y e. A ( ( a ` y ) i^i ( b ` y ) ) e. B ) |
54 |
53
|
expr |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( c e. Fin /\ d e. Fin ) ) -> ( ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) -> X_ y e. A ( ( a ` y ) i^i ( b ` y ) ) e. B ) ) |
55 |
54
|
rexlimdvva |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) -> ( E. c e. Fin E. d e. Fin ( A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) -> X_ y e. A ( ( a ` y ) i^i ( b ` y ) ) e. B ) ) |
56 |
11 55
|
syl5bir |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) -> ( ( E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) -> X_ y e. A ( ( a ` y ) i^i ( b ` y ) ) e. B ) ) |
57 |
56
|
3expb |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) ) -> ( ( E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) -> X_ y e. A ( ( a ` y ) i^i ( b ` y ) ) e. B ) ) |
58 |
57
|
impr |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( ( ( a Fn A /\ b Fn A ) /\ ( A. y e. A ( a ` y ) e. ( F ` y ) /\ A. y e. A ( b ` y ) e. ( F ` y ) ) ) /\ ( E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) -> X_ y e. A ( ( a ` y ) i^i ( b ` y ) ) e. B ) |
59 |
10 58
|
sylan2b |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) -> X_ y e. A ( ( a ` y ) i^i ( b ` y ) ) e. B ) |
60 |
|
ineq12 |
|- ( ( X = X_ y e. A ( a ` y ) /\ Y = X_ y e. A ( b ` y ) ) -> ( X i^i Y ) = ( X_ y e. A ( a ` y ) i^i X_ y e. A ( b ` y ) ) ) |
61 |
|
ixpin |
|- X_ y e. A ( ( a ` y ) i^i ( b ` y ) ) = ( X_ y e. A ( a ` y ) i^i X_ y e. A ( b ` y ) ) |
62 |
60 61
|
eqtr4di |
|- ( ( X = X_ y e. A ( a ` y ) /\ Y = X_ y e. A ( b ` y ) ) -> ( X i^i Y ) = X_ y e. A ( ( a ` y ) i^i ( b ` y ) ) ) |
63 |
62
|
eleq1d |
|- ( ( X = X_ y e. A ( a ` y ) /\ Y = X_ y e. A ( b ` y ) ) -> ( ( X i^i Y ) e. B <-> X_ y e. A ( ( a ` y ) i^i ( b ` y ) ) e. B ) ) |
64 |
59 63
|
syl5ibrcom |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) ) -> ( ( X = X_ y e. A ( a ` y ) /\ Y = X_ y e. A ( b ` y ) ) -> ( X i^i Y ) e. B ) ) |
65 |
64
|
expimpd |
|- ( ( A e. V /\ F : A --> Top ) -> ( ( ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) ) /\ ( X = X_ y e. A ( a ` y ) /\ Y = X_ y e. A ( b ` y ) ) ) -> ( X i^i Y ) e. B ) ) |
66 |
7 65
|
syl5bi |
|- ( ( A e. V /\ F : A --> Top ) -> ( ( ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ X = X_ y e. A ( a ` y ) ) /\ ( ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) /\ Y = X_ y e. A ( b ` y ) ) ) -> ( X i^i Y ) e. B ) ) |
67 |
66
|
exlimdvv |
|- ( ( A e. V /\ F : A --> Top ) -> ( E. a E. b ( ( ( a Fn A /\ A. y e. A ( a ` y ) e. ( F ` y ) /\ E. c e. Fin A. y e. ( A \ c ) ( a ` y ) = U. ( F ` y ) ) /\ X = X_ y e. A ( a ` y ) ) /\ ( ( b Fn A /\ A. y e. A ( b ` y ) e. ( F ` y ) /\ E. d e. Fin A. y e. ( A \ d ) ( b ` y ) = U. ( F ` y ) ) /\ Y = X_ y e. A ( b ` y ) ) ) -> ( X i^i Y ) e. B ) ) |
68 |
6 67
|
syl5bi |
|- ( ( A e. V /\ F : A --> Top ) -> ( ( X e. B /\ Y e. B ) -> ( X i^i Y ) e. B ) ) |
69 |
68
|
imp |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( X e. B /\ Y e. B ) ) -> ( X i^i Y ) e. B ) |