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 ⊢ ( 𝜑 → 𝑃 ∈ Prob )
dstfrv.2 ⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
Assertion dstfrvunirn ( 𝜑 → ∪ ran ( 𝑛 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ) = ∪ dom 𝑃 )

Proof

Step Hyp Ref Expression
1 dstfrv.1 ⊢ ( 𝜑 → 𝑃 ∈ Prob )
2 dstfrv.2 ⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3 1red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → 1 ∈ ℝ )
4 1 2 rrvvf ⊢ ( 𝜑 → 𝑋 : ∪ dom 𝑃 ⟶ ℝ )
5 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → ( 𝑋 ‘ 𝑥 ) ∈ ℝ )
6 3 5 ifcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ∈ ℝ )
7 breq2 ⊢ ( 1 = if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) → ( 1 ≤ 1 ↔ 1 ≤ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) )
8 breq2 ⊢ ( ( 𝑋 ‘ 𝑥 ) = if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) → ( 1 ≤ ( 𝑋 ‘ 𝑥 ) ↔ 1 ≤ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) )
9 1le1 ⊢ 1 ≤ 1
10 9 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) ∧ ( 𝑋 ‘ 𝑥 ) < 1 ) → 1 ≤ 1 )
11 3 5 lenltd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → ( 1 ≤ ( 𝑋 ‘ 𝑥 ) ↔ ¬ ( 𝑋 ‘ 𝑥 ) < 1 ) )
12 11 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) ∧ ¬ ( 𝑋 ‘ 𝑥 ) < 1 ) → 1 ≤ ( 𝑋 ‘ 𝑥 ) )
13 7 8 10 12 ifbothda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → 1 ≤ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) )
14 flge1nn ⊢ ( ( if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ∈ ℝ ∧ 1 ≤ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) → ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) ∈ ℕ )
15 6 13 14 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) ∈ ℕ )
16 15 peano2nnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → ( ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) + 1 ) ∈ ℕ )
17 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → 𝑃 ∈ Prob )
18 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
19 16 nnred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → ( ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) + 1 ) ∈ ℝ )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → 𝑥 ∈ ∪ dom 𝑃 )
21 breq2 ⊢ ( 1 = if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) → ( ( 𝑋 ‘ 𝑥 ) ≤ 1 ↔ ( 𝑋 ‘ 𝑥 ) ≤ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) )
22 breq2 ⊢ ( ( 𝑋 ‘ 𝑥 ) = if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) → ( ( 𝑋 ‘ 𝑥 ) ≤ ( 𝑋 ‘ 𝑥 ) ↔ ( 𝑋 ‘ 𝑥 ) ≤ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) )
23 5 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) ∧ ( 𝑋 ‘ 𝑥 ) < 1 ) → ( 𝑋 ‘ 𝑥 ) ∈ ℝ )
24 1red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) ∧ ( 𝑋 ‘ 𝑥 ) < 1 ) → 1 ∈ ℝ )
25 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) ∧ ( 𝑋 ‘ 𝑥 ) < 1 ) → ( 𝑋 ‘ 𝑥 ) < 1 )
26 23 24 25 ltled ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) ∧ ( 𝑋 ‘ 𝑥 ) < 1 ) → ( 𝑋 ‘ 𝑥 ) ≤ 1 )
27 5 leidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → ( 𝑋 ‘ 𝑥 ) ≤ ( 𝑋 ‘ 𝑥 ) )
28 27 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) ∧ ¬ ( 𝑋 ‘ 𝑥 ) < 1 ) → ( 𝑋 ‘ 𝑥 ) ≤ ( 𝑋 ‘ 𝑥 ) )
29 21 22 26 28 ifbothda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → ( 𝑋 ‘ 𝑥 ) ≤ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) )
30 fllep1 ⊢ ( if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ∈ ℝ → if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ≤ ( ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) + 1 ) )
31 6 30 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ≤ ( ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) + 1 ) )
32 5 6 19 29 31 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → ( 𝑋 ‘ 𝑥 ) ≤ ( ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) + 1 ) )
33 17 18 19 20 32 dstfrvel ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → 𝑥 ∈ ( 𝑋 ∘RV/𝑐 ≤ ( ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) + 1 ) ) )
34 oveq2 ⊢ ( 𝑛 = ( ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) + 1 ) → ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) = ( 𝑋 ∘RV/𝑐 ≤ ( ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) + 1 ) ) )
35 34 eleq2d ⊢ ( 𝑛 = ( ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) + 1 ) → ( 𝑥 ∈ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ↔ 𝑥 ∈ ( 𝑋 ∘RV/𝑐 ≤ ( ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) + 1 ) ) ) )
36 35 rspcev ⊢ ( ( ( ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) + 1 ) ∈ ℕ ∧ 𝑥 ∈ ( 𝑋 ∘RV/𝑐 ≤ ( ( ⌊ ‘ if ( ( 𝑋 ‘ 𝑥 ) < 1 , 1 , ( 𝑋 ‘ 𝑥 ) ) ) + 1 ) ) ) → ∃ 𝑛 ∈ ℕ 𝑥 ∈ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) )
37 16 33 36 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ dom 𝑃 ) → ∃ 𝑛 ∈ ℕ 𝑥 ∈ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) )
38 37 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ dom 𝑃 → ∃ 𝑛 ∈ ℕ 𝑥 ∈ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ) )
39 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑃 ∈ Prob )
40 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
42 41 nnred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ )
43 39 40 42 orvclteel ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ∈ dom 𝑃 )
44 elunii ⊢ ( ( 𝑥 ∈ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ∧ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ∈ dom 𝑃 ) → 𝑥 ∈ ∪ dom 𝑃 )
45 44 expcom ⊢ ( ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ∈ dom 𝑃 → ( 𝑥 ∈ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) → 𝑥 ∈ ∪ dom 𝑃 ) )
46 43 45 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ∈ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) → 𝑥 ∈ ∪ dom 𝑃 ) )
47 46 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ 𝑥 ∈ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) → 𝑥 ∈ ∪ dom 𝑃 ) )
48 38 47 impbid ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ dom 𝑃 ↔ ∃ 𝑛 ∈ ℕ 𝑥 ∈ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ) )
49 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ℕ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ 𝑥 ∈ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) )
50 48 49 bitr4di ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ dom 𝑃 ↔ 𝑥 ∈ ∪ 𝑛 ∈ ℕ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ) )
51 50 eqrdv ⊢ ( 𝜑 → ∪ dom 𝑃 = ∪ 𝑛 ∈ ℕ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) )
52 ovex ⊢ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ∈ V
53 52 dfiun3 ⊢ ∪ 𝑛 ∈ ℕ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) = ∪ ran ( 𝑛 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) )
54 51 53 eqtr2di ⊢ ( 𝜑 → ∪ ran ( 𝑛 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ) = ∪ dom 𝑃 )