Metamath Proof Explorer

Theorem unima

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

Ref Expression
Assertion unima ⊢ F Fn A ∧ B ⊆ A ∧ C ⊆ A → F B ∪ C = F B ∪ F C

Proof

Step Hyp Ref Expression
1 simp1 ⊢ F Fn A ∧ B ⊆ A ∧ C ⊆ A → F Fn A
2 simpl ⊢ B ⊆ A ∧ C ⊆ A → B ⊆ A
3 simpr ⊢ B ⊆ A ∧ C ⊆ A → C ⊆ A
4 2 3 unssd ⊢ B ⊆ A ∧ C ⊆ A → B ∪ C ⊆ A
5 4 3adant1 ⊢ F Fn A ∧ B ⊆ A ∧ C ⊆ A → B ∪ C ⊆ A
6 1 5 fvelimabd ⊢ F Fn A ∧ B ⊆ A ∧ C ⊆ A → y ∈ F B ∪ C ↔ ∃ x ∈ B ∪ C F ⁡ x = y
7 rexun ⊢ ∃ x ∈ B ∪ C F ⁡ x = y ↔ ∃ x ∈ B F ⁡ x = y ∨ ∃ x ∈ C F ⁡ x = y
8 6 7 bitrdi ⊢ F Fn A ∧ B ⊆ A ∧ C ⊆ A → y ∈ F B ∪ C ↔ ∃ x ∈ B F ⁡ x = y ∨ ∃ x ∈ C F ⁡ x = y
9 fvelimab ⊢ F Fn A ∧ B ⊆ A → y ∈ F B ↔ ∃ x ∈ B F ⁡ x = y
10 9 3adant3 ⊢ F Fn A ∧ B ⊆ A ∧ C ⊆ A → y ∈ F B ↔ ∃ x ∈ B F ⁡ x = y
11 fvelimab ⊢ F Fn A ∧ C ⊆ A → y ∈ F C ↔ ∃ x ∈ C F ⁡ x = y
12 11 3adant2 ⊢ F Fn A ∧ B ⊆ A ∧ C ⊆ A → y ∈ F C ↔ ∃ x ∈ C F ⁡ x = y
13 10 12 orbi12d ⊢ F Fn A ∧ B ⊆ A ∧ C ⊆ A → y ∈ F B ∨ y ∈ F C ↔ ∃ x ∈ B F ⁡ x = y ∨ ∃ x ∈ C F ⁡ x = y
14 8 13 bitr4d ⊢ F Fn A ∧ B ⊆ A ∧ C ⊆ A → y ∈ F B ∪ C ↔ y ∈ F B ∨ y ∈ F C
15 elun ⊢ y ∈ F B ∪ F C ↔ y ∈ F B ∨ y ∈ F C
16 14 15 bitr4di ⊢ F Fn A ∧ B ⊆ A ∧ C ⊆ A → y ∈ F B ∪ C ↔ y ∈ F B ∪ F C
17 16 eqrdv ⊢ F Fn A ∧ B ⊆ A ∧ C ⊆ A → F B ∪ C = F B ∪ F C