orvccel - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > orvccel		Structured version Visualization version GIF version

Theorem orvccel 34454

Description: If the relation produces closed sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)

**Hypotheses**
Ref	Expression
orvccel.1	⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)
orvccel.2	⊢ (𝜑 → 𝐽 ∈ Top)
orvccel.3	⊢ (𝜑 → 𝑋 ∈ (𝑆MblFnM(sigaGen‘𝐽)))
orvccel.4	⊢ (𝜑 → 𝐴 ∈ 𝑉)
orvccel.5	⊢ (𝜑 → {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴} ∈ (Clsd‘𝐽))

**Assertion**
Ref	Expression
orvccel	⊢ (𝜑 → (𝑋∘_RV/𝑐𝑅𝐴) ∈ 𝑆)

Distinct variable groups: 𝑦,𝐴 𝑦,𝑅 𝑦,𝑋 𝑦,𝐽 Allowed substitution hints: 𝜑(𝑦) 𝑆(𝑦) 𝑉(𝑦)

**Proof of Theorem orvccel**
Step	Hyp	Ref	Expression
1		orvccel.1	. . 3 ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)
2		orvccel.2	. . 3 ⊢ (𝜑 → 𝐽 ∈ Top)
3		orvccel.3	. . 3 ⊢ (𝜑 → 𝑋 ∈ (𝑆MblFnM(sigaGen‘𝐽)))
4		orvccel.4	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
5	1, 2, 3, 4	orvcval4 34452	. 2 ⊢ (𝜑 → (𝑋∘_RV/𝑐𝑅𝐴) = (^◡𝑋 “ {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴}))
6	2	sgsiga 34132	. . 3 ⊢ (𝜑 → (sigaGen‘𝐽) ∈ ∪ ran sigAlgebra)
7		cldssbrsiga 34177	. . . . 5 ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) ⊆ (sigaGen‘𝐽))
8	2, 7	syl 17	. . . 4 ⊢ (𝜑 → (Clsd‘𝐽) ⊆ (sigaGen‘𝐽))
9		orvccel.5	. . . 4 ⊢ (𝜑 → {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴} ∈ (Clsd‘𝐽))
10	8, 9	sseldd 3947	. . 3 ⊢ (𝜑 → {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴} ∈ (sigaGen‘𝐽))
11	1, 6, 3, 10	mbfmcnvima 34246	. 2 ⊢ (𝜑 → (^◡𝑋 “ {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴}) ∈ 𝑆)
12	5, 11	eqeltrd 2828	1 ⊢ (𝜑 → (𝑋∘_RV/𝑐𝑅𝐴) ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2109 {crab 3405 ⊆ wss 3914 ∪ cuni 4871 class class class wbr 5107 ^◡ccnv 5637 ran crn 5639 “ cima 5641 ‘cfv 6511 (class class class)co 7387 Topctop 22780 Clsdccld 22903 sigAlgebracsiga 34098 sigaGencsigagen 34128 MblFnMcmbfm 34239 ∘_RV/𝑐corvc 34447

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-ac2 10416

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-iin 4958 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-er 8671 df-map 8801 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-oi 9463 df-dju 9854 df-card 9892 df-acn 9895 df-ac 10069 df-top 22781 df-cld 22906 df-siga 34099 df-sigagen 34129 df-mbfm 34240 df-orvc 34448

This theorem is referenced by: orrvccel 34458

W3C validator