Metamath Proof Explorer


Theorem salpreimalegt

Description: If all the preimages of right-closed, unbounded below intervals, belong to a sigma-algebra, then all the preimages of left-open, unbounded above intervals, belong to the sigma-algebra. (ii) implies (iii) in Proposition 121B of Fremlin1 p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses salpreimalegt.x xφ
salpreimalegt.a aφ
salpreimalegt.s φSSAlg
salpreimalegt.u A=S
salpreimalegt.b φxAB*
salpreimalegt.p φaxA|BaS
salpreimalegt.c φC
Assertion salpreimalegt φxA|C<BS

Proof

Step Hyp Ref Expression
1 salpreimalegt.x xφ
2 salpreimalegt.a aφ
3 salpreimalegt.s φSSAlg
4 salpreimalegt.u A=S
5 salpreimalegt.b φxAB*
6 salpreimalegt.p φaxA|BaS
7 salpreimalegt.c φC
8 4 eqcomi S=A
9 8 a1i φS=A
10 9 difeq1d φSxA|BC=AxA|BC
11 7 rexrd φC*
12 1 5 11 preimalegt φAxA|BC=xA|C<B
13 10 12 eqtr2d φxA|C<B=SxA|BC
14 7 ancli φφC
15 nfv aC
16 2 15 nfan aφC
17 nfv axA|BCS
18 16 17 nfim aφCxA|BCS
19 eleq1 a=CaC
20 19 anbi2d a=CφaφC
21 breq2 a=CBaBC
22 21 rabbidv a=CxA|Ba=xA|BC
23 22 eleq1d a=CxA|BaSxA|BCS
24 20 23 imbi12d a=CφaxA|BaSφCxA|BCS
25 18 24 6 vtoclg1f CφCxA|BCS
26 7 14 25 sylc φxA|BCS
27 3 26 saldifcld φSxA|BCS
28 13 27 eqeltrd φxA|C<BS