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

Metamath Proof Explorer

Theorem unpreima

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

Ref Expression
Assertion unpreima ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝐴 ∪ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝐴 ) ∪ ( ◡ 𝐹 “ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 funfn ⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
2 elpreima ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝐴 ∪ 𝐵 ) ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∪ 𝐵 ) ) ) )
3 elun ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ∨ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
4 3 anbi2i ⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∪ 𝐵 ) ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ∨ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) )
5 andi ⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ∨ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) ↔ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) ∨ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) )
6 4 5 bitri ⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∪ 𝐵 ) ) ↔ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) ∨ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) )
7 elun ⊢ ( 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) ∪ ( ◡ 𝐹 “ 𝐵 ) ) ↔ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝐴 ) ∨ 𝑥 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )
8 elpreima ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝐴 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) ) )
9 elpreima ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝐵 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) )
10 8 9 orbi12d ⊢ ( 𝐹 Fn dom 𝐹 → ( ( 𝑥 ∈ ( ◡ 𝐹 “ 𝐴 ) ∨ 𝑥 ∈ ( ◡ 𝐹 “ 𝐵 ) ) ↔ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) ∨ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) ) )
11 7 10 bitrid ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) ∪ ( ◡ 𝐹 “ 𝐵 ) ) ↔ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) ∨ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) ) )
12 6 11 bitr4id ⊢ ( 𝐹 Fn dom 𝐹 → ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∪ 𝐵 ) ) ↔ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) ∪ ( ◡ 𝐹 “ 𝐵 ) ) ) )
13 2 12 bitrd ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝐴 ∪ 𝐵 ) ) ↔ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) ∪ ( ◡ 𝐹 “ 𝐵 ) ) ) )
14 13 eqrdv ⊢ ( 𝐹 Fn dom 𝐹 → ( ◡ 𝐹 “ ( 𝐴 ∪ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝐴 ) ∪ ( ◡ 𝐹 “ 𝐵 ) ) )
15 1 14 sylbi ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝐴 ∪ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝐴 ) ∪ ( ◡ 𝐹 “ 𝐵 ) ) )