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 nnrp 
 |-  ( n e. NN -> n e. RR+ )
16 rpreccl 
 |-  ( n e. RR+ -> ( 1 / n ) e. RR+ )
17 15 16 syl 
 |-  ( n e. NN -> ( 1 / n ) e. RR+ )
18 17 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / n ) e. RR+ )
19 8 18 ltaddrpd 
 |-  ( ( ph /\ n e. NN ) -> C < ( C + ( 1 / n ) ) )
20 19 ad4ant14 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> C < ( C + ( 1 / n ) ) )
21 5 7 13 14 20 xrlelttrd 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> B < ( C + ( 1 / n ) ) )
22 4 21 jca 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> ( x e. A /\ B < ( C + ( 1 / n ) ) ) )
23 rabid 
 |-  ( x e. { x e. A | B < ( C + ( 1 / n ) ) } <-> ( x e. A /\ B < ( C + ( 1 / n ) ) ) )
24 22 23 sylibr 
 |-  ( ( ( ( ph /\ x e. A ) /\ B <_ C ) /\ n e. NN ) -> x e. { x e. A | B < ( C + ( 1 / n ) ) } )
25 24 ralrimiva 
 |-  ( ( ( ph /\ x e. A ) /\ B <_ C ) -> A. n e. NN x e. { x e. A | B < ( C + ( 1 / n ) ) } )
26 vex 
 |-  x e. _V
27 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 ) ) } ) )
28 26 27 ax-mp 
 |-  ( 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 ) ) } )
29 25 28 sylibr 
 |-  ( ( ( ph /\ x e. A ) /\ B <_ C ) -> x e. |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } )
30 29 ex 
 |-  ( ( ph /\ x e. A ) -> ( B <_ C -> x e. |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } ) )
31 30 ex 
 |-  ( ph -> ( x e. A -> ( B <_ C -> x e. |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } ) ) )
32 1 31 ralrimi 
 |-  ( ph -> A. x e. A ( B <_ C -> x e. |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } ) )
33 nfcv 
 |-  F/_ x NN
34 nfrab1 
 |-  F/_ x { x e. A | B < ( C + ( 1 / n ) ) }
35 33 34 nfiin 
 |-  F/_ x |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) }
36 35 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 ) ) } ) )
37 32 36 sylibr 
 |-  ( ph -> { x e. A | B <_ C } C_ |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } )
38 nnn0 
 |-  NN =/= (/)
39 38 a1i 
 |-  ( ph -> NN =/= (/) )
40 iinrab 
 |-  ( NN =/= (/) -> |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } = { x e. A | A. n e. NN B < ( C + ( 1 / n ) ) } )
41 39 40 syl 
 |-  ( ph -> |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } = { x e. A | A. n e. NN B < ( C + ( 1 / n ) ) } )
42 2 ad2antrr 
 |-  ( ( ( ( ph /\ x e. A ) /\ n e. NN ) /\ B < ( C + ( 1 / n ) ) ) -> B e. RR* )
43 11 ad4ant13 
 |-  ( ( ( ( ph /\ x e. A ) /\ n e. NN ) /\ B < ( C + ( 1 / n ) ) ) -> ( C + ( 1 / n ) ) e. RR )
44 43 rexrd 
 |-  ( ( ( ( ph /\ x e. A ) /\ n e. NN ) /\ B < ( C + ( 1 / n ) ) ) -> ( C + ( 1 / n ) ) e. RR* )
45 simpr 
 |-  ( ( ( ( ph /\ x e. A ) /\ n e. NN ) /\ B < ( C + ( 1 / n ) ) ) -> B < ( C + ( 1 / n ) ) )
46 42 44 45 xrltled 
 |-  ( ( ( ( ph /\ x e. A ) /\ n e. NN ) /\ B < ( C + ( 1 / n ) ) ) -> B <_ ( C + ( 1 / n ) ) )
47 46 ex 
 |-  ( ( ( ph /\ x e. A ) /\ n e. NN ) -> ( B < ( C + ( 1 / n ) ) -> B <_ ( C + ( 1 / n ) ) ) )
48 47 ralimdva 
 |-  ( ( ph /\ x e. A ) -> ( A. n e. NN B < ( C + ( 1 / n ) ) -> A. n e. NN B <_ ( C + ( 1 / n ) ) ) )
49 48 imp 
 |-  ( ( ( ph /\ x e. A ) /\ A. n e. NN B < ( C + ( 1 / n ) ) ) -> A. n e. NN B <_ ( C + ( 1 / n ) ) )
50 nfv 
 |-  F/ n ( ph /\ x e. A )
51 nfra1 
 |-  F/ n A. n e. NN B < ( C + ( 1 / n ) )
52 50 51 nfan 
 |-  F/ n ( ( ph /\ x e. A ) /\ A. n e. NN B < ( C + ( 1 / n ) ) )
53 2 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ A. n e. NN B < ( C + ( 1 / n ) ) ) -> B e. RR* )
54 3 ad2antrr 
 |-  ( ( ( ph /\ x e. A ) /\ A. n e. NN B < ( C + ( 1 / n ) ) ) -> C e. RR )
55 52 53 54 xrralrecnnle 
 |-  ( ( ( ph /\ x e. A ) /\ A. n e. NN B < ( C + ( 1 / n ) ) ) -> ( B <_ C <-> A. n e. NN B <_ ( C + ( 1 / n ) ) ) )
56 49 55 mpbird 
 |-  ( ( ( ph /\ x e. A ) /\ A. n e. NN B < ( C + ( 1 / n ) ) ) -> B <_ C )
57 56 ex 
 |-  ( ( ph /\ x e. A ) -> ( A. n e. NN B < ( C + ( 1 / n ) ) -> B <_ C ) )
58 57 ex 
 |-  ( ph -> ( x e. A -> ( A. n e. NN B < ( C + ( 1 / n ) ) -> B <_ C ) ) )
59 1 58 ralrimi 
 |-  ( ph -> A. x e. A ( A. n e. NN B < ( C + ( 1 / n ) ) -> B <_ C ) )
60 ss2rab 
 |-  ( { x e. A | A. n e. NN B < ( C + ( 1 / n ) ) } C_ { x e. A | B <_ C } <-> A. x e. A ( A. n e. NN B < ( C + ( 1 / n ) ) -> B <_ C ) )
61 59 60 sylibr 
 |-  ( ph -> { x e. A | A. n e. NN B < ( C + ( 1 / n ) ) } C_ { x e. A | B <_ C } )
62 41 61 eqsstrd 
 |-  ( ph -> |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } C_ { x e. A | B <_ C } )
63 37 62 eqssd 
 |-  ( ph -> { x e. A | B <_ C } = |^|_ n e. NN { x e. A | B < ( C + ( 1 / n ) ) } )