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