Theorem unima

Description: Image of a union. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	unima	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 “ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐹 “ 𝐵 ) ∪ ( 𝐹 “ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → 𝐹 Fn 𝐴 )
2		simpl	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → 𝐵 ⊆ 𝐴 )
3		simpr	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → 𝐶 ⊆ 𝐴 )
4	2 3	unssd	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐵 ∪ 𝐶 ) ⊆ 𝐴 )
5	4	3adant1	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐵 ∪ 𝐶 ) ⊆ 𝐴 )
6	1 5	fvelimabd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ ( 𝐵 ∪ 𝐶 ) ) ↔ ∃ 𝑥 ∈ ( 𝐵 ∪ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
7		rexun	⊢ ( ∃ 𝑥 ∈ ( 𝐵 ∪ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ ( ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝑦 ∨ ∃ 𝑥 ∈ 𝐶 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
8	6 7	bitrdi	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ ( 𝐵 ∪ 𝐶 ) ) ↔ ( ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝑦 ∨ ∃ 𝑥 ∈ 𝐶 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
9		fvelimab	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
10	9	3adant3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
11		fvelimab	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐶 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
12	11	3adant2	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐶 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
13	10 12	orbi12d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝑦 ∈ ( 𝐹 “ 𝐵 ) ∨ 𝑦 ∈ ( 𝐹 “ 𝐶 ) ) ↔ ( ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝑦 ∨ ∃ 𝑥 ∈ 𝐶 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
14	8 13	bitr4d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ ( 𝐵 ∪ 𝐶 ) ) ↔ ( 𝑦 ∈ ( 𝐹 “ 𝐵 ) ∨ 𝑦 ∈ ( 𝐹 “ 𝐶 ) ) ) )
15		elun	⊢ ( 𝑦 ∈ ( ( 𝐹 “ 𝐵 ) ∪ ( 𝐹 “ 𝐶 ) ) ↔ ( 𝑦 ∈ ( 𝐹 “ 𝐵 ) ∨ 𝑦 ∈ ( 𝐹 “ 𝐶 ) ) )
16	14 15	bitr4di	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ ( 𝐵 ∪ 𝐶 ) ) ↔ 𝑦 ∈ ( ( 𝐹 “ 𝐵 ) ∪ ( 𝐹 “ 𝐶 ) ) ) )
17	16	eqrdv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 “ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐹 “ 𝐵 ) ∪ ( 𝐹 “ 𝐶 ) ) )