This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )