Metamath Proof Explorer

Theorem preimageiingt

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

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

Proof

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