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	$⊢ φ \to P \in Prob$
	dstfrv.2	$⊢ φ \to X \in {RndVar}_{ℝ} (P)$
Assertion	dstfrvunirn	$⊢ φ \to ⋃ ran (n \in ℕ ⟼ X \leq_{RV/c} n) = ⋃ dom P$

Proof

Step	Hyp	Ref	Expression
1		dstfrv.1	$⊢ φ \to P \in Prob$
2		dstfrv.2	$⊢ φ \to X \in {RndVar}_{ℝ} (P)$
3		1red	$⊢ (φ \land x \in ⋃ dom P) \to 1 \in ℝ$
4	1 2	rrvvf	$⊢ φ \to X : ⋃ dom P ⟶ ℝ$
5	4	ffvelrnda	$⊢ (φ \land x \in ⋃ dom P) \to X (x) \in ℝ$
6	3 5	ifcld	$⊢ (φ \land x \in ⋃ dom P) \to if (X (x) < 1, 1, X (x)) \in ℝ$
7		breq2	$⊢ 1 = if (X (x) < 1, 1, X (x)) \to (1 \leq 1 \leftrightarrow 1 \leq if (X (x) < 1, 1, X (x)))$
8		breq2	$⊢ X (x) = if (X (x) < 1, 1, X (x)) \to (1 \leq X (x) \leftrightarrow 1 \leq if (X (x) < 1, 1, X (x)))$
9		1le1	$⊢ 1 \leq 1$
10	9	a1i	$⊢ ((φ \land x \in ⋃ dom P) \land X (x) < 1) \to 1 \leq 1$
11	3 5	lenltd	$⊢ (φ \land x \in ⋃ dom P) \to (1 \leq X (x) \leftrightarrow \neg X (x) < 1)$
12	11	biimpar	$⊢ ((φ \land x \in ⋃ dom P) \land \neg X (x) < 1) \to 1 \leq X (x)$
13	7 8 10 12	ifbothda	$⊢ (φ \land x \in ⋃ dom P) \to 1 \leq if (X (x) < 1, 1, X (x))$
14		flge1nn	$⊢ (if (X (x) < 1, 1, X (x)) \in ℝ \land 1 \leq if (X (x) < 1, 1, X (x))) \to ⌊if (X (x) < 1, 1, X (x))⌋ \in ℕ$
15	6 13 14	syl2anc	$⊢ (φ \land x \in ⋃ dom P) \to ⌊if (X (x) < 1, 1, X (x))⌋ \in ℕ$
16	15	peano2nnd	$⊢ (φ \land x \in ⋃ dom P) \to ⌊if (X (x) < 1, 1, X (x))⌋ + 1 \in ℕ$
17	1	adantr	$⊢ (φ \land x \in ⋃ dom P) \to P \in Prob$
18	2	adantr	$⊢ (φ \land x \in ⋃ dom P) \to X \in {RndVar}_{ℝ} (P)$
19	16	nnred	$⊢ (φ \land x \in ⋃ dom P) \to ⌊if (X (x) < 1, 1, X (x))⌋ + 1 \in ℝ$
20		simpr	$⊢ (φ \land x \in ⋃ dom P) \to x \in ⋃ dom P$
21		breq2	$⊢ 1 = if (X (x) < 1, 1, X (x)) \to (X (x) \leq 1 \leftrightarrow X (x) \leq if (X (x) < 1, 1, X (x)))$
22		breq2	$⊢ X (x) = if (X (x) < 1, 1, X (x)) \to (X (x) \leq X (x) \leftrightarrow X (x) \leq if (X (x) < 1, 1, X (x)))$
23	5	adantr	$⊢ ((φ \land x \in ⋃ dom P) \land X (x) < 1) \to X (x) \in ℝ$
24		1red	$⊢ ((φ \land x \in ⋃ dom P) \land X (x) < 1) \to 1 \in ℝ$
25		simpr	$⊢ ((φ \land x \in ⋃ dom P) \land X (x) < 1) \to X (x) < 1$
26	23 24 25	ltled	$⊢ ((φ \land x \in ⋃ dom P) \land X (x) < 1) \to X (x) \leq 1$
27	5	leidd	$⊢ (φ \land x \in ⋃ dom P) \to X (x) \leq X (x)$
28	27	adantr	$⊢ ((φ \land x \in ⋃ dom P) \land \neg X (x) < 1) \to X (x) \leq X (x)$
29	21 22 26 28	ifbothda	$⊢ (φ \land x \in ⋃ dom P) \to X (x) \leq if (X (x) < 1, 1, X (x))$
30		fllep1	$⊢ if (X (x) < 1, 1, X (x)) \in ℝ \to if (X (x) < 1, 1, X (x)) \leq ⌊if (X (x) < 1, 1, X (x))⌋ + 1$
31	6 30	syl	$⊢ (φ \land x \in ⋃ dom P) \to if (X (x) < 1, 1, X (x)) \leq ⌊if (X (x) < 1, 1, X (x))⌋ + 1$
32	5 6 19 29 31	letrd	$⊢ (φ \land x \in ⋃ dom P) \to X (x) \leq ⌊if (X (x) < 1, 1, X (x))⌋ + 1$
33	17 18 19 20 32	dstfrvel	$⊢ (φ \land x \in ⋃ dom P) \to x \in (X \leq_{RV/c} (⌊if (X (x) < 1, 1, X (x))⌋ + 1))$
34		oveq2	$⊢ n = ⌊if (X (x) < 1, 1, X (x))⌋ + 1 \to X \leq_{RV/c} n = X \leq_{RV/c} (⌊if (X (x) < 1, 1, X (x))⌋ + 1)$
35	34	eleq2d	$⊢ n = ⌊if (X (x) < 1, 1, X (x))⌋ + 1 \to (x \in (X \leq_{RV/c} n) \leftrightarrow x \in (X \leq_{RV/c} (⌊if (X (x) < 1, 1, X (x))⌋ + 1)))$
36	35	rspcev	$⊢ (⌊if (X (x) < 1, 1, X (x))⌋ + 1 \in ℕ \land x \in (X \leq_{RV/c} (⌊if (X (x) < 1, 1, X (x))⌋ + 1))) \to \exists n \in ℕ x \in (X \leq_{RV/c} n)$
37	16 33 36	syl2anc	$⊢ (φ \land x \in ⋃ dom P) \to \exists n \in ℕ x \in (X \leq_{RV/c} n)$
38	37	ex	$⊢ φ \to (x \in ⋃ dom P \to \exists n \in ℕ x \in (X \leq_{RV/c} n))$
39	1	adantr	$⊢ (φ \land n \in ℕ) \to P \in Prob$
40	2	adantr	$⊢ (φ \land n \in ℕ) \to X \in {RndVar}_{ℝ} (P)$
41		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
42	41	nnred	$⊢ (φ \land n \in ℕ) \to n \in ℝ$
43	39 40 42	orvclteel	$⊢ (φ \land n \in ℕ) \to X \leq_{RV/c} n \in dom P$
44		elunii	$⊢ (x \in (X \leq_{RV/c} n) \land X \leq_{RV/c} n \in dom P) \to x \in ⋃ dom P$
45	44	expcom	$⊢ X \leq_{RV/c} n \in dom P \to (x \in (X \leq_{RV/c} n) \to x \in ⋃ dom P)$
46	43 45	syl	$⊢ (φ \land n \in ℕ) \to (x \in (X \leq_{RV/c} n) \to x \in ⋃ dom P)$
47	46	rexlimdva	$⊢ φ \to (\exists n \in ℕ x \in (X \leq_{RV/c} n) \to x \in ⋃ dom P)$
48	38 47	impbid	$⊢ φ \to (x \in ⋃ dom P \leftrightarrow \exists n \in ℕ x \in (X \leq_{RV/c} n))$
49		eliun	$⊢ x \in ⋃_{n \in ℕ} (X \leq_{RV/c} n) \leftrightarrow \exists n \in ℕ x \in (X \leq_{RV/c} n)$
50	48 49	bitr4di	$⊢ φ \to (x \in ⋃ dom P \leftrightarrow x \in ⋃_{n \in ℕ} (X \leq_{RV/c} n))$
51	50	eqrdv	$⊢ φ \to ⋃ dom P = ⋃_{n \in ℕ} (X \leq_{RV/c} n)$
52		ovex	$⊢ X \leq_{RV/c} n \in V$
53	52	dfiun3	$⊢ ⋃_{n \in ℕ} (X \leq_{RV/c} n) = ⋃ ran (n \in ℕ ⟼ X \leq_{RV/c} n)$
54	51 53	eqtr2di	$⊢ φ \to ⋃ ran (n \in ℕ ⟼ X \leq_{RV/c} n) = ⋃ dom P$

Metamath Proof Explorer

Theorem dstfrvunirn

Proof