eldju1st

Description: The first component of an element of a disjoint union is either (/) or 1o . (Contributed by AV, 26-Jun-2022)

		Ref	Expression
	Assertion	eldju1st	⊢ ( 𝑋 ∈ ( 𝐴 ⊔ 𝐵 ) → ( ( 1^st ‘ 𝑋 ) = ∅ ∨ ( 1^st ‘ 𝑋 ) = 1_o ) )

Step	Hyp	Ref	Expression
1		djuss	⊢ ( 𝐴 ⊔ 𝐵 ) ⊆ ( { ∅ , 1_o } × ( 𝐴 ∪ 𝐵 ) )
2		ssel2	⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ⊆ ( { ∅ , 1_o } × ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑋 ∈ ( 𝐴 ⊔ 𝐵 ) ) → 𝑋 ∈ ( { ∅ , 1_o } × ( 𝐴 ∪ 𝐵 ) ) )
3		xp1st	⊢ ( 𝑋 ∈ ( { ∅ , 1_o } × ( 𝐴 ∪ 𝐵 ) ) → ( 1^st ‘ 𝑋 ) ∈ { ∅ , 1_o } )
4		elpri	⊢ ( ( 1^st ‘ 𝑋 ) ∈ { ∅ , 1_o } → ( ( 1^st ‘ 𝑋 ) = ∅ ∨ ( 1^st ‘ 𝑋 ) = 1_o ) )
5	2 3 4	3syl	⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ⊆ ( { ∅ , 1_o } × ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑋 ∈ ( 𝐴 ⊔ 𝐵 ) ) → ( ( 1^st ‘ 𝑋 ) = ∅ ∨ ( 1^st ‘ 𝑋 ) = 1_o ) )
6	1 5	mpan	⊢ ( 𝑋 ∈ ( 𝐴 ⊔ 𝐵 ) → ( ( 1^st ‘ 𝑋 ) = ∅ ∨ ( 1^st ‘ 𝑋 ) = 1_o ) )

Metamath Proof Explorer