Metamath Proof Explorer

Theorem unipreima

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

Ref Expression
Assertion unipreima ⊢ Fun ⁡ F → F -1 ⋃ A = ⋃ x ∈ A F -1 x

Proof

Step Hyp Ref Expression
1 funfn ⊢ Fun ⁡ F ↔ F Fn dom ⁡ F
2 r19.42v ⊢ ∃ x ∈ A y ∈ dom ⁡ F ∧ F ⁡ y ∈ x ↔ y ∈ dom ⁡ F ∧ ∃ x ∈ A F ⁡ y ∈ x
3 2 bicomi ⊢ y ∈ dom ⁡ F ∧ ∃ x ∈ A F ⁡ y ∈ x ↔ ∃ x ∈ A y ∈ dom ⁡ F ∧ F ⁡ y ∈ x
4 3 a1i ⊢ F Fn dom ⁡ F → y ∈ dom ⁡ F ∧ ∃ x ∈ A F ⁡ y ∈ x ↔ ∃ x ∈ A y ∈ dom ⁡ F ∧ F ⁡ y ∈ x
5 eluni2 ⊢ F ⁡ y ∈ ⋃ A ↔ ∃ x ∈ A F ⁡ y ∈ x
6 5 anbi2i ⊢ y ∈ dom ⁡ F ∧ F ⁡ y ∈ ⋃ A ↔ y ∈ dom ⁡ F ∧ ∃ x ∈ A F ⁡ y ∈ x
7 6 a1i ⊢ F Fn dom ⁡ F → y ∈ dom ⁡ F ∧ F ⁡ y ∈ ⋃ A ↔ y ∈ dom ⁡ F ∧ ∃ x ∈ A F ⁡ y ∈ x
8 elpreima ⊢ F Fn dom ⁡ F → y ∈ F -1 x ↔ y ∈ dom ⁡ F ∧ F ⁡ y ∈ x
9 8 rexbidv ⊢ F Fn dom ⁡ F → ∃ x ∈ A y ∈ F -1 x ↔ ∃ x ∈ A y ∈ dom ⁡ F ∧ F ⁡ y ∈ x
10 4 7 9 3bitr4d ⊢ F Fn dom ⁡ F → y ∈ dom ⁡ F ∧ F ⁡ y ∈ ⋃ A ↔ ∃ x ∈ A y ∈ F -1 x
11 elpreima ⊢ F Fn dom ⁡ F → y ∈ F -1 ⋃ A ↔ y ∈ dom ⁡ F ∧ F ⁡ y ∈ ⋃ A
12 eliun ⊢ y ∈ ⋃ x ∈ A F -1 x ↔ ∃ x ∈ A y ∈ F -1 x
13 12 a1i ⊢ F Fn dom ⁡ F → y ∈ ⋃ x ∈ A F -1 x ↔ ∃ x ∈ A y ∈ F -1 x
14 10 11 13 3bitr4d ⊢ F Fn dom ⁡ F → y ∈ F -1 ⋃ A ↔ y ∈ ⋃ x ∈ A F -1 x
15 14 eqrdv ⊢ F Fn dom ⁡ F → F -1 ⋃ A = ⋃ x ∈ A F -1 x
16 1 15 sylbi ⊢ Fun ⁡ F → F -1 ⋃ A = ⋃ x ∈ A F -1 x