Theorem iunpreima

Description: Preimage of an indexed union. (Contributed by Thierry Arnoux, 27-Mar-2018)

	Ref	Expression
Assertion	iunpreima	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eliun	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
2	1	a1i	⊢ ( Fun 𝐹 → ( ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ) )
3	2	rabbidv	⊢ ( Fun 𝐹 → { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 } = { 𝑦 ∈ dom 𝐹 ∣ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } )
4		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
5		fncnvima2	⊢ ( 𝐹 Fn dom 𝐹 → ( ◡ 𝐹 “ ∪ 𝑥 ∈ 𝐴 𝐵 ) = { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 } )
6	4 5	sylbi	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ∪ 𝑥 ∈ 𝐴 𝐵 ) = { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 } )
7		iunrab	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } = { 𝑦 ∈ dom 𝐹 ∣ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 }
8	7	a1i	⊢ ( Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } = { 𝑦 ∈ dom 𝐹 ∣ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } )
9	3 6 8	3eqtr4d	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } )
10		fncnvima2	⊢ ( 𝐹 Fn dom 𝐹 → ( ◡ 𝐹 “ 𝐵 ) = { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } )
11	4 10	sylbi	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ 𝐵 ) = { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } )
12	11	iuneq2d	⊢ ( Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝐵 ) = ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } )
13	9 12	eqtr4d	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝐵 ) )