Metamath Proof Explorer

Theorem ptbasin

Description: The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypothesis 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 ) ) }
Assertion ptbasin 
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( X e. B /\ Y e. B ) ) -> ( X i^i Y ) e. B )

Proof

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 ffvelcdmda 
 |-  ( ( ( ( ( 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 biimtrrid 
 |-  ( ( ( 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 biimtrid 
 |-  ( ( 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 biimtrid 
 |-  ( ( 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 )