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 ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ∪ ( 𝑋 ↾t 𝐴 ) = ( ∪ 𝑋 ∩ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eluni ⊢ ( 𝑥 ∈ ∪ ( 𝑋 ↾t 𝐴 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑋 ↾t 𝐴 ) ) )
2 elrest ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑦 ∈ ( 𝑋 ↾t 𝐴 ) ↔ ∃ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ∩ 𝐴 ) ) )
3 2 anbi2d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑋 ↾t 𝐴 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) )
4 3 exbidv ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑋 ↾t 𝐴 ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) )
5 eluni ⊢ ( 𝑥 ∈ ∪ 𝑋 ↔ ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋 ) )
6 5 bicomi ⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋 ) ↔ 𝑥 ∈ ∪ 𝑋 )
7 6 anbi1i ⊢ ( ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ ∪ 𝑋 ∧ 𝑥 ∈ 𝐴 ) )
8 7 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ ∪ 𝑋 ∧ 𝑥 ∈ 𝐴 ) ) )
9 df-rex ⊢ ( ∃ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ∩ 𝐴 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) )
10 9 anbi2i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) )
11 19.42v ⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝑦 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) )
12 11 bicomi ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) ↔ ∃ 𝑧 ( 𝑥 ∈ 𝑦 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) )
13 10 12 bitri ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ↔ ∃ 𝑧 ( 𝑥 ∈ 𝑦 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) )
14 13 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 ∈ 𝑦 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) )
15 excom ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 ∈ 𝑦 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) ↔ ∃ 𝑧 ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) )
16 an12 ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) )
17 16 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) )
18 19.42v ⊢ ( ∃ 𝑦 ( 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) ↔ ( 𝑧 ∈ 𝑋 ∧ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) )
19 eqimss ⊢ ( 𝑦 = ( 𝑧 ∩ 𝐴 ) → 𝑦 ⊆ ( 𝑧 ∩ 𝐴 ) )
20 19 sseld ⊢ ( 𝑦 = ( 𝑧 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) ) )
21 20 imdistanri ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) → ( 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) )
22 eqimss2 ⊢ ( 𝑦 = ( 𝑧 ∩ 𝐴 ) → ( 𝑧 ∩ 𝐴 ) ⊆ 𝑦 )
23 22 sseld ⊢ ( 𝑦 = ( 𝑧 ∩ 𝐴 ) → ( 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) → 𝑥 ∈ 𝑦 ) )
24 23 imdistanri ⊢ ( ( 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) → ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) )
25 21 24 impbii ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ↔ ( 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) )
26 25 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) )
27 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ↔ ( 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) ∧ ∃ 𝑦 𝑦 = ( 𝑧 ∩ 𝐴 ) ) )
28 vex ⊢ 𝑧 ∈ V
29 28 inex1 ⊢ ( 𝑧 ∩ 𝐴 ) ∈ V
30 29 isseti ⊢ ∃ 𝑦 𝑦 = ( 𝑧 ∩ 𝐴 )
31 30 biantru ⊢ ( 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) ↔ ( 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) ∧ ∃ 𝑦 𝑦 = ( 𝑧 ∩ 𝐴 ) ) )
32 31 bicomi ⊢ ( ( 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) ∧ ∃ 𝑦 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ↔ 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) )
33 elin ⊢ ( 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝐴 ) )
34 32 33 bitri ⊢ ( ( 𝑥 ∈ ( 𝑧 ∩ 𝐴 ) ∧ ∃ 𝑦 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝐴 ) )
35 26 27 34 3bitri ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝐴 ) )
36 35 bianassc ⊢ ( ( 𝑧 ∈ 𝑋 ∧ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) ↔ ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) )
37 17 18 36 3bitri ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) ↔ ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) )
38 37 exbii ⊢ ( ∃ 𝑧 ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) ↔ ∃ 𝑧 ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) )
39 19.41v ⊢ ( ∃ 𝑧 ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) ↔ ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) )
40 38 39 bitri ⊢ ( ∃ 𝑧 ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ) ↔ ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) )
41 14 15 40 3bitri ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ↔ ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) )
42 elin ⊢ ( 𝑥 ∈ ( ∪ 𝑋 ∩ 𝐴 ) ↔ ( 𝑥 ∈ ∪ 𝑋 ∧ 𝑥 ∈ 𝐴 ) )
43 8 41 42 3bitr4g ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ∩ 𝐴 ) ) ↔ 𝑥 ∈ ( ∪ 𝑋 ∩ 𝐴 ) ) )
44 4 43 bitrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑋 ↾t 𝐴 ) ) ↔ 𝑥 ∈ ( ∪ 𝑋 ∩ 𝐴 ) ) )
45 1 44 syl5bb ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑥 ∈ ∪ ( 𝑋 ↾t 𝐴 ) ↔ 𝑥 ∈ ( ∪ 𝑋 ∩ 𝐴 ) ) )
46 45 eqrdv ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ∪ ( 𝑋 ↾t 𝐴 ) = ( ∪ 𝑋 ∩ 𝐴 ) )