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