Metamath Proof Explorer

Theorem unpreima

Description: Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion unpreima ⊢ Fun ⁡ F → F -1 A ∪ B = F -1 A ∪ F -1 B

Proof

Step Hyp Ref Expression
1 funfn ⊢ Fun ⁡ F ↔ F Fn dom ⁡ F
2 elpreima ⊢ F Fn dom ⁡ F → x ∈ F -1 A ∪ B ↔ x ∈ dom ⁡ F ∧ F ⁡ x ∈ A ∪ B
3 elun ⊢ F ⁡ x ∈ A ∪ B ↔ F ⁡ x ∈ A ∨ F ⁡ x ∈ B
4 3 anbi2i ⊢ x ∈ dom ⁡ F ∧ F ⁡ x ∈ A ∪ B ↔ x ∈ dom ⁡ F ∧ F ⁡ x ∈ A ∨ F ⁡ x ∈ B
5 andi ⊢ x ∈ dom ⁡ F ∧ F ⁡ x ∈ A ∨ F ⁡ x ∈ B ↔ x ∈ dom ⁡ F ∧ F ⁡ x ∈ A ∨ x ∈ dom ⁡ F ∧ F ⁡ x ∈ B
6 4 5 bitri ⊢ x ∈ dom ⁡ F ∧ F ⁡ x ∈ A ∪ B ↔ x ∈ dom ⁡ F ∧ F ⁡ x ∈ A ∨ x ∈ dom ⁡ F ∧ F ⁡ x ∈ B
7 elun ⊢ x ∈ F -1 A ∪ F -1 B ↔ x ∈ F -1 A ∨ x ∈ F -1 B
8 elpreima ⊢ F Fn dom ⁡ F → x ∈ F -1 A ↔ x ∈ dom ⁡ F ∧ F ⁡ x ∈ A
9 elpreima ⊢ F Fn dom ⁡ F → x ∈ F -1 B ↔ x ∈ dom ⁡ F ∧ F ⁡ x ∈ B
10 8 9 orbi12d ⊢ F Fn dom ⁡ F → x ∈ F -1 A ∨ x ∈ F -1 B ↔ x ∈ dom ⁡ F ∧ F ⁡ x ∈ A ∨ x ∈ dom ⁡ F ∧ F ⁡ x ∈ B
11 7 10 bitrid ⊢ F Fn dom ⁡ F → x ∈ F -1 A ∪ F -1 B ↔ x ∈ dom ⁡ F ∧ F ⁡ x ∈ A ∨ x ∈ dom ⁡ F ∧ F ⁡ x ∈ B
12 6 11 bitr4id ⊢ F Fn dom ⁡ F → x ∈ dom ⁡ F ∧ F ⁡ x ∈ A ∪ B ↔ x ∈ F -1 A ∪ F -1 B
13 2 12 bitrd ⊢ F Fn dom ⁡ F → x ∈ F -1 A ∪ B ↔ x ∈ F -1 A ∪ F -1 B
14 13 eqrdv ⊢ F Fn dom ⁡ F → F -1 A ∪ B = F -1 A ∪ F -1 B
15 1 14 sylbi ⊢ Fun ⁡ F → F -1 A ∪ B = F -1 A ∪ F -1 B