This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 → ( ◡ 𝐹 “ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝐵 ) )