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