Metamath Proof Explorer

Theorem subsaliuncl

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

Ref Expression
Hypotheses subsaliuncl.1 
|- ( ph -> S e. SAlg )
subsaliuncl.2 
|- ( ph -> D e. V )
subsaliuncl.3 
|- T = ( S |`t D )
subsaliuncl.4 
|- ( ph -> F : NN --> T )
Assertion subsaliuncl 
|- ( ph -> U_ n e. NN ( F ` n ) e. T )

Proof

Step Hyp Ref Expression
1 subsaliuncl.1 
 |-  ( ph -> S e. SAlg )
2 subsaliuncl.2 
 |-  ( ph -> D e. V )
3 subsaliuncl.3 
 |-  T = ( S |`t D )
4 subsaliuncl.4 
 |-  ( ph -> F : NN --> T )
5 eqid 
 |-  { x e. S | ( F ` n ) = ( x i^i D ) } = { x e. S | ( F ` n ) = ( x i^i D ) }
6 5 1 rabexd 
 |-  ( ph -> { x e. S | ( F ` n ) = ( x i^i D ) } e. _V )
7 6 ralrimivw 
 |-  ( ph -> A. n e. NN { x e. S | ( F ` n ) = ( x i^i D ) } e. _V )
8 eqid 
 |-  ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) = ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } )
9 8 fnmpt 
 |-  ( A. n e. NN { x e. S | ( F ` n ) = ( x i^i D ) } e. _V -> ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) Fn NN )
10 7 9 syl 
 |-  ( ph -> ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) Fn NN )
11 nnex 
 |-  NN e. _V
12 fnrndomg 
 |-  ( NN e. _V -> ( ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) Fn NN -> ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ~<_ NN ) )
13 11 12 ax-mp 
 |-  ( ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) Fn NN -> ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ~<_ NN )
14 10 13 syl 
 |-  ( ph -> ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ~<_ NN )
15 nnenom 
 |-  NN ~~ _om
16 15 a1i 
 |-  ( ph -> NN ~~ _om )
17 domentr 
 |-  ( ( ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ~<_ NN /\ NN ~~ _om ) -> ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ~<_ _om )
18 14 16 17 syl2anc 
 |-  ( ph -> ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ~<_ _om )
19 vex 
 |-  y e. _V
20 8 elrnmpt 
 |-  ( y e. _V -> ( y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) <-> E. n e. NN y = { x e. S | ( F ` n ) = ( x i^i D ) } ) )
21 19 20 ax-mp 
 |-  ( y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) <-> E. n e. NN y = { x e. S | ( F ` n ) = ( x i^i D ) } )
22 21 bilani 
 |-  ( ( ph /\ y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ) -> E. n e. NN y = { x e. S | ( F ` n ) = ( x i^i D ) } )
23 simp3 
 |-  ( ( ph /\ n e. NN /\ y = { x e. S | ( F ` n ) = ( x i^i D ) } ) -> y = { x e. S | ( F ` n ) = ( x i^i D ) } )
24 4 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. T )
25 24 3 eleqtrdi 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. ( S |`t D ) )
26 2 elexd 
 |-  ( ph -> D e. _V )
27 elrest 
 |-  ( ( S e. SAlg /\ D e. _V ) -> ( ( F ` n ) e. ( S |`t D ) <-> E. x e. S ( F ` n ) = ( x i^i D ) ) )
28 1 26 27 syl2anc 
 |-  ( ph -> ( ( F ` n ) e. ( S |`t D ) <-> E. x e. S ( F ` n ) = ( x i^i D ) ) )
29 28 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( ( F ` n ) e. ( S |`t D ) <-> E. x e. S ( F ` n ) = ( x i^i D ) ) )
30 25 29 mpbid 
 |-  ( ( ph /\ n e. NN ) -> E. x e. S ( F ` n ) = ( x i^i D ) )
31 rabn0 
 |-  ( { x e. S | ( F ` n ) = ( x i^i D ) } =/= (/) <-> E. x e. S ( F ` n ) = ( x i^i D ) )
32 30 31 sylibr 
 |-  ( ( ph /\ n e. NN ) -> { x e. S | ( F ` n ) = ( x i^i D ) } =/= (/) )
33 32 3adant3 
 |-  ( ( ph /\ n e. NN /\ y = { x e. S | ( F ` n ) = ( x i^i D ) } ) -> { x e. S | ( F ` n ) = ( x i^i D ) } =/= (/) )
34 23 33 eqnetrd 
 |-  ( ( ph /\ n e. NN /\ y = { x e. S | ( F ` n ) = ( x i^i D ) } ) -> y =/= (/) )
35 34 3exp 
 |-  ( ph -> ( n e. NN -> ( y = { x e. S | ( F ` n ) = ( x i^i D ) } -> y =/= (/) ) ) )
36 35 rexlimdv 
 |-  ( ph -> ( E. n e. NN y = { x e. S | ( F ` n ) = ( x i^i D ) } -> y =/= (/) ) )
37 36 adantr 
 |-  ( ( ph /\ y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ) -> ( E. n e. NN y = { x e. S | ( F ` n ) = ( x i^i D ) } -> y =/= (/) ) )
38 22 37 mpd 
 |-  ( ( ph /\ y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ) -> y =/= (/) )
39 18 38 axccdom 
 |-  ( ph -> E. f ( f Fn ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) /\ A. y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` y ) e. y ) )
40 simpl 
 |-  ( ( ph /\ ( f Fn ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) /\ A. y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` y ) e. y ) ) -> ph )
41 fveq2 
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
42 41 eqeq1d 
 |-  ( n = m -> ( ( F ` n ) = ( x i^i D ) <-> ( F ` m ) = ( x i^i D ) ) )
43 42 rabbidv 
 |-  ( n = m -> { x e. S | ( F ` n ) = ( x i^i D ) } = { x e. S | ( F ` m ) = ( x i^i D ) } )
44 43 cbvmptv 
 |-  ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) = ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } )
45 44 rneqi 
 |-  ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) = ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } )
46 45 fneq2i 
 |-  ( f Fn ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) <-> f Fn ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) )
47 46 biimpi 
 |-  ( f Fn ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) -> f Fn ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) )
48 47 ad2antrl 
 |-  ( ( ph /\ ( f Fn ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) /\ A. y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` y ) e. y ) ) -> f Fn ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) )
49 45 raleqi 
 |-  ( A. y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` y ) e. y <-> A. y e. ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) ( f ` y ) e. y )
50 49 bilani 
 |-  ( ( ph /\ A. y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` y ) e. y ) -> A. y e. ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) ( f ` y ) e. y )
51 50 adantrl 
 |-  ( ( ph /\ ( f Fn ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) /\ A. y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` y ) e. y ) ) -> A. y e. ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) ( f ` y ) e. y )
52 nfv 
 |-  F/ z ( ph /\ f Fn ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) /\ A. y e. ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) ( f ` y ) e. y )
53 1 3ad2ant1 
 |-  ( ( ph /\ f Fn ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) /\ A. y e. ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) ( f ` y ) e. y ) -> S e. SAlg )
54 ineq1 
 |-  ( x = z -> ( x i^i D ) = ( z i^i D ) )
55 54 eqeq2d 
 |-  ( x = z -> ( ( F ` m ) = ( x i^i D ) <-> ( F ` m ) = ( z i^i D ) ) )
56 55 cbvrabv 
 |-  { x e. S | ( F ` m ) = ( x i^i D ) } = { z e. S | ( F ` m ) = ( z i^i D ) }
57 56 mpteq2i 
 |-  ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) = ( m e. NN |-> { z e. S | ( F ` m ) = ( z i^i D ) } )
58 44 57 eqtr2i 
 |-  ( m e. NN |-> { z e. S | ( F ` m ) = ( z i^i D ) } ) = ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } )
59 58 coeq2i 
 |-  ( f o. ( m e. NN |-> { z e. S | ( F ` m ) = ( z i^i D ) } ) ) = ( f o. ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) )
60 46 biimpri 
 |-  ( f Fn ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) -> f Fn ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) )
61 60 3ad2ant2 
 |-  ( ( ph /\ f Fn ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) /\ A. y e. ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) ( f ` y ) e. y ) -> f Fn ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) )
62 45 eqcomi 
 |-  ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) = ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } )
63 62 raleqi 
 |-  ( A. y e. ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) ( f ` y ) e. y <-> A. y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` y ) e. y )
64 fveq2 
 |-  ( y = z -> ( f ` y ) = ( f ` z ) )
65 id 
 |-  ( y = z -> y = z )
66 64 65 eleq12d 
 |-  ( y = z -> ( ( f ` y ) e. y <-> ( f ` z ) e. z ) )
67 66 cbvralvw 
 |-  ( A. y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` y ) e. y <-> A. z e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` z ) e. z )
68 63 67 bitri 
 |-  ( A. y e. ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) ( f ` y ) e. y <-> A. z e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` z ) e. z )
69 68 biimpi 
 |-  ( A. y e. ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) ( f ` y ) e. y -> A. z e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` z ) e. z )
70 69 3ad2ant3 
 |-  ( ( ph /\ f Fn ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) /\ A. y e. ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) ( f ` y ) e. y ) -> A. z e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` z ) e. z )
71 52 53 8 59 61 70 subsaliuncllem 
 |-  ( ( ph /\ f Fn ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) /\ A. y e. ran ( m e. NN |-> { x e. S | ( F ` m ) = ( x i^i D ) } ) ( f ` y ) e. y ) -> E. e e. ( S ^m NN ) A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) )
72 40 48 51 71 syl3anc 
 |-  ( ( ph /\ ( f Fn ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) /\ A. y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` y ) e. y ) ) -> E. e e. ( S ^m NN ) A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) )
73 72 ex 
 |-  ( ph -> ( ( f Fn ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) /\ A. y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` y ) e. y ) -> E. e e. ( S ^m NN ) A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) ) )
74 73 exlimdv 
 |-  ( ph -> ( E. f ( f Fn ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) /\ A. y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ( f ` y ) e. y ) -> E. e e. ( S ^m NN ) A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) ) )
75 39 74 mpd 
 |-  ( ph -> E. e e. ( S ^m NN ) A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) )
76 1 3ad2ant1 
 |-  ( ( ph /\ e e. ( S ^m NN ) /\ A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) ) -> S e. SAlg )
77 26 3ad2ant1 
 |-  ( ( ph /\ e e. ( S ^m NN ) /\ A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) ) -> D e. _V )
78 1 adantr 
 |-  ( ( ph /\ e e. ( S ^m NN ) ) -> S e. SAlg )
79 nnct 
 |-  NN ~<_ _om
80 79 a1i 
 |-  ( ( ph /\ e e. ( S ^m NN ) ) -> NN ~<_ _om )
81 elmapi 
 |-  ( e e. ( S ^m NN ) -> e : NN --> S )
82 81 adantl 
 |-  ( ( ph /\ e e. ( S ^m NN ) ) -> e : NN --> S )
83 82 ffvelcdmda 
 |-  ( ( ( ph /\ e e. ( S ^m NN ) ) /\ n e. NN ) -> ( e ` n ) e. S )
84 78 80 83 saliuncl 
 |-  ( ( ph /\ e e. ( S ^m NN ) ) -> U_ n e. NN ( e ` n ) e. S )
85 84 3adant3 
 |-  ( ( ph /\ e e. ( S ^m NN ) /\ A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) ) -> U_ n e. NN ( e ` n ) e. S )
86 eqid 
 |-  ( U_ n e. NN ( e ` n ) i^i D ) = ( U_ n e. NN ( e ` n ) i^i D )
87 76 77 85 86 elrestd 
 |-  ( ( ph /\ e e. ( S ^m NN ) /\ A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) ) -> ( U_ n e. NN ( e ` n ) i^i D ) e. ( S |`t D ) )
88 nfra1 
 |-  F/ n A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D )
89 rspa 
 |-  ( ( A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) /\ n e. NN ) -> ( F ` n ) = ( ( e ` n ) i^i D ) )
90 88 89 iuneq2df 
 |-  ( A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) -> U_ n e. NN ( F ` n ) = U_ n e. NN ( ( e ` n ) i^i D ) )
91 iunin1 
 |-  U_ n e. NN ( ( e ` n ) i^i D ) = ( U_ n e. NN ( e ` n ) i^i D )
92 91 a1i 
 |-  ( A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) -> U_ n e. NN ( ( e ` n ) i^i D ) = ( U_ n e. NN ( e ` n ) i^i D ) )
93 90 92 eqtrd 
 |-  ( A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) -> U_ n e. NN ( F ` n ) = ( U_ n e. NN ( e ` n ) i^i D ) )
94 93 3ad2ant3 
 |-  ( ( ph /\ e e. ( S ^m NN ) /\ A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) ) -> U_ n e. NN ( F ` n ) = ( U_ n e. NN ( e ` n ) i^i D ) )
95 3 a1i 
 |-  ( ( ph /\ e e. ( S ^m NN ) /\ A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) ) -> T = ( S |`t D ) )
96 94 95 eleq12d 
 |-  ( ( ph /\ e e. ( S ^m NN ) /\ A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) ) -> ( U_ n e. NN ( F ` n ) e. T <-> ( U_ n e. NN ( e ` n ) i^i D ) e. ( S |`t D ) ) )
97 87 96 mpbird 
 |-  ( ( ph /\ e e. ( S ^m NN ) /\ A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) ) -> U_ n e. NN ( F ` n ) e. T )
98 97 3exp 
 |-  ( ph -> ( e e. ( S ^m NN ) -> ( A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) -> U_ n e. NN ( F ` n ) e. T ) ) )
99 98 rexlimdv 
 |-  ( ph -> ( E. e e. ( S ^m NN ) A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) -> U_ n e. NN ( F ` n ) e. T ) )
100 75 99 mpd 
 |-  ( ph -> U_ n e. NN ( F ` n ) e. T )