Theorem 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	|- ( X e. ( A |_| B ) -> ( ( 1st ` X ) = (/) \/ ( 1st ` X ) = 1o ) )

Proof

Step	Hyp	Ref	Expression
1		djuss	|- ( A |_| B ) C_ ( { (/) , 1o } X. ( A u. B ) )
2		ssel2	|- ( ( ( A |_| B ) C_ ( { (/) , 1o } X. ( A u. B ) ) /\ X e. ( A |_| B ) ) -> X e. ( { (/) , 1o } X. ( A u. B ) ) )
3		xp1st	|- ( X e. ( { (/) , 1o } X. ( A u. B ) ) -> ( 1st ` X ) e. { (/) , 1o } )
4		elpri	|- ( ( 1st ` X ) e. { (/) , 1o } -> ( ( 1st ` X ) = (/) \/ ( 1st ` X ) = 1o ) )
5	2 3 4	3syl	|- ( ( ( A |_| B ) C_ ( { (/) , 1o } X. ( A u. B ) ) /\ X e. ( A |_| B ) ) -> ( ( 1st ` X ) = (/) \/ ( 1st ` X ) = 1o ) )
6	1 5	mpan	|- ( X e. ( A |_| B ) -> ( ( 1st ` X ) = (/) \/ ( 1st ` X ) = 1o ) )