Theorem sibff

Description: A simple function is a function. (Contributed by Thierry Arnoux, 19-Feb-2018)

	Ref	Expression
Hypotheses	sitgval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
	sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
	sitgval.0	⊢ 0 = ( 0g ‘ 𝑊 )
	sitgval.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
	sitgval.h	⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
	sitgval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
	sitgval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
	sibfmbl.1	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
Assertion	sibff	⊢ ( 𝜑 → 𝐹 : ∪ dom 𝑀 ⟶ ∪ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3		sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
4		sitgval.0	⊢ 0 = ( 0g ‘ 𝑊 )
5		sitgval.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		sitgval.h	⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
7		sitgval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
8		sitgval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
9		sibfmbl.1	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
10		dmmeas	⊢ ( 𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra )
11	8 10	syl	⊢ ( 𝜑 → dom 𝑀 ∈ ∪ ran sigAlgebra )
12		fvexd	⊢ ( 𝜑 → ( TopOpen ‘ 𝑊 ) ∈ V )
13	2 12	eqeltrid	⊢ ( 𝜑 → 𝐽 ∈ V )
14	13	sgsiga	⊢ ( 𝜑 → ( sigaGen ‘ 𝐽 ) ∈ ∪ ran sigAlgebra )
15	3 14	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
16	1 2 3 4 5 6 7 8 9	sibfmbl	⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) )
17	11 15 16	mbfmf	⊢ ( 𝜑 → 𝐹 : ∪ dom 𝑀 ⟶ ∪ 𝑆 )
18	3	unieqi	⊢ ∪ 𝑆 = ∪ ( sigaGen ‘ 𝐽 )
19		unisg	⊢ ( 𝐽 ∈ V → ∪ ( sigaGen ‘ 𝐽 ) = ∪ 𝐽 )
20	13 19	syl	⊢ ( 𝜑 → ∪ ( sigaGen ‘ 𝐽 ) = ∪ 𝐽 )
21	18 20	syl5eq	⊢ ( 𝜑 → ∪ 𝑆 = ∪ 𝐽 )
22	21	feq3d	⊢ ( 𝜑 → ( 𝐹 : ∪ dom 𝑀 ⟶ ∪ 𝑆 ↔ 𝐹 : ∪ dom 𝑀 ⟶ ∪ 𝐽 ) )
23	17 22	mpbid	⊢ ( 𝜑 → 𝐹 : ∪ dom 𝑀 ⟶ ∪ 𝐽 )