Theorem joincomALT

Description: The join of a poset is commutative. (This may not be a theorem under other definitions of meet.) (Contributed by NM, 16-Sep-2011) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	joincom.b	|- B = ( Base ` K )
	joincom.j	|- .\/ = ( join ` K )
Assertion	joincomALT	|- ( ( K e. V /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) = ( Y .\/ X ) )

Proof

Step	Hyp	Ref	Expression
1		joincom.b	|- B = ( Base ` K )
2		joincom.j	|- .\/ = ( join ` K )
3		prcom	|- { Y , X } = { X , Y }
4	3	fveq2i	|- ( ( lub ` K ) ` { Y , X } ) = ( ( lub ` K ) ` { X , Y } )
5	4	a1i	|- ( ( K e. V /\ X e. B /\ Y e. B ) -> ( ( lub ` K ) ` { Y , X } ) = ( ( lub ` K ) ` { X , Y } ) )
6		eqid	|- ( lub ` K ) = ( lub ` K )
7		simp1	|- ( ( K e. V /\ X e. B /\ Y e. B ) -> K e. V )
8		simp3	|- ( ( K e. V /\ X e. B /\ Y e. B ) -> Y e. B )
9		simp2	|- ( ( K e. V /\ X e. B /\ Y e. B ) -> X e. B )
10	6 2 7 8 9	joinval	|- ( ( K e. V /\ X e. B /\ Y e. B ) -> ( Y .\/ X ) = ( ( lub ` K ) ` { Y , X } ) )
11	6 2 7 9 8	joinval	|- ( ( K e. V /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) = ( ( lub ` K ) ` { X , Y } ) )
12	5 10 11	3eqtr4rd	|- ( ( K e. V /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) = ( Y .\/ X ) )