Metamath Proof Explorer

Theorem bj-restuni

Description: The union of an elementwise intersection by a set is equal to the intersection with that set of the union of the family. See also restuni and restuni2 . (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion bj-restuni 
|- ( ( X e. V /\ A e. W ) -> U. ( X |`t A ) = ( U. X i^i A ) )

Proof

Step Hyp Ref Expression
1 eluni 
 |-  ( x e. U. ( X |`t A ) <-> E. y ( x e. y /\ y e. ( X |`t A ) ) )
2 elrest 
 |-  ( ( X e. V /\ A e. W ) -> ( y e. ( X |`t A ) <-> E. z e. X y = ( z i^i A ) ) )
3 2 anbi2d 
 |-  ( ( X e. V /\ A e. W ) -> ( ( x e. y /\ y e. ( X |`t A ) ) <-> ( x e. y /\ E. z e. X y = ( z i^i A ) ) ) )
4 3 exbidv 
 |-  ( ( X e. V /\ A e. W ) -> ( E. y ( x e. y /\ y e. ( X |`t A ) ) <-> E. y ( x e. y /\ E. z e. X y = ( z i^i A ) ) ) )
5 eluni 
 |-  ( x e. U. X <-> E. z ( x e. z /\ z e. X ) )
6 5 bicomi 
 |-  ( E. z ( x e. z /\ z e. X ) <-> x e. U. X )
7 6 anbi1i 
 |-  ( ( E. z ( x e. z /\ z e. X ) /\ x e. A ) <-> ( x e. U. X /\ x e. A ) )
8 7 a1i 
 |-  ( ( X e. V /\ A e. W ) -> ( ( E. z ( x e. z /\ z e. X ) /\ x e. A ) <-> ( x e. U. X /\ x e. A ) ) )
9 df-rex 
 |-  ( E. z e. X y = ( z i^i A ) <-> E. z ( z e. X /\ y = ( z i^i A ) ) )
10 9 anbi2i 
 |-  ( ( x e. y /\ E. z e. X y = ( z i^i A ) ) <-> ( x e. y /\ E. z ( z e. X /\ y = ( z i^i A ) ) ) )
11 19.42v 
 |-  ( E. z ( x e. y /\ ( z e. X /\ y = ( z i^i A ) ) ) <-> ( x e. y /\ E. z ( z e. X /\ y = ( z i^i A ) ) ) )
12 11 bicomi 
 |-  ( ( x e. y /\ E. z ( z e. X /\ y = ( z i^i A ) ) ) <-> E. z ( x e. y /\ ( z e. X /\ y = ( z i^i A ) ) ) )
13 10 12 bitri 
 |-  ( ( x e. y /\ E. z e. X y = ( z i^i A ) ) <-> E. z ( x e. y /\ ( z e. X /\ y = ( z i^i A ) ) ) )
14 13 exbii 
 |-  ( E. y ( x e. y /\ E. z e. X y = ( z i^i A ) ) <-> E. y E. z ( x e. y /\ ( z e. X /\ y = ( z i^i A ) ) ) )
15 excom 
 |-  ( E. y E. z ( x e. y /\ ( z e. X /\ y = ( z i^i A ) ) ) <-> E. z E. y ( x e. y /\ ( z e. X /\ y = ( z i^i A ) ) ) )
16 an12 
 |-  ( ( x e. y /\ ( z e. X /\ y = ( z i^i A ) ) ) <-> ( z e. X /\ ( x e. y /\ y = ( z i^i A ) ) ) )
17 16 exbii 
 |-  ( E. y ( x e. y /\ ( z e. X /\ y = ( z i^i A ) ) ) <-> E. y ( z e. X /\ ( x e. y /\ y = ( z i^i A ) ) ) )
18 19.42v 
 |-  ( E. y ( z e. X /\ ( x e. y /\ y = ( z i^i A ) ) ) <-> ( z e. X /\ E. y ( x e. y /\ y = ( z i^i A ) ) ) )
19 eqimss 
 |-  ( y = ( z i^i A ) -> y C_ ( z i^i A ) )
20 19 sseld 
 |-  ( y = ( z i^i A ) -> ( x e. y -> x e. ( z i^i A ) ) )
21 20 imdistanri 
 |-  ( ( x e. y /\ y = ( z i^i A ) ) -> ( x e. ( z i^i A ) /\ y = ( z i^i A ) ) )
22 eqimss2 
 |-  ( y = ( z i^i A ) -> ( z i^i A ) C_ y )
23 22 sseld 
 |-  ( y = ( z i^i A ) -> ( x e. ( z i^i A ) -> x e. y ) )
24 23 imdistanri 
 |-  ( ( x e. ( z i^i A ) /\ y = ( z i^i A ) ) -> ( x e. y /\ y = ( z i^i A ) ) )
25 21 24 impbii 
 |-  ( ( x e. y /\ y = ( z i^i A ) ) <-> ( x e. ( z i^i A ) /\ y = ( z i^i A ) ) )
26 25 exbii 
 |-  ( E. y ( x e. y /\ y = ( z i^i A ) ) <-> E. y ( x e. ( z i^i A ) /\ y = ( z i^i A ) ) )
27 19.42v 
 |-  ( E. y ( x e. ( z i^i A ) /\ y = ( z i^i A ) ) <-> ( x e. ( z i^i A ) /\ E. y y = ( z i^i A ) ) )
28 vex 
 |-  z e. _V
29 28 inex1 
 |-  ( z i^i A ) e. _V
30 29 isseti 
 |-  E. y y = ( z i^i A )
31 30 biantru 
 |-  ( x e. ( z i^i A ) <-> ( x e. ( z i^i A ) /\ E. y y = ( z i^i A ) ) )
32 31 bicomi 
 |-  ( ( x e. ( z i^i A ) /\ E. y y = ( z i^i A ) ) <-> x e. ( z i^i A ) )
33 elin 
 |-  ( x e. ( z i^i A ) <-> ( x e. z /\ x e. A ) )
34 32 33 bitri 
 |-  ( ( x e. ( z i^i A ) /\ E. y y = ( z i^i A ) ) <-> ( x e. z /\ x e. A ) )
35 26 27 34 3bitri 
 |-  ( E. y ( x e. y /\ y = ( z i^i A ) ) <-> ( x e. z /\ x e. A ) )
36 35 bianassc 
 |-  ( ( z e. X /\ E. y ( x e. y /\ y = ( z i^i A ) ) ) <-> ( ( x e. z /\ z e. X ) /\ x e. A ) )
37 17 18 36 3bitri 
 |-  ( E. y ( x e. y /\ ( z e. X /\ y = ( z i^i A ) ) ) <-> ( ( x e. z /\ z e. X ) /\ x e. A ) )
38 37 exbii 
 |-  ( E. z E. y ( x e. y /\ ( z e. X /\ y = ( z i^i A ) ) ) <-> E. z ( ( x e. z /\ z e. X ) /\ x e. A ) )
39 19.41v 
 |-  ( E. z ( ( x e. z /\ z e. X ) /\ x e. A ) <-> ( E. z ( x e. z /\ z e. X ) /\ x e. A ) )
40 38 39 bitri 
 |-  ( E. z E. y ( x e. y /\ ( z e. X /\ y = ( z i^i A ) ) ) <-> ( E. z ( x e. z /\ z e. X ) /\ x e. A ) )
41 14 15 40 3bitri 
 |-  ( E. y ( x e. y /\ E. z e. X y = ( z i^i A ) ) <-> ( E. z ( x e. z /\ z e. X ) /\ x e. A ) )
42 elin 
 |-  ( x e. ( U. X i^i A ) <-> ( x e. U. X /\ x e. A ) )
43 8 41 42 3bitr4g 
 |-  ( ( X e. V /\ A e. W ) -> ( E. y ( x e. y /\ E. z e. X y = ( z i^i A ) ) <-> x e. ( U. X i^i A ) ) )
44 4 43 bitrd 
 |-  ( ( X e. V /\ A e. W ) -> ( E. y ( x e. y /\ y e. ( X |`t A ) ) <-> x e. ( U. X i^i A ) ) )
45 1 44 bitrid 
 |-  ( ( X e. V /\ A e. W ) -> ( x e. U. ( X |`t A ) <-> x e. ( U. X i^i A ) ) )
46 45 eqrdv 
 |-  ( ( X e. V /\ A e. W ) -> U. ( X |`t A ) = ( U. X i^i A ) )