Metamath Proof Explorer

Theorem subsalsal

Description: A subspace sigma-algebra is a sigma algebra. This is Lemma 121A of Fremlin1 p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses subsalsal.1 
|- ( ph -> S e. SAlg )
subsalsal.2 
|- ( ph -> D e. V )
subsalsal.3 
|- T = ( S |`t D )
Assertion subsalsal 
|- ( ph -> T e. SAlg )

Proof

Step Hyp Ref Expression
1 subsalsal.1 
 |-  ( ph -> S e. SAlg )
2 subsalsal.2 
 |-  ( ph -> D e. V )
3 subsalsal.3 
 |-  T = ( S |`t D )
4 3 ovexi 
 |-  T e. _V
5 4 a1i 
 |-  ( ph -> T e. _V )
6 1 0sald 
 |-  ( ph -> (/) e. S )
7 0in 
 |-  ( (/) i^i D ) = (/)
8 7 eqcomi 
 |-  (/) = ( (/) i^i D )
9 1 2 6 8 elrestd 
 |-  ( ph -> (/) e. ( S |`t D ) )
10 9 3 eleqtrrdi 
 |-  ( ph -> (/) e. T )
11 eqid 
 |-  U. T = U. T
12 id 
 |-  ( x e. T -> x e. T )
13 12 3 eleqtrdi 
 |-  ( x e. T -> x e. ( S |`t D ) )
14 13 adantl 
 |-  ( ( ph /\ x e. T ) -> x e. ( S |`t D ) )
15 elrest 
 |-  ( ( S e. SAlg /\ D e. V ) -> ( x e. ( S |`t D ) <-> E. y e. S x = ( y i^i D ) ) )
16 1 2 15 syl2anc 
 |-  ( ph -> ( x e. ( S |`t D ) <-> E. y e. S x = ( y i^i D ) ) )
17 16 adantr 
 |-  ( ( ph /\ x e. T ) -> ( x e. ( S |`t D ) <-> E. y e. S x = ( y i^i D ) ) )
18 14 17 mpbid 
 |-  ( ( ph /\ x e. T ) -> E. y e. S x = ( y i^i D ) )
19 1 adantr 
 |-  ( ( ph /\ y e. S ) -> S e. SAlg )
20 19 3adant3 
 |-  ( ( ph /\ y e. S /\ x = ( y i^i D ) ) -> S e. SAlg )
21 2 3ad2ant1 
 |-  ( ( ph /\ y e. S /\ x = ( y i^i D ) ) -> D e. V )
22 simpr 
 |-  ( ( ph /\ y e. S ) -> y e. S )
23 19 22 saldifcld 
 |-  ( ( ph /\ y e. S ) -> ( U. S \ y ) e. S )
24 23 3adant3 
 |-  ( ( ph /\ y e. S /\ x = ( y i^i D ) ) -> ( U. S \ y ) e. S )
25 eqid 
 |-  ( ( U. S \ y ) i^i D ) = ( ( U. S \ y ) i^i D )
26 20 21 24 25 elrestd 
 |-  ( ( ph /\ y e. S /\ x = ( y i^i D ) ) -> ( ( U. S \ y ) i^i D ) e. ( S |`t D ) )
27 3 unieqi 
 |-  U. T = U. ( S |`t D )
28 27 a1i 
 |-  ( ph -> U. T = U. ( S |`t D ) )
29 1 2 restuni3 
 |-  ( ph -> U. ( S |`t D ) = ( U. S i^i D ) )
30 28 29 eqtrd 
 |-  ( ph -> U. T = ( U. S i^i D ) )
31 30 adantr 
 |-  ( ( ph /\ x = ( y i^i D ) ) -> U. T = ( U. S i^i D ) )
32 simpr 
 |-  ( ( ph /\ x = ( y i^i D ) ) -> x = ( y i^i D ) )
33 31 32 difeq12d 
 |-  ( ( ph /\ x = ( y i^i D ) ) -> ( U. T \ x ) = ( ( U. S i^i D ) \ ( y i^i D ) ) )
34 indifdir 
 |-  ( ( U. S \ y ) i^i D ) = ( ( U. S i^i D ) \ ( y i^i D ) )
35 34 eqcomi 
 |-  ( ( U. S i^i D ) \ ( y i^i D ) ) = ( ( U. S \ y ) i^i D )
36 35 a1i 
 |-  ( ( ph /\ x = ( y i^i D ) ) -> ( ( U. S i^i D ) \ ( y i^i D ) ) = ( ( U. S \ y ) i^i D ) )
37 33 36 eqtrd 
 |-  ( ( ph /\ x = ( y i^i D ) ) -> ( U. T \ x ) = ( ( U. S \ y ) i^i D ) )
38 3 a1i 
 |-  ( ( ph /\ x = ( y i^i D ) ) -> T = ( S |`t D ) )
39 37 38 eleq12d 
 |-  ( ( ph /\ x = ( y i^i D ) ) -> ( ( U. T \ x ) e. T <-> ( ( U. S \ y ) i^i D ) e. ( S |`t D ) ) )
40 39 3adant2 
 |-  ( ( ph /\ y e. S /\ x = ( y i^i D ) ) -> ( ( U. T \ x ) e. T <-> ( ( U. S \ y ) i^i D ) e. ( S |`t D ) ) )
41 26 40 mpbird 
 |-  ( ( ph /\ y e. S /\ x = ( y i^i D ) ) -> ( U. T \ x ) e. T )
42 41 3exp 
 |-  ( ph -> ( y e. S -> ( x = ( y i^i D ) -> ( U. T \ x ) e. T ) ) )
43 42 rexlimdv 
 |-  ( ph -> ( E. y e. S x = ( y i^i D ) -> ( U. T \ x ) e. T ) )
44 43 adantr 
 |-  ( ( ph /\ x e. T ) -> ( E. y e. S x = ( y i^i D ) -> ( U. T \ x ) e. T ) )
45 18 44 mpd 
 |-  ( ( ph /\ x e. T ) -> ( U. T \ x ) e. T )
46 1 adantr 
 |-  ( ( ph /\ f : NN --> T ) -> S e. SAlg )
47 2 adantr 
 |-  ( ( ph /\ f : NN --> T ) -> D e. V )
48 simpr 
 |-  ( ( ph /\ f : NN --> T ) -> f : NN --> T )
49 46 47 3 48 subsaliuncl 
 |-  ( ( ph /\ f : NN --> T ) -> U_ n e. NN ( f ` n ) e. T )
50 5 10 11 45 49 issalnnd 
 |-  ( ph -> T e. SAlg )