Metamath Proof Explorer

Theorem preimaleiinlt

Description: A preimage of a left-open, right-closed, unbounded below interval, expressed as an indexed intersection of preimages of open, unbound below intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses preimaleiinlt.x 
|- F/ x ph
preimaleiinlt.b 
|- ( ( ph /\ x e. A ) -> B e. RR* )
preimaleiinlt.c 
|- ( ph -> C e. RR )
Assertion preimaleiinlt 
|- ( ph -> { x e. A | B <_ C } = |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } )

Proof

Step Hyp Ref Expression
1 preimaleiinlt.x 
 |-  F/ x ph
2 preimaleiinlt.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
3 preimaleiinlt.c 
 |-  ( ph -> C e. RR )
4 simpllr 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> x e. A )
5 2 ad2antrr 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> B e. RR* )
6 3 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> C e. RR )
7 6 rexrd 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> C e. RR* )
8 3 adantr 
 |-  ( ( ph /\ n e. NN ) -> C e. RR )
9 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
10 9 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / n ) e. RR )
11 8 10 readdcld 
 |-  ( ( ph /\ n e. NN ) -> ( C + ( 1 / n ) ) e. RR )
12 11 ad4ant14 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> ( C + ( 1 / n ) ) e. RR )
13 12 rexrd 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> ( C + ( 1 / n ) ) e. RR* )
14 simplr 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> B <_ C )
15 nnrecrp 
 |-  ( n e. NN -> ( 1 / n ) e. RR+ )
16 15 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / n ) e. RR+ )
17 8 16 ltaddrpd 
 |-  ( ( ph /\ n e. NN ) -> C < ( C + ( 1 / n ) ) )
18 17 ad4ant14 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> C < ( C + ( 1 / n ) ) )
19 5 7 13 14 18 xrlelttrd 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> B < ( C + ( 1 / n ) ) )
20 4 19 rabidd 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> x e. { x e. A | B < ( C + ( 1 / n ) ) } )
21 20 ralrimiva 
 |-  ( ( ( ph /\ x e. A ) /\ B <_ C ) -> A. n e. NN x e. { x e. A | B < ( C + ( 1 / n ) ) } )
22 eliin 
 |-  ( x e. _V -> ( x e. |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } <-> A. n e. NN x e. { x e. A | B < ( C + ( 1 / n ) ) } ) )
23 22 elv 
 |-  ( x e. |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } <-> A. n e. NN x e. { x e. A | B < ( C + ( 1 / n ) ) } )
24 21 23 sylibr 
 |-  ( ( ( ph /\ x e. A ) /\ B <_ C ) -> x e. |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } )
25 24 ex 
 |-  ( ( ph /\ x e. A ) -> ( B <_ C -> x e. |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } ) )
26 1 25 ralrimia 
 |-  ( ph -> A. x e. A ( B <_ C -> x e. |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } ) )
27 nfcv 
 |-  F/_ x NN
28 nfrab1 
 |-  F/_ x { x e. A | B < ( C + ( 1 / n ) ) }
29 27 28 nfiin 
 |-  F/_ x |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) }
30 29 rabssf 
 |-  ( { x e. A | B <_ C } C_ |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } <-> A. x e. A ( B <_ C -> x e. |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } ) )
31 26 30 sylibr 
 |-  ( ph -> { x e. A | B <_ C } C_ |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } )
32 nnn0 
 |-  NN =/= (/)
33 iinrab 
 |-  ( NN =/= (/) -> |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } = { x e. A | A. n e. NN B < ( C + ( 1 / n ) ) } )
34 32 33 mp1i 
 |-  ( ph -> |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } = { x e. A | A. n e. NN B < ( C + ( 1 / n ) ) } )
35 2 ad2antrr 
 |-  ( ( ( ( ph /\ x e. A ) /\ n e. NN ) /\ B < ( C + ( 1 / n ) ) ) -> B e. RR* )
36 11 ad4ant13 
 |-  ( ( ( ( ph /\ x e. A ) /\ n e. NN ) /\ B < ( C + ( 1 / n ) ) ) -> ( C + ( 1 / n ) ) e. RR )
37 36 rexrd 
 |-  ( ( ( ( ph /\ x e. A ) /\ n e. NN ) /\ B < ( C + ( 1 / n ) ) ) -> ( C + ( 1 / n ) ) e. RR* )
38 simpr 
 |-  ( ( ( ( ph /\ x e. A ) /\ n e. NN ) /\ B < ( C + ( 1 / n ) ) ) -> B < ( C + ( 1 / n ) ) )
39 35 37 38 xrltled 
 |-  ( ( ( ( ph /\ x e. A ) /\ n e. NN ) /\ B < ( C + ( 1 / n ) ) ) -> B <_ ( C + ( 1 / n ) ) )
40 39 ex 
 |-  ( ( ( ph /\ x e. A ) /\ n e. NN ) -> ( B < ( C + ( 1 / n ) ) -> B <_ ( C + ( 1 / n ) ) ) )
41 40 ralimdva 
 |-  ( ( ph /\ x e. A ) -> ( A. n e. NN B < ( C + ( 1 / n ) ) -> A. n e. NN B <_ ( C + ( 1 / n ) ) ) )
42 41 imp 
 |-  ( ( ( ph /\ x e. A ) /\ A. n e. NN B < ( C + ( 1 / n ) ) ) -> A. n e. NN B <_ ( C + ( 1 / n ) ) )
43 nfv 
 |-  F/ n ( ph /\ x e. A )
44 nfra1 
 |-  F/ n A. n e. NN B < ( C + ( 1 / n ) )
45 43 44 nfan 
 |-  F/ n ( ( ph /\ x e. A ) /\ A. n e. NN B < ( C + ( 1 / n ) ) )
46 2 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ A. n e. NN B < ( C + ( 1 / n ) ) ) -> B e. RR* )
47 3 ad2antrr 
 |-  ( ( ( ph /\ x e. A ) /\ A. n e. NN B < ( C + ( 1 / n ) ) ) -> C e. RR )
48 45 46 47 xrralrecnnle 
 |-  ( ( ( ph /\ x e. A ) /\ A. n e. NN B < ( C + ( 1 / n ) ) ) -> ( B <_ C <-> A. n e. NN B <_ ( C + ( 1 / n ) ) ) )
49 42 48 mpbird 
 |-  ( ( ( ph /\ x e. A ) /\ A. n e. NN B < ( C + ( 1 / n ) ) ) -> B <_ C )
50 49 ex 
 |-  ( ( ph /\ x e. A ) -> ( A. n e. NN B < ( C + ( 1 / n ) ) -> B <_ C ) )
51 1 50 ss2rabdf 
 |-  ( ph -> { x e. A | A. n e. NN B < ( C + ( 1 / n ) ) } C_ { x e. A | B <_ C } )
52 34 51 eqsstrd 
 |-  ( ph -> |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } C_ { x e. A | B <_ C } )
53 31 52 eqssd 
 |-  ( ph -> { x e. A | B <_ C } = |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } )