orvcval4

Description: The value of the preimage mapping operator can be restricted to preimages in the base set of the topology. Cf. orvcval . (Contributed by Thierry Arnoux, 21-Jan-2017)

	Ref	Expression
Hypotheses	orvccel.1	$⊢ φ \to S \in ⋃ ran sigAlgebra$
	orvccel.2	$⊢ φ \to J \in Top$
	orvccel.3	$⊢ φ \to X \in (S {MblFn}_{μ} 𝛔 (J))$
	orvccel.4	$⊢ φ \to A \in V$
Assertion	orvcval4	$⊢ φ \to X R_{RV/c} A = X^{-1} [\{y \in ⋃ J \| y R A\}]$

Proof

Step	Hyp	Ref	Expression
1		orvccel.1	$⊢ φ \to S \in ⋃ ran sigAlgebra$
2		orvccel.2	$⊢ φ \to J \in Top$
3		orvccel.3	$⊢ φ \to X \in (S {MblFn}_{μ} 𝛔 (J))$
4		orvccel.4	$⊢ φ \to A \in V$
5	2	sgsiga	$⊢ φ \to 𝛔 (J) \in ⋃ ran sigAlgebra$
6	1 5 3	isanmbfm	$⊢ φ \to X \in ⋃ ran {MblFn}_{μ}$
7	6	mbfmfun	$⊢ φ \to Fun X$
8	1 5 3	mbfmf	$⊢ φ \to X : ⋃ S ⟶ ⋃ 𝛔 (J)$
9		elex	$⊢ J \in Top \to J \in V$
10		unisg	$⊢ J \in V \to ⋃ 𝛔 (J) = ⋃ J$
11	2 9 10	3syl	$⊢ φ \to ⋃ 𝛔 (J) = ⋃ J$
12	11	feq3d	$⊢ φ \to (X : ⋃ S ⟶ ⋃ 𝛔 (J) \leftrightarrow X : ⋃ S ⟶ ⋃ J)$
13	8 12	mpbid	$⊢ φ \to X : ⋃ S ⟶ ⋃ J$
14	13	frnd	$⊢ φ \to ran X \subseteq ⋃ J$
15		fimacnvinrn2	$⊢ (Fun X \land ran X \subseteq ⋃ J) \to X^{-1} [\{y \| y R A\}] = X^{-1} [\{y \| y R A\} \cap ⋃ J]$
16	7 14 15	syl2anc	$⊢ φ \to X^{-1} [\{y \| y R A\}] = X^{-1} [\{y \| y R A\} \cap ⋃ J]$
17	7 3 4	orvcval	$⊢ φ \to X R_{RV/c} A = X^{-1} [\{y \| y R A\}]$
18		dfrab2	$⊢ \{y \in ⋃ J \| y R A\} = \{y \| y R A\} \cap ⋃ J$
19	18	a1i	$⊢ φ \to \{y \in ⋃ J \| y R A\} = \{y \| y R A\} \cap ⋃ J$
20	19	imaeq2d	$⊢ φ \to X^{-1} [\{y \in ⋃ J \| y R A\}] = X^{-1} [\{y \| y R A\} \cap ⋃ J]$
21	16 17 20	3eqtr4d	$⊢ φ \to X R_{RV/c} A = X^{-1} [\{y \in ⋃ J \| y R A\}]$

Metamath Proof Explorer

Theorem orvcval4

Proof