Metamath Proof Explorer

Theorem subsaliuncllem

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 subsaliuncllem.f 
|- F/ y ph
subsaliuncllem.s 
|- ( ph -> S e. V )
subsaliuncllem.g 
|- G = ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } )
subsaliuncllem.e 
|- E = ( H o. G )
subsaliuncllem.h 
|- ( ph -> H Fn ran G )
subsaliuncllem.y 
|- ( ph -> A. y e. ran G ( H ` y ) e. y )
Assertion subsaliuncllem 
|- ( ph -> E. e e. ( S ^m NN ) A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) )

Proof

Step Hyp Ref Expression
1 subsaliuncllem.f 
 |-  F/ y ph
2 subsaliuncllem.s 
 |-  ( ph -> S e. V )
3 subsaliuncllem.g 
 |-  G = ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } )
4 subsaliuncllem.e 
 |-  E = ( H o. G )
5 subsaliuncllem.h 
 |-  ( ph -> H Fn ran G )
6 subsaliuncllem.y 
 |-  ( ph -> A. y e. ran G ( H ` y ) e. y )
7 vex 
 |-  y e. _V
8 3 elrnmpt 
 |-  ( y e. _V -> ( y e. ran G <-> E. n e. NN y = { x e. S | ( F ` n ) = ( x i^i D ) } ) )
9 7 8 ax-mp 
 |-  ( y e. ran G <-> E. n e. NN y = { x e. S | ( F ` n ) = ( x i^i D ) } )
10 9 biimpi 
 |-  ( y e. ran G -> E. n e. NN y = { x e. S | ( F ` n ) = ( x i^i D ) } )
11 id 
 |-  ( y = { x e. S | ( F ` n ) = ( x i^i D ) } -> y = { x e. S | ( F ` n ) = ( x i^i D ) } )
12 ssrab2 
 |-  { x e. S | ( F ` n ) = ( x i^i D ) } C_ S
13 12 a1i 
 |-  ( y = { x e. S | ( F ` n ) = ( x i^i D ) } -> { x e. S | ( F ` n ) = ( x i^i D ) } C_ S )
14 11 13 eqsstrd 
 |-  ( y = { x e. S | ( F ` n ) = ( x i^i D ) } -> y C_ S )
15 14 a1i 
 |-  ( n e. NN -> ( y = { x e. S | ( F ` n ) = ( x i^i D ) } -> y C_ S ) )
16 15 rexlimiv 
 |-  ( E. n e. NN y = { x e. S | ( F ` n ) = ( x i^i D ) } -> y C_ S )
17 16 a1i 
 |-  ( y e. ran G -> ( E. n e. NN y = { x e. S | ( F ` n ) = ( x i^i D ) } -> y C_ S ) )
18 10 17 mpd 
 |-  ( y e. ran G -> y C_ S )
19 18 adantl 
 |-  ( ( ph /\ y e. ran G ) -> y C_ S )
20 6 r19.21bi 
 |-  ( ( ph /\ y e. ran G ) -> ( H ` y ) e. y )
21 19 20 sseldd 
 |-  ( ( ph /\ y e. ran G ) -> ( H ` y ) e. S )
22 21 ex 
 |-  ( ph -> ( y e. ran G -> ( H ` y ) e. S ) )
23 1 22 ralrimi 
 |-  ( ph -> A. y e. ran G ( H ` y ) e. S )
24 5 23 jca 
 |-  ( ph -> ( H Fn ran G /\ A. y e. ran G ( H ` y ) e. S ) )
25 ffnfv 
 |-  ( H : ran G --> S <-> ( H Fn ran G /\ A. y e. ran G ( H ` y ) e. S ) )
26 24 25 sylibr 
 |-  ( ph -> H : ran G --> S )
27 eqid 
 |-  { x e. S | ( F ` n ) = ( x i^i D ) } = { x e. S | ( F ` n ) = ( x i^i D ) }
28 27 2 rabexd 
 |-  ( ph -> { x e. S | ( F ` n ) = ( x i^i D ) } e. _V )
29 28 ralrimivw 
 |-  ( ph -> A. n e. NN { x e. S | ( F ` n ) = ( x i^i D ) } e. _V )
30 3 fnmpt 
 |-  ( A. n e. NN { x e. S | ( F ` n ) = ( x i^i D ) } e. _V -> G Fn NN )
31 29 30 syl 
 |-  ( ph -> G Fn NN )
32 dffn3 
 |-  ( G Fn NN <-> G : NN --> ran G )
33 31 32 sylib 
 |-  ( ph -> G : NN --> ran G )
34 fco 
 |-  ( ( H : ran G --> S /\ G : NN --> ran G ) -> ( H o. G ) : NN --> S )
35 26 33 34 syl2anc 
 |-  ( ph -> ( H o. G ) : NN --> S )
36 nnex 
 |-  NN e. _V
37 36 a1i 
 |-  ( ph -> NN e. _V )
38 2 37 elmapd 
 |-  ( ph -> ( ( H o. G ) e. ( S ^m NN ) <-> ( H o. G ) : NN --> S ) )
39 35 38 mpbird 
 |-  ( ph -> ( H o. G ) e. ( S ^m NN ) )
40 4 39 eqeltrid 
 |-  ( ph -> E e. ( S ^m NN ) )
41 33 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) e. ran G )
42 6 adantr 
 |-  ( ( ph /\ n e. NN ) -> A. y e. ran G ( H ` y ) e. y )
43 fveq2 
 |-  ( y = ( G ` n ) -> ( H ` y ) = ( H ` ( G ` n ) ) )
44 id 
 |-  ( y = ( G ` n ) -> y = ( G ` n ) )
45 43 44 eleq12d 
 |-  ( y = ( G ` n ) -> ( ( H ` y ) e. y <-> ( H ` ( G ` n ) ) e. ( G ` n ) ) )
46 45 rspcva 
 |-  ( ( ( G ` n ) e. ran G /\ A. y e. ran G ( H ` y ) e. y ) -> ( H ` ( G ` n ) ) e. ( G ` n ) )
47 41 42 46 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( H ` ( G ` n ) ) e. ( G ` n ) )
48 33 ffund 
 |-  ( ph -> Fun G )
49 48 adantr 
 |-  ( ( ph /\ n e. NN ) -> Fun G )
50 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
51 3 dmeqi 
 |-  dom G = dom ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } )
52 51 a1i 
 |-  ( ph -> dom G = dom ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) )
53 dmmptg 
 |-  ( A. n e. NN { x e. S | ( F ` n ) = ( x i^i D ) } e. _V -> dom ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) = NN )
54 29 53 syl 
 |-  ( ph -> dom ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) = NN )
55 52 54 eqtrd 
 |-  ( ph -> dom G = NN )
56 55 eqcomd 
 |-  ( ph -> NN = dom G )
57 56 adantr 
 |-  ( ( ph /\ n e. NN ) -> NN = dom G )
58 50 57 eleqtrd 
 |-  ( ( ph /\ n e. NN ) -> n e. dom G )
59 49 58 4 fvcod 
 |-  ( ( ph /\ n e. NN ) -> ( E ` n ) = ( H ` ( G ` n ) ) )
60 3 a1i 
 |-  ( ph -> G = ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } ) )
61 28 adantr 
 |-  ( ( ph /\ n e. NN ) -> { x e. S | ( F ` n ) = ( x i^i D ) } e. _V )
62 60 61 fvmpt2d 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) = { x e. S | ( F ` n ) = ( x i^i D ) } )
63 62 eqcomd 
 |-  ( ( ph /\ n e. NN ) -> { x e. S | ( F ` n ) = ( x i^i D ) } = ( G ` n ) )
64 59 63 eleq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( E ` n ) e. { x e. S | ( F ` n ) = ( x i^i D ) } <-> ( H ` ( G ` n ) ) e. ( G ` n ) ) )
65 47 64 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( E ` n ) e. { x e. S | ( F ` n ) = ( x i^i D ) } )
66 ineq1 
 |-  ( x = ( E ` n ) -> ( x i^i D ) = ( ( E ` n ) i^i D ) )
67 66 eqeq2d 
 |-  ( x = ( E ` n ) -> ( ( F ` n ) = ( x i^i D ) <-> ( F ` n ) = ( ( E ` n ) i^i D ) ) )
68 67 elrab 
 |-  ( ( E ` n ) e. { x e. S | ( F ` n ) = ( x i^i D ) } <-> ( ( E ` n ) e. S /\ ( F ` n ) = ( ( E ` n ) i^i D ) ) )
69 65 68 sylib 
 |-  ( ( ph /\ n e. NN ) -> ( ( E ` n ) e. S /\ ( F ` n ) = ( ( E ` n ) i^i D ) ) )
70 69 simprd 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) = ( ( E ` n ) i^i D ) )
71 70 ralrimiva 
 |-  ( ph -> A. n e. NN ( F ` n ) = ( ( E ` n ) i^i D ) )
72 fveq1 
 |-  ( e = E -> ( e ` n ) = ( E ` n ) )
73 72 ineq1d 
 |-  ( e = E -> ( ( e ` n ) i^i D ) = ( ( E ` n ) i^i D ) )
74 73 eqeq2d 
 |-  ( e = E -> ( ( F ` n ) = ( ( e ` n ) i^i D ) <-> ( F ` n ) = ( ( E ` n ) i^i D ) ) )
75 74 ralbidv 
 |-  ( e = E -> ( A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) <-> A. n e. NN ( F ` n ) = ( ( E ` n ) i^i D ) ) )
76 75 rspcev 
 |-  ( ( E e. ( S ^m NN ) /\ A. n e. NN ( F ` n ) = ( ( E ` n ) i^i D ) ) -> E. e e. ( S ^m NN ) A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) )
77 40 71 76 syl2anc 
 |-  ( ph -> E. e e. ( S ^m NN ) A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) )