Theorem djurcl

Description: Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022)

	Ref	Expression
Assertion	djurcl	⊢ ( 𝐶 ∈ 𝐵 → ( inr ‘ 𝐶 ) ∈ ( 𝐴 ⊔ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐶 ∈ 𝐵 → 𝐶 ∈ V )
2		1oex	⊢ 1o ∈ V
3	2	snid	⊢ 1o ∈ { 1o }
4		opelxpi	⊢ ( ( 1o ∈ { 1o } ∧ 𝐶 ∈ 𝐵 ) → ⟨ 1o , 𝐶 ⟩ ∈ ( { 1o } × 𝐵 ) )
5	3 4	mpan	⊢ ( 𝐶 ∈ 𝐵 → ⟨ 1o , 𝐶 ⟩ ∈ ( { 1o } × 𝐵 ) )
6		opeq2	⊢ ( 𝑥 = 𝐶 → ⟨ 1o , 𝑥 ⟩ = ⟨ 1o , 𝐶 ⟩ )
7		df-inr	⊢ inr = ( 𝑥 ∈ V ↦ ⟨ 1o , 𝑥 ⟩ )
8	6 7	fvmptg	⊢ ( ( 𝐶 ∈ V ∧ ⟨ 1o , 𝐶 ⟩ ∈ ( { 1o } × 𝐵 ) ) → ( inr ‘ 𝐶 ) = ⟨ 1o , 𝐶 ⟩ )
9	1 5 8	syl2anc	⊢ ( 𝐶 ∈ 𝐵 → ( inr ‘ 𝐶 ) = ⟨ 1o , 𝐶 ⟩ )
10		elun2	⊢ ( ⟨ 1o , 𝐶 ⟩ ∈ ( { 1o } × 𝐵 ) → ⟨ 1o , 𝐶 ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) )
11	5 10	syl	⊢ ( 𝐶 ∈ 𝐵 → ⟨ 1o , 𝐶 ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) )
12		df-dju	⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
13	11 12	eleqtrrdi	⊢ ( 𝐶 ∈ 𝐵 → ⟨ 1o , 𝐶 ⟩ ∈ ( 𝐴 ⊔ 𝐵 ) )
14	9 13	eqeltrd	⊢ ( 𝐶 ∈ 𝐵 → ( inr ‘ 𝐶 ) ∈ ( 𝐴 ⊔ 𝐵 ) )