This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐶 ) ∈ ( 𝐴 ⊔ 𝐵 ) )