Theorem hash2prd

Description: A set of size two is an unordered pair if it contains two different elements. (Contributed by Alexander van der Vekens, 9-Dec-2018) (Proof shortened by AV, 16-Jun-2022)

	Ref	Expression
Assertion	hash2prd	|- ( ( P e. V /\ ( # ` P ) = 2 ) -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> P = { X , Y } ) )

Proof

Step	Hyp	Ref	Expression
1		hash2prb	|- ( P e. V -> ( ( # ` P ) = 2 <-> E. x e. P E. y e. P ( x =/= y /\ P = { x , y } ) ) )
2		simpr	|- ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> P = { x , y } )
3		3simpa	|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X e. P /\ Y e. P ) )
4	3	ad2antlr	|- ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> ( X e. P /\ Y e. P ) )
5		eleq2	|- ( P = { x , y } -> ( X e. P <-> X e. { x , y } ) )
6		eleq2	|- ( P = { x , y } -> ( Y e. P <-> Y e. { x , y } ) )
7	5 6	anbi12d	|- ( P = { x , y } -> ( ( X e. P /\ Y e. P ) <-> ( X e. { x , y } /\ Y e. { x , y } ) ) )
8	7	adantl	|- ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> ( ( X e. P /\ Y e. P ) <-> ( X e. { x , y } /\ Y e. { x , y } ) ) )
9	4 8	mpbid	|- ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> ( X e. { x , y } /\ Y e. { x , y } ) )
10		prel12g	|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( { X , Y } = { x , y } <-> ( X e. { x , y } /\ Y e. { x , y } ) ) )
11	10	ad2antlr	|- ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> ( { X , Y } = { x , y } <-> ( X e. { x , y } /\ Y e. { x , y } ) ) )
12	9 11	mpbird	|- ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> { X , Y } = { x , y } )
13	2 12	eqtr4d	|- ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> P = { X , Y } )
14	13	exp31	|- ( ( ( x e. P /\ y e. P ) /\ x =/= y ) -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( P = { x , y } -> P = { X , Y } ) ) )
15	14	com23	|- ( ( ( x e. P /\ y e. P ) /\ x =/= y ) -> ( P = { x , y } -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> P = { X , Y } ) ) )
16	15	expimpd	|- ( ( x e. P /\ y e. P ) -> ( ( x =/= y /\ P = { x , y } ) -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> P = { X , Y } ) ) )
17	16	rexlimivv	|- ( E. x e. P E. y e. P ( x =/= y /\ P = { x , y } ) -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> P = { X , Y } ) )
18	1 17	biimtrdi	|- ( P e. V -> ( ( # ` P ) = 2 -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> P = { X , Y } ) ) )
19	18	imp	|- ( ( P e. V /\ ( # ` P ) = 2 ) -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> P = { X , Y } ) )