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	⊢ ( ( 𝑋 ∈ ( 𝐴 ⊔ 𝐵 ) ∧ ( 1^st ‘ 𝑋 ) ≠ ∅ ) → ( 2^nd ‘ 𝑋 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-dju	⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 𝐵 ) )
2	1	eleq2i	⊢ ( 𝑋 ∈ ( 𝐴 ⊔ 𝐵 ) ↔ 𝑋 ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 𝐵 ) ) )
3		elun	⊢ ( 𝑋 ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 𝐵 ) ) ↔ ( 𝑋 ∈ ( { ∅ } × 𝐴 ) ∨ 𝑋 ∈ ( { 1_o } × 𝐵 ) ) )
4	2 3	bitri	⊢ ( 𝑋 ∈ ( 𝐴 ⊔ 𝐵 ) ↔ ( 𝑋 ∈ ( { ∅ } × 𝐴 ) ∨ 𝑋 ∈ ( { 1_o } × 𝐵 ) ) )
5		elxp6	⊢ ( 𝑋 ∈ ( { ∅ } × 𝐴 ) ↔ ( 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∧ ( ( 1^st ‘ 𝑋 ) ∈ { ∅ } ∧ ( 2^nd ‘ 𝑋 ) ∈ 𝐴 ) ) )
6		elsni	⊢ ( ( 1^st ‘ 𝑋 ) ∈ { ∅ } → ( 1^st ‘ 𝑋 ) = ∅ )
7		eqneqall	⊢ ( ( 1^st ‘ 𝑋 ) = ∅ → ( ( 1^st ‘ 𝑋 ) ≠ ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐵 ) )
8	6 7	syl	⊢ ( ( 1^st ‘ 𝑋 ) ∈ { ∅ } → ( ( 1^st ‘ 𝑋 ) ≠ ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐵 ) )
9	8	ad2antrl	⊢ ( ( 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∧ ( ( 1^st ‘ 𝑋 ) ∈ { ∅ } ∧ ( 2^nd ‘ 𝑋 ) ∈ 𝐴 ) ) → ( ( 1^st ‘ 𝑋 ) ≠ ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐵 ) )
10	5 9	sylbi	⊢ ( 𝑋 ∈ ( { ∅ } × 𝐴 ) → ( ( 1^st ‘ 𝑋 ) ≠ ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐵 ) )
11		elxp6	⊢ ( 𝑋 ∈ ( { 1_o } × 𝐵 ) ↔ ( 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∧ ( ( 1^st ‘ 𝑋 ) ∈ { 1_o } ∧ ( 2^nd ‘ 𝑋 ) ∈ 𝐵 ) ) )
12		simprr	⊢ ( ( 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∧ ( ( 1^st ‘ 𝑋 ) ∈ { 1_o } ∧ ( 2^nd ‘ 𝑋 ) ∈ 𝐵 ) ) → ( 2^nd ‘ 𝑋 ) ∈ 𝐵 )
13	12	a1d	⊢ ( ( 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∧ ( ( 1^st ‘ 𝑋 ) ∈ { 1_o } ∧ ( 2^nd ‘ 𝑋 ) ∈ 𝐵 ) ) → ( ( 1^st ‘ 𝑋 ) ≠ ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐵 ) )
14	11 13	sylbi	⊢ ( 𝑋 ∈ ( { 1_o } × 𝐵 ) → ( ( 1^st ‘ 𝑋 ) ≠ ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐵 ) )
15	10 14	jaoi	⊢ ( ( 𝑋 ∈ ( { ∅ } × 𝐴 ) ∨ 𝑋 ∈ ( { 1_o } × 𝐵 ) ) → ( ( 1^st ‘ 𝑋 ) ≠ ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐵 ) )
16	4 15	sylbi	⊢ ( 𝑋 ∈ ( 𝐴 ⊔ 𝐵 ) → ( ( 1^st ‘ 𝑋 ) ≠ ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐵 ) )
17	16	imp	⊢ ( ( 𝑋 ∈ ( 𝐴 ⊔ 𝐵 ) ∧ ( 1^st ‘ 𝑋 ) ≠ ∅ ) → ( 2^nd ‘ 𝑋 ) ∈ 𝐵 )