Theorem mptun

Description: Union of mappings which are mutually compatible. (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	mptun	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∪ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		df-mpt	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑦 = 𝐶 ) }
2		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) }
3		df-mpt	⊢ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶 ) }
4	2 3	uneq12i	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∪ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶 ) } )
5		elun	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
6	5	anbi1i	⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑦 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ 𝑦 = 𝐶 ) )
7		andir	⊢ ( ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ 𝑦 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶 ) ) )
8	6 7	bitri	⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑦 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶 ) ) )
9	8	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑦 = 𝐶 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶 ) ) }
10		unopab	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶 ) ) }
11	9 10	eqtr4i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑦 = 𝐶 ) } = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶 ) } )
12	4 11	eqtr4i	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∪ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑦 = 𝐶 ) }
13	1 12	eqtr4i	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↦ 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∪ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )