| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fnun |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) ) |
| 2 |
1
|
expcom |
⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) ) ) |
| 3 |
|
rnun |
⊢ ran ( 𝐹 ∪ 𝐺 ) = ( ran 𝐹 ∪ ran 𝐺 ) |
| 4 |
|
unss12 |
⊢ ( ( ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷 ) → ( ran 𝐹 ∪ ran 𝐺 ) ⊆ ( 𝐶 ∪ 𝐷 ) ) |
| 5 |
3 4
|
eqsstrid |
⊢ ( ( ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷 ) → ran ( 𝐹 ∪ 𝐺 ) ⊆ ( 𝐶 ∪ 𝐷 ) ) |
| 6 |
2 5
|
anim12d1 |
⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷 ) ) → ( ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) ∧ ran ( 𝐹 ∪ 𝐺 ) ⊆ ( 𝐶 ∪ 𝐷 ) ) ) ) |
| 7 |
|
df-f |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶 ) ) |
| 8 |
|
df-f |
⊢ ( 𝐺 : 𝐵 ⟶ 𝐷 ↔ ( 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐷 ) ) |
| 9 |
7 8
|
anbi12i |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐷 ) ↔ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ ( 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐷 ) ) ) |
| 10 |
|
an4 |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ ( 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐷 ) ) ↔ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷 ) ) ) |
| 11 |
9 10
|
bitri |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐷 ) ↔ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷 ) ) ) |
| 12 |
|
df-f |
⊢ ( ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ( 𝐶 ∪ 𝐷 ) ↔ ( ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) ∧ ran ( 𝐹 ∪ 𝐺 ) ⊆ ( 𝐶 ∪ 𝐷 ) ) ) |
| 13 |
6 11 12
|
3imtr4g |
⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐷 ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ( 𝐶 ∪ 𝐷 ) ) ) |
| 14 |
13
|
impcom |
⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐷 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ( 𝐶 ∪ 𝐷 ) ) |