Metamath Proof Explorer

Theorem eldju2ndr

Description: The second component of an element of a disjoint union is an element of the right class of the disjoint union if its first component is not the empty set. (Contributed by AV, 26-Jun-2022)

Ref Expression
Assertion eldju2ndr ⊢ X ∈ A ⊔︀ B ∧ 1 st ⁡ X ≠ ∅ → 2 nd ⁡ X ∈ B

Proof

Step Hyp Ref Expression
1 df-dju ⊢ A ⊔︀ B = ∅ × A ∪ 1 𝑜 × B
2 1 eleq2i ⊢ X ∈ A ⊔︀ B ↔ X ∈ ∅ × A ∪ 1 𝑜 × B
3 elun ⊢ X ∈ ∅ × A ∪ 1 𝑜 × B ↔ X ∈ ∅ × A ∨ X ∈ 1 𝑜 × B
4 2 3 bitri ⊢ X ∈ A ⊔︀ B ↔ X ∈ ∅ × A ∨ X ∈ 1 𝑜 × B
5 elxp6 ⊢ X ∈ ∅ × A ↔ X = 1 st ⁡ X 2 nd ⁡ X ∧ 1 st ⁡ X ∈ ∅ ∧ 2 nd ⁡ X ∈ A
6 elsni ⊢ 1 st ⁡ X ∈ ∅ → 1 st ⁡ X = ∅
7 eqneqall ⊢ 1 st ⁡ X = ∅ → 1 st ⁡ X ≠ ∅ → 2 nd ⁡ X ∈ B
8 6 7 syl ⊢ 1 st ⁡ X ∈ ∅ → 1 st ⁡ X ≠ ∅ → 2 nd ⁡ X ∈ B
9 8 ad2antrl ⊢ X = 1 st ⁡ X 2 nd ⁡ X ∧ 1 st ⁡ X ∈ ∅ ∧ 2 nd ⁡ X ∈ A → 1 st ⁡ X ≠ ∅ → 2 nd ⁡ X ∈ B
10 5 9 sylbi ⊢ X ∈ ∅ × A → 1 st ⁡ X ≠ ∅ → 2 nd ⁡ X ∈ B
11 elxp6 ⊢ X ∈ 1 𝑜 × B ↔ X = 1 st ⁡ X 2 nd ⁡ X ∧ 1 st ⁡ X ∈ 1 𝑜 ∧ 2 nd ⁡ X ∈ B
12 simprr ⊢ X = 1 st ⁡ X 2 nd ⁡ X ∧ 1 st ⁡ X ∈ 1 𝑜 ∧ 2 nd ⁡ X ∈ B → 2 nd ⁡ X ∈ B
13 12 a1d ⊢ X = 1 st ⁡ X 2 nd ⁡ X ∧ 1 st ⁡ X ∈ 1 𝑜 ∧ 2 nd ⁡ X ∈ B → 1 st ⁡ X ≠ ∅ → 2 nd ⁡ X ∈ B
14 11 13 sylbi ⊢ X ∈ 1 𝑜 × B → 1 st ⁡ X ≠ ∅ → 2 nd ⁡ X ∈ B
15 10 14 jaoi ⊢ X ∈ ∅ × A ∨ X ∈ 1 𝑜 × B → 1 st ⁡ X ≠ ∅ → 2 nd ⁡ X ∈ B
16 4 15 sylbi ⊢ X ∈ A ⊔︀ B → 1 st ⁡ X ≠ ∅ → 2 nd ⁡ X ∈ B
17 16 imp ⊢ X ∈ A ⊔︀ B ∧ 1 st ⁡ X ≠ ∅ → 2 nd ⁡ X ∈ B