Metamath Proof Explorer

Theorem dstfrvunirn

Description: The limit of all preimage maps by the "less than or equal to" relation is the universe. (Contributed by Thierry Arnoux, 12-Feb-2017)

Ref Expression
Hypotheses dstfrv.1 
|- ( ph -> P e. Prob )
dstfrv.2 
|- ( ph -> X e. ( rRndVar ` P ) )
Assertion dstfrvunirn 
|- ( ph -> U. ran ( n e. NN |-> ( X oRVC <_ n ) ) = U. dom P )

Proof

Step Hyp Ref Expression
1 dstfrv.1 
 |-  ( ph -> P e. Prob )
2 dstfrv.2 
 |-  ( ph -> X e. ( rRndVar ` P ) )
3 1red 
 |-  ( ( ph /\ x e. U. dom P ) -> 1 e. RR )
4 1 2 rrvvf 
 |-  ( ph -> X : U. dom P --> RR )
5 4 ffvelrnda 
 |-  ( ( ph /\ x e. U. dom P ) -> ( X ` x ) e. RR )
6 3 5 ifcld 
 |-  ( ( ph /\ x e. U. dom P ) -> if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) e. RR )
7 breq2 
 |-  ( 1 = if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) -> ( 1 <_ 1 <-> 1 <_ if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) )
8 breq2 
 |-  ( ( X ` x ) = if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) -> ( 1 <_ ( X ` x ) <-> 1 <_ if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) )
9 1le1 
 |-  1 <_ 1
10 9 a1i 
 |-  ( ( ( ph /\ x e. U. dom P ) /\ ( X ` x ) < 1 ) -> 1 <_ 1 )
11 3 5 lenltd 
 |-  ( ( ph /\ x e. U. dom P ) -> ( 1 <_ ( X ` x ) <-> -. ( X ` x ) < 1 ) )
12 11 biimpar 
 |-  ( ( ( ph /\ x e. U. dom P ) /\ -. ( X ` x ) < 1 ) -> 1 <_ ( X ` x ) )
13 7 8 10 12 ifbothda 
 |-  ( ( ph /\ x e. U. dom P ) -> 1 <_ if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) )
14 flge1nn 
 |-  ( ( if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) e. RR /\ 1 <_ if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) -> ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) e. NN )
15 6 13 14 syl2anc 
 |-  ( ( ph /\ x e. U. dom P ) -> ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) e. NN )
16 15 peano2nnd 
 |-  ( ( ph /\ x e. U. dom P ) -> ( ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) + 1 ) e. NN )
17 1 adantr 
 |-  ( ( ph /\ x e. U. dom P ) -> P e. Prob )
18 2 adantr 
 |-  ( ( ph /\ x e. U. dom P ) -> X e. ( rRndVar ` P ) )
19 16 nnred 
 |-  ( ( ph /\ x e. U. dom P ) -> ( ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) + 1 ) e. RR )
20 simpr 
 |-  ( ( ph /\ x e. U. dom P ) -> x e. U. dom P )
21 breq2 
 |-  ( 1 = if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) -> ( ( X ` x ) <_ 1 <-> ( X ` x ) <_ if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) )
22 breq2 
 |-  ( ( X ` x ) = if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) -> ( ( X ` x ) <_ ( X ` x ) <-> ( X ` x ) <_ if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) )
23 5 adantr 
 |-  ( ( ( ph /\ x e. U. dom P ) /\ ( X ` x ) < 1 ) -> ( X ` x ) e. RR )
24 1red 
 |-  ( ( ( ph /\ x e. U. dom P ) /\ ( X ` x ) < 1 ) -> 1 e. RR )
25 simpr 
 |-  ( ( ( ph /\ x e. U. dom P ) /\ ( X ` x ) < 1 ) -> ( X ` x ) < 1 )
26 23 24 25 ltled 
 |-  ( ( ( ph /\ x e. U. dom P ) /\ ( X ` x ) < 1 ) -> ( X ` x ) <_ 1 )
27 5 leidd 
 |-  ( ( ph /\ x e. U. dom P ) -> ( X ` x ) <_ ( X ` x ) )
28 27 adantr 
 |-  ( ( ( ph /\ x e. U. dom P ) /\ -. ( X ` x ) < 1 ) -> ( X ` x ) <_ ( X ` x ) )
29 21 22 26 28 ifbothda 
 |-  ( ( ph /\ x e. U. dom P ) -> ( X ` x ) <_ if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) )
30 fllep1 
 |-  ( if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) e. RR -> if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) <_ ( ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) + 1 ) )
31 6 30 syl 
 |-  ( ( ph /\ x e. U. dom P ) -> if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) <_ ( ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) + 1 ) )
32 5 6 19 29 31 letrd 
 |-  ( ( ph /\ x e. U. dom P ) -> ( X ` x ) <_ ( ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) + 1 ) )
33 17 18 19 20 32 dstfrvel 
 |-  ( ( ph /\ x e. U. dom P ) -> x e. ( X oRVC <_ ( ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) + 1 ) ) )
34 oveq2 
 |-  ( n = ( ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) + 1 ) -> ( X oRVC <_ n ) = ( X oRVC <_ ( ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) + 1 ) ) )
35 34 eleq2d 
 |-  ( n = ( ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) + 1 ) -> ( x e. ( X oRVC <_ n ) <-> x e. ( X oRVC <_ ( ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) + 1 ) ) ) )
36 35 rspcev 
 |-  ( ( ( ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) + 1 ) e. NN /\ x e. ( X oRVC <_ ( ( |_ ` if ( ( X ` x ) < 1 , 1 , ( X ` x ) ) ) + 1 ) ) ) -> E. n e. NN x e. ( X oRVC <_ n ) )
37 16 33 36 syl2anc 
 |-  ( ( ph /\ x e. U. dom P ) -> E. n e. NN x e. ( X oRVC <_ n ) )
38 37 ex 
 |-  ( ph -> ( x e. U. dom P -> E. n e. NN x e. ( X oRVC <_ n ) ) )
39 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> P e. Prob )
40 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. ( rRndVar ` P ) )
41 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
42 41 nnred 
 |-  ( ( ph /\ n e. NN ) -> n e. RR )
43 39 40 42 orvclteel 
 |-  ( ( ph /\ n e. NN ) -> ( X oRVC <_ n ) e. dom P )
44 elunii 
 |-  ( ( x e. ( X oRVC <_ n ) /\ ( X oRVC <_ n ) e. dom P ) -> x e. U. dom P )
45 44 expcom 
 |-  ( ( X oRVC <_ n ) e. dom P -> ( x e. ( X oRVC <_ n ) -> x e. U. dom P ) )
46 43 45 syl 
 |-  ( ( ph /\ n e. NN ) -> ( x e. ( X oRVC <_ n ) -> x e. U. dom P ) )
47 46 rexlimdva 
 |-  ( ph -> ( E. n e. NN x e. ( X oRVC <_ n ) -> x e. U. dom P ) )
48 38 47 impbid 
 |-  ( ph -> ( x e. U. dom P <-> E. n e. NN x e. ( X oRVC <_ n ) ) )
49 eliun 
 |-  ( x e. U_ n e. NN ( X oRVC <_ n ) <-> E. n e. NN x e. ( X oRVC <_ n ) )
50 48 49 bitr4di 
 |-  ( ph -> ( x e. U. dom P <-> x e. U_ n e. NN ( X oRVC <_ n ) ) )
51 50 eqrdv 
 |-  ( ph -> U. dom P = U_ n e. NN ( X oRVC <_ n ) )
52 ovex 
 |-  ( X oRVC <_ n ) e. _V
53 52 dfiun3 
 |-  U_ n e. NN ( X oRVC <_ n ) = U. ran ( n e. NN |-> ( X oRVC <_ n ) )
54 51 53 eqtr2di 
 |-  ( ph -> U. ran ( n e. NN |-> ( X oRVC <_ n ) ) = U. dom P )