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 φ S SAlg
salpreimalegt.u A = S
salpreimalegt.b φ x A B *
salpreimalegt.p φ a x A | B a S
salpreimalegt.c φ C
Assertion salpreimalegt φ x A | C < B S

Proof

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