eldju2ndl

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

		Ref	Expression
	Assertion	eldju2ndl	⊢ ( ( 𝑋 ∈ ( 𝐴 ⊔ 𝐵 ) ∧ ( 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		simprr	⊢ ( ( 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∧ ( ( 1^st ‘ 𝑋 ) ∈ { ∅ } ∧ ( 2^nd ‘ 𝑋 ) ∈ 𝐴 ) ) → ( 2^nd ‘ 𝑋 ) ∈ 𝐴 )
7	6	a1d	⊢ ( ( 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∧ ( ( 1^st ‘ 𝑋 ) ∈ { ∅ } ∧ ( 2^nd ‘ 𝑋 ) ∈ 𝐴 ) ) → ( ( 1^st ‘ 𝑋 ) = ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐴 ) )
8	5 7	sylbi	⊢ ( 𝑋 ∈ ( { ∅ } × 𝐴 ) → ( ( 1^st ‘ 𝑋 ) = ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐴 ) )
9		elxp6	⊢ ( 𝑋 ∈ ( { 1_o } × 𝐵 ) ↔ ( 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∧ ( ( 1^st ‘ 𝑋 ) ∈ { 1_o } ∧ ( 2^nd ‘ 𝑋 ) ∈ 𝐵 ) ) )
10		elsni	⊢ ( ( 1^st ‘ 𝑋 ) ∈ { 1_o } → ( 1^st ‘ 𝑋 ) = 1_o )
11		1n0	⊢ 1_o ≠ ∅
12		neeq1	⊢ ( ( 1^st ‘ 𝑋 ) = 1_o → ( ( 1^st ‘ 𝑋 ) ≠ ∅ ↔ 1_o ≠ ∅ ) )
13	11 12	mpbiri	⊢ ( ( 1^st ‘ 𝑋 ) = 1_o → ( 1^st ‘ 𝑋 ) ≠ ∅ )
14		eqneqall	⊢ ( ( 1^st ‘ 𝑋 ) = ∅ → ( ( 1^st ‘ 𝑋 ) ≠ ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐴 ) )
15	14	com12	⊢ ( ( 1^st ‘ 𝑋 ) ≠ ∅ → ( ( 1^st ‘ 𝑋 ) = ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐴 ) )
16	10 13 15	3syl	⊢ ( ( 1^st ‘ 𝑋 ) ∈ { 1_o } → ( ( 1^st ‘ 𝑋 ) = ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐴 ) )
17	16	ad2antrl	⊢ ( ( 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∧ ( ( 1^st ‘ 𝑋 ) ∈ { 1_o } ∧ ( 2^nd ‘ 𝑋 ) ∈ 𝐵 ) ) → ( ( 1^st ‘ 𝑋 ) = ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐴 ) )
18	9 17	sylbi	⊢ ( 𝑋 ∈ ( { 1_o } × 𝐵 ) → ( ( 1^st ‘ 𝑋 ) = ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐴 ) )
19	8 18	jaoi	⊢ ( ( 𝑋 ∈ ( { ∅ } × 𝐴 ) ∨ 𝑋 ∈ ( { 1_o } × 𝐵 ) ) → ( ( 1^st ‘ 𝑋 ) = ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐴 ) )
20	4 19	sylbi	⊢ ( 𝑋 ∈ ( 𝐴 ⊔ 𝐵 ) → ( ( 1^st ‘ 𝑋 ) = ∅ → ( 2^nd ‘ 𝑋 ) ∈ 𝐴 ) )
21	20	imp	⊢ ( ( 𝑋 ∈ ( 𝐴 ⊔ 𝐵 ) ∧ ( 1^st ‘ 𝑋 ) = ∅ ) → ( 2^nd ‘ 𝑋 ) ∈ 𝐴 )

Metamath Proof Explorer

Theorem eldju2ndl

Proof