Metamath Proof Explorer

Theorem restuni3

Description: The underlying set of a subspace induced by the subspace operator ` |``t ` . The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses restuni3.1 
|- ( ph -> A e. V )
restuni3.2 
|- ( ph -> B e. W )
Assertion restuni3 
|- ( ph -> U. ( A |`t B ) = ( U. A i^i B ) )

Proof

Step Hyp Ref Expression
1 restuni3.1 
 |-  ( ph -> A e. V )
2 restuni3.2 
 |-  ( ph -> B e. W )
3 eluni2 
 |-  ( x e. U. ( A |`t B ) <-> E. y e. ( A |`t B ) x e. y )
4 3 biimpi 
 |-  ( x e. U. ( A |`t B ) -> E. y e. ( A |`t B ) x e. y )
5 4 adantl 
 |-  ( ( ph /\ x e. U. ( A |`t B ) ) -> E. y e. ( A |`t B ) x e. y )
6 simpr 
 |-  ( ( ph /\ y e. ( A |`t B ) ) -> y e. ( A |`t B ) )
7 elrest 
 |-  ( ( A e. V /\ B e. W ) -> ( y e. ( A |`t B ) <-> E. z e. A y = ( z i^i B ) ) )
8 1 2 7 syl2anc 
 |-  ( ph -> ( y e. ( A |`t B ) <-> E. z e. A y = ( z i^i B ) ) )
9 8 adantr 
 |-  ( ( ph /\ y e. ( A |`t B ) ) -> ( y e. ( A |`t B ) <-> E. z e. A y = ( z i^i B ) ) )
10 6 9 mpbid 
 |-  ( ( ph /\ y e. ( A |`t B ) ) -> E. z e. A y = ( z i^i B ) )
11 10 3adant3 
 |-  ( ( ph /\ y e. ( A |`t B ) /\ x e. y ) -> E. z e. A y = ( z i^i B ) )
12 simpl 
 |-  ( ( x e. y /\ y = ( z i^i B ) ) -> x e. y )
13 simpr 
 |-  ( ( x e. y /\ y = ( z i^i B ) ) -> y = ( z i^i B ) )
14 12 13 eleqtrd 
 |-  ( ( x e. y /\ y = ( z i^i B ) ) -> x e. ( z i^i B ) )
15 14 ex 
 |-  ( x e. y -> ( y = ( z i^i B ) -> x e. ( z i^i B ) ) )
16 15 3ad2ant3 
 |-  ( ( ph /\ y e. ( A |`t B ) /\ x e. y ) -> ( y = ( z i^i B ) -> x e. ( z i^i B ) ) )
17 16 reximdv 
 |-  ( ( ph /\ y e. ( A |`t B ) /\ x e. y ) -> ( E. z e. A y = ( z i^i B ) -> E. z e. A x e. ( z i^i B ) ) )
18 11 17 mpd 
 |-  ( ( ph /\ y e. ( A |`t B ) /\ x e. y ) -> E. z e. A x e. ( z i^i B ) )
19 18 3exp 
 |-  ( ph -> ( y e. ( A |`t B ) -> ( x e. y -> E. z e. A x e. ( z i^i B ) ) ) )
20 19 rexlimdv 
 |-  ( ph -> ( E. y e. ( A |`t B ) x e. y -> E. z e. A x e. ( z i^i B ) ) )
21 20 adantr 
 |-  ( ( ph /\ x e. U. ( A |`t B ) ) -> ( E. y e. ( A |`t B ) x e. y -> E. z e. A x e. ( z i^i B ) ) )
22 5 21 mpd 
 |-  ( ( ph /\ x e. U. ( A |`t B ) ) -> E. z e. A x e. ( z i^i B ) )
23 elinel1 
 |-  ( x e. ( z i^i B ) -> x e. z )
24 23 adantl 
 |-  ( ( z e. A /\ x e. ( z i^i B ) ) -> x e. z )
25 simpl 
 |-  ( ( z e. A /\ x e. ( z i^i B ) ) -> z e. A )
26 elunii 
 |-  ( ( x e. z /\ z e. A ) -> x e. U. A )
27 24 25 26 syl2anc 
 |-  ( ( z e. A /\ x e. ( z i^i B ) ) -> x e. U. A )
28 elinel2 
 |-  ( x e. ( z i^i B ) -> x e. B )
29 28 adantl 
 |-  ( ( z e. A /\ x e. ( z i^i B ) ) -> x e. B )
30 27 29 elind 
 |-  ( ( z e. A /\ x e. ( z i^i B ) ) -> x e. ( U. A i^i B ) )
31 30 ex 
 |-  ( z e. A -> ( x e. ( z i^i B ) -> x e. ( U. A i^i B ) ) )
32 31 adantl 
 |-  ( ( ( ph /\ x e. U. ( A |`t B ) ) /\ z e. A ) -> ( x e. ( z i^i B ) -> x e. ( U. A i^i B ) ) )
33 32 rexlimdva 
 |-  ( ( ph /\ x e. U. ( A |`t B ) ) -> ( E. z e. A x e. ( z i^i B ) -> x e. ( U. A i^i B ) ) )
34 22 33 mpd 
 |-  ( ( ph /\ x e. U. ( A |`t B ) ) -> x e. ( U. A i^i B ) )
35 34 ralrimiva 
 |-  ( ph -> A. x e. U. ( A |`t B ) x e. ( U. A i^i B ) )
36 dfss3 
 |-  ( U. ( A |`t B ) C_ ( U. A i^i B ) <-> A. x e. U. ( A |`t B ) x e. ( U. A i^i B ) )
37 35 36 sylibr 
 |-  ( ph -> U. ( A |`t B ) C_ ( U. A i^i B ) )
38 elinel1 
 |-  ( x e. ( U. A i^i B ) -> x e. U. A )
39 eluni2 
 |-  ( x e. U. A <-> E. z e. A x e. z )
40 38 39 sylib 
 |-  ( x e. ( U. A i^i B ) -> E. z e. A x e. z )
41 40 adantl 
 |-  ( ( ph /\ x e. ( U. A i^i B ) ) -> E. z e. A x e. z )
42 1 adantr 
 |-  ( ( ph /\ z e. A ) -> A e. V )
43 2 adantr 
 |-  ( ( ph /\ z e. A ) -> B e. W )
44 simpr 
 |-  ( ( ph /\ z e. A ) -> z e. A )
45 eqid 
 |-  ( z i^i B ) = ( z i^i B )
46 42 43 44 45 elrestd 
 |-  ( ( ph /\ z e. A ) -> ( z i^i B ) e. ( A |`t B ) )
47 46 3adant3 
 |-  ( ( ph /\ z e. A /\ x e. z ) -> ( z i^i B ) e. ( A |`t B ) )
48 47 3adant1r 
 |-  ( ( ( ph /\ x e. ( U. A i^i B ) ) /\ z e. A /\ x e. z ) -> ( z i^i B ) e. ( A |`t B ) )
49 simp3 
 |-  ( ( ( ph /\ x e. ( U. A i^i B ) ) /\ z e. A /\ x e. z ) -> x e. z )
50 simp1r 
 |-  ( ( ( ph /\ x e. ( U. A i^i B ) ) /\ z e. A /\ x e. z ) -> x e. ( U. A i^i B ) )
51 elinel2 
 |-  ( x e. ( U. A i^i B ) -> x e. B )
52 50 51 syl 
 |-  ( ( ( ph /\ x e. ( U. A i^i B ) ) /\ z e. A /\ x e. z ) -> x e. B )
53 simpl 
 |-  ( ( x e. z /\ x e. B ) -> x e. z )
54 simpr 
 |-  ( ( x e. z /\ x e. B ) -> x e. B )
55 53 54 elind 
 |-  ( ( x e. z /\ x e. B ) -> x e. ( z i^i B ) )
56 49 52 55 syl2anc 
 |-  ( ( ( ph /\ x e. ( U. A i^i B ) ) /\ z e. A /\ x e. z ) -> x e. ( z i^i B ) )
57 eleq2 
 |-  ( y = ( z i^i B ) -> ( x e. y <-> x e. ( z i^i B ) ) )
58 57 rspcev 
 |-  ( ( ( z i^i B ) e. ( A |`t B ) /\ x e. ( z i^i B ) ) -> E. y e. ( A |`t B ) x e. y )
59 48 56 58 syl2anc 
 |-  ( ( ( ph /\ x e. ( U. A i^i B ) ) /\ z e. A /\ x e. z ) -> E. y e. ( A |`t B ) x e. y )
60 59 3exp 
 |-  ( ( ph /\ x e. ( U. A i^i B ) ) -> ( z e. A -> ( x e. z -> E. y e. ( A |`t B ) x e. y ) ) )
61 60 rexlimdv 
 |-  ( ( ph /\ x e. ( U. A i^i B ) ) -> ( E. z e. A x e. z -> E. y e. ( A |`t B ) x e. y ) )
62 41 61 mpd 
 |-  ( ( ph /\ x e. ( U. A i^i B ) ) -> E. y e. ( A |`t B ) x e. y )
63 62 3 sylibr 
 |-  ( ( ph /\ x e. ( U. A i^i B ) ) -> x e. U. ( A |`t B ) )
64 37 63 eqelssd 
 |-  ( ph -> U. ( A |`t B ) = ( U. A i^i B ) )