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 biimpi 
 |-  ( 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 22 adantl 
 |-  ( ( 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 ) } )
24 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 ) } )
25 4 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. T )
26 25 3 eleqtrdi 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. ( S |`t D ) )
27 2 elexd 
 |-  ( ph -> D e. _V )
28 elrest 
 |-  ( ( S e. SAlg /\ D e. _V ) -> ( ( F ` n ) e. ( S |`t D ) <-> E. x e. S ( F ` n ) = ( x i^i D ) ) )
29 1 27 28 syl2anc 
 |-  ( ph -> ( ( F ` n ) e. ( S |`t D ) <-> E. x e. S ( F ` n ) = ( x i^i D ) ) )
30 29 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( ( F ` n ) e. ( S |`t D ) <-> E. x e. S ( F ` n ) = ( x i^i D ) ) )
31 26 30 mpbid 
 |-  ( ( ph /\ n e. NN ) -> E. x e. S ( F ` n ) = ( x i^i D ) )
32 rabn0 
 |-  ( { x e. S | ( F ` n ) = ( x i^i D ) } =/= (/) <-> E. x e. S ( F ` n ) = ( x i^i D ) )
33 31 32 sylibr 
 |-  ( ( ph /\ n e. NN ) -> { x e. S | ( F ` n ) = ( x i^i D ) } =/= (/) )
34 33 3adant3 
 |-  ( ( ph /\ n e. NN /\ y = { x e. S | ( F ` n ) = ( x i^i D ) } ) -> { x e. S | ( F ` n ) = ( x i^i D ) } =/= (/) )
35 24 34 eqnetrd 
 |-  ( ( ph /\ n e. NN /\ y = { x e. S | ( F ` n ) = ( x i^i D ) } ) -> y =/= (/) )
36 35 3exp 
 |-  ( ph -> ( n e. NN -> ( y = { x e. S | ( F ` n ) = ( x i^i D ) } -> y =/= (/) ) ) )
37 36 rexlimdv 
 |-  ( ph -> ( E. n e. NN y = { x e. S | ( F ` n ) = ( x i^i D ) } -> y =/= (/) ) )
38 37 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 =/= (/) ) )
39 23 38 mpd 
 |-  ( ( ph /\ y e. ran ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) ) -> y =/= (/) )
40 18 39 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 ) )
41 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 )
42 fveq2 
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
43 42 eqeq1d 
 |-  ( n = m -> ( ( F ` n ) = ( x i^i D ) <-> ( F ` m ) = ( x i^i D ) ) )
44 43 rabbidv 
 |-  ( n = m -> { x e. S | ( F ` n ) = ( x i^i D ) } = { x e. S | ( F ` m ) = ( x i^i D ) } )
45 44 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 ) } )
46 45 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 ) } )
47 46 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 ) } ) )
48 47 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 ) } ) )
49 48 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 ) } ) )
50 46 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 )
51 50 biimpi 
 |-  ( 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 51 adantl 
 |-  ( ( 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 )
53 52 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 )
54 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 )
55 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 )
56 ineq1 
 |-  ( x = z -> ( x i^i D ) = ( z i^i D ) )
57 56 eqeq2d 
 |-  ( x = z -> ( ( F ` m ) = ( x i^i D ) <-> ( F ` m ) = ( z i^i D ) ) )
58 57 cbvrabv 
 |-  { x e. S | ( F ` m ) = ( x i^i D ) } = { z e. S | ( F ` m ) = ( z i^i D ) }
59 58 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 ) } )
60 45 59 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 ) } )
61 60 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 ) } ) )
62 47 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 ) } ) )
63 62 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 ) } ) )
64 46 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 ) } )
65 64 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 )
66 fveq2 
 |-  ( y = z -> ( f ` y ) = ( f ` z ) )
67 id 
 |-  ( y = z -> y = z )
68 66 67 eleq12d 
 |-  ( y = z -> ( ( f ` y ) e. y <-> ( f ` z ) e. z ) )
69 68 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 )
70 65 69 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 )
71 70 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 )
72 71 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 )
73 54 55 8 61 63 72 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 ) )
74 41 49 53 73 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 ) )
75 74 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 ) ) )
76 75 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 ) ) )
77 40 76 mpd 
 |-  ( ph -> E. e e. ( S ^m NN ) A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) )
78 1 3ad2ant1 
 |-  ( ( ph /\ e e. ( S ^m NN ) /\ A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) ) -> S e. SAlg )
79 27 3ad2ant1 
 |-  ( ( ph /\ e e. ( S ^m NN ) /\ A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) ) -> D e. _V )
80 1 adantr 
 |-  ( ( ph /\ e e. ( S ^m NN ) ) -> S e. SAlg )
81 nnct 
 |-  NN ~<_ _om
82 81 a1i 
 |-  ( ( ph /\ e e. ( S ^m NN ) ) -> NN ~<_ _om )
83 elmapi 
 |-  ( e e. ( S ^m NN ) -> e : NN --> S )
84 83 adantl 
 |-  ( ( ph /\ e e. ( S ^m NN ) ) -> e : NN --> S )
85 84 ffvelcdmda 
 |-  ( ( ( ph /\ e e. ( S ^m NN ) ) /\ n e. NN ) -> ( e ` n ) e. S )
86 80 82 85 saliuncl 
 |-  ( ( ph /\ e e. ( S ^m NN ) ) -> U_ n e. NN ( e ` n ) e. S )
87 86 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 )
88 eqid 
 |-  ( U_ n e. NN ( e ` n ) i^i D ) = ( U_ n e. NN ( e ` n ) i^i D )
89 78 79 87 88 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 ) )
90 nfra1 
 |-  F/ n A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D )
91 rspa 
 |-  ( ( A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) /\ n e. NN ) -> ( F ` n ) = ( ( e ` n ) i^i D ) )
92 90 91 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 ) )
93 iunin1 
 |-  U_ n e. NN ( ( e ` n ) i^i D ) = ( U_ n e. NN ( e ` n ) i^i D )
94 93 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 ) )
95 92 94 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 ) )
96 95 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 ) )
97 3 a1i 
 |-  ( ( ph /\ e e. ( S ^m NN ) /\ A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) ) -> T = ( S |`t D ) )
98 96 97 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 ) ) )
99 89 98 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 )
100 99 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 ) ) )
101 100 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 ) )
102 77 101 mpd 
 |-  ( ph -> U_ n e. NN ( F ` n ) e. T )