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

Metamath Proof Explorer

Theorem unipreima

Description: Preimage of a class union. (Contributed by Thierry Arnoux, 7-Feb-2017)

Ref Expression
Assertion unipreima ( Fun 𝐹 → ( ◡ 𝐹 “ ∪ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 funfn ⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
2 r19.42v ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ↔ ( 𝑦 ∈ dom 𝐹 ∧ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) )
3 2 bicomi ⊢ ( ( 𝑦 ∈ dom 𝐹 ∧ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) )
4 3 a1i ⊢ ( 𝐹 Fn dom 𝐹 → ( ( 𝑦 ∈ dom 𝐹 ∧ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) )
5 eluni2 ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 )
6 5 anbi2i ⊢ ( ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐴 ) ↔ ( 𝑦 ∈ dom 𝐹 ∧ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) )
7 6 a1i ⊢ ( 𝐹 Fn dom 𝐹 → ( ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐴 ) ↔ ( 𝑦 ∈ dom 𝐹 ∧ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) )
8 elpreima ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ↔ ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) )
9 8 rexbidv ⊢ ( 𝐹 Fn dom 𝐹 → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) )
10 4 7 9 3bitr4d ⊢ ( 𝐹 Fn dom 𝐹 → ( ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
11 elpreima ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑦 ∈ ( ◡ 𝐹 “ ∪ 𝐴 ) ↔ ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐴 ) ) )
12 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) )
13 12 a1i ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
14 10 11 13 3bitr4d ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑦 ∈ ( ◡ 𝐹 “ ∪ 𝐴 ) ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) ) )
15 14 eqrdv ⊢ ( 𝐹 Fn dom 𝐹 → ( ◡ 𝐹 “ ∪ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) )
16 1 15 sylbi ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ∪ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) )