Theorem 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	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
	orvccel.2	⊢ ( 𝜑 → 𝐽 ∈ Top )
	orvccel.3	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑆 MblFnM ( sigaGen ‘ 𝐽 ) ) )
	orvccel.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	orvcval4	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) = ( ◡ 𝑋 “ { 𝑦 ∈ ∪ 𝐽 ∣ 𝑦 𝑅 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		orvccel.1	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
2		orvccel.2	⊢ ( 𝜑 → 𝐽 ∈ Top )
3		orvccel.3	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑆 MblFnM ( sigaGen ‘ 𝐽 ) ) )
4		orvccel.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5	3	isanmbfm	⊢ ( 𝜑 → 𝑋 ∈ ∪ ran MblFnM )
6	5	mbfmfun	⊢ ( 𝜑 → Fun 𝑋 )
7	2	sgsiga	⊢ ( 𝜑 → ( sigaGen ‘ 𝐽 ) ∈ ∪ ran sigAlgebra )
8	1 7 3	mbfmf	⊢ ( 𝜑 → 𝑋 : ∪ 𝑆 ⟶ ∪ ( sigaGen ‘ 𝐽 ) )
9		elex	⊢ ( 𝐽 ∈ Top → 𝐽 ∈ V )
10		unisg	⊢ ( 𝐽 ∈ V → ∪ ( sigaGen ‘ 𝐽 ) = ∪ 𝐽 )
11	2 9 10	3syl	⊢ ( 𝜑 → ∪ ( sigaGen ‘ 𝐽 ) = ∪ 𝐽 )
12	11	feq3d	⊢ ( 𝜑 → ( 𝑋 : ∪ 𝑆 ⟶ ∪ ( sigaGen ‘ 𝐽 ) ↔ 𝑋 : ∪ 𝑆 ⟶ ∪ 𝐽 ) )
13	8 12	mpbid	⊢ ( 𝜑 → 𝑋 : ∪ 𝑆 ⟶ ∪ 𝐽 )
14	13	frnd	⊢ ( 𝜑 → ran 𝑋 ⊆ ∪ 𝐽 )
15		fimacnvinrn2	⊢ ( ( Fun 𝑋 ∧ ran 𝑋 ⊆ ∪ 𝐽 ) → ( ◡ 𝑋 “ { 𝑦 ∣ 𝑦 𝑅 𝐴 } ) = ( ◡ 𝑋 “ ( { 𝑦 ∣ 𝑦 𝑅 𝐴 } ∩ ∪ 𝐽 ) ) )
16	6 14 15	syl2anc	⊢ ( 𝜑 → ( ◡ 𝑋 “ { 𝑦 ∣ 𝑦 𝑅 𝐴 } ) = ( ◡ 𝑋 “ ( { 𝑦 ∣ 𝑦 𝑅 𝐴 } ∩ ∪ 𝐽 ) ) )
17	6 3 4	orvcval	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) = ( ◡ 𝑋 “ { 𝑦 ∣ 𝑦 𝑅 𝐴 } ) )
18		dfrab2	⊢ { 𝑦 ∈ ∪ 𝐽 ∣ 𝑦 𝑅 𝐴 } = ( { 𝑦 ∣ 𝑦 𝑅 𝐴 } ∩ ∪ 𝐽 )
19	18	a1i	⊢ ( 𝜑 → { 𝑦 ∈ ∪ 𝐽 ∣ 𝑦 𝑅 𝐴 } = ( { 𝑦 ∣ 𝑦 𝑅 𝐴 } ∩ ∪ 𝐽 ) )
20	19	imaeq2d	⊢ ( 𝜑 → ( ◡ 𝑋 “ { 𝑦 ∈ ∪ 𝐽 ∣ 𝑦 𝑅 𝐴 } ) = ( ◡ 𝑋 “ ( { 𝑦 ∣ 𝑦 𝑅 𝐴 } ∩ ∪ 𝐽 ) ) )
21	16 17 20	3eqtr4d	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) = ( ◡ 𝑋 “ { 𝑦 ∈ ∪ 𝐽 ∣ 𝑦 𝑅 𝐴 } ) )