Metamath Proof Explorer

Theorem prsprel

Description: The elements of a pair from the set of all unordered pairs over a given set V are elements of the set V . (Contributed by AV, 22-Nov-2021)

Ref Expression
Assertion prsprel 
|- ( ( { X , Y } e. ( Pairs ` V ) /\ ( X e. U /\ Y e. W ) ) -> ( X e. V /\ Y e. V ) )

Proof

Step Hyp Ref Expression
1 sprel 
 |-  ( { X , Y } e. ( Pairs ` V ) -> E. a e. V E. b e. V { X , Y } = { a , b } )
2 preq12bg 
 |-  ( ( ( X e. U /\ Y e. W ) /\ ( a e. V /\ b e. V ) ) -> ( { X , Y } = { a , b } <-> ( ( X = a /\ Y = b ) \/ ( X = b /\ Y = a ) ) ) )
3 eleq1 
 |-  ( a = X -> ( a e. V <-> X e. V ) )
4 3 eqcoms 
 |-  ( X = a -> ( a e. V <-> X e. V ) )
5 eleq1 
 |-  ( b = Y -> ( b e. V <-> Y e. V ) )
6 5 eqcoms 
 |-  ( Y = b -> ( b e. V <-> Y e. V ) )
7 4 6 bi2anan9 
 |-  ( ( X = a /\ Y = b ) -> ( ( a e. V /\ b e. V ) <-> ( X e. V /\ Y e. V ) ) )
8 7 biimpd 
 |-  ( ( X = a /\ Y = b ) -> ( ( a e. V /\ b e. V ) -> ( X e. V /\ Y e. V ) ) )
9 eleq1 
 |-  ( b = X -> ( b e. V <-> X e. V ) )
10 9 eqcoms 
 |-  ( X = b -> ( b e. V <-> X e. V ) )
11 eleq1 
 |-  ( a = Y -> ( a e. V <-> Y e. V ) )
12 11 eqcoms 
 |-  ( Y = a -> ( a e. V <-> Y e. V ) )
13 10 12 bi2anan9 
 |-  ( ( X = b /\ Y = a ) -> ( ( b e. V /\ a e. V ) <-> ( X e. V /\ Y e. V ) ) )
14 13 biimpd 
 |-  ( ( X = b /\ Y = a ) -> ( ( b e. V /\ a e. V ) -> ( X e. V /\ Y e. V ) ) )
15 14 ancomsd 
 |-  ( ( X = b /\ Y = a ) -> ( ( a e. V /\ b e. V ) -> ( X e. V /\ Y e. V ) ) )
16 8 15 jaoi 
 |-  ( ( ( X = a /\ Y = b ) \/ ( X = b /\ Y = a ) ) -> ( ( a e. V /\ b e. V ) -> ( X e. V /\ Y e. V ) ) )
17 16 com12 
 |-  ( ( a e. V /\ b e. V ) -> ( ( ( X = a /\ Y = b ) \/ ( X = b /\ Y = a ) ) -> ( X e. V /\ Y e. V ) ) )
18 17 adantl 
 |-  ( ( ( X e. U /\ Y e. W ) /\ ( a e. V /\ b e. V ) ) -> ( ( ( X = a /\ Y = b ) \/ ( X = b /\ Y = a ) ) -> ( X e. V /\ Y e. V ) ) )
19 2 18 sylbid 
 |-  ( ( ( X e. U /\ Y e. W ) /\ ( a e. V /\ b e. V ) ) -> ( { X , Y } = { a , b } -> ( X e. V /\ Y e. V ) ) )
20 19 expcom 
 |-  ( ( a e. V /\ b e. V ) -> ( ( X e. U /\ Y e. W ) -> ( { X , Y } = { a , b } -> ( X e. V /\ Y e. V ) ) ) )
21 20 com23 
 |-  ( ( a e. V /\ b e. V ) -> ( { X , Y } = { a , b } -> ( ( X e. U /\ Y e. W ) -> ( X e. V /\ Y e. V ) ) ) )
22 21 rexlimivv 
 |-  ( E. a e. V E. b e. V { X , Y } = { a , b } -> ( ( X e. U /\ Y e. W ) -> ( X e. V /\ Y e. V ) ) )
23 1 22 syl 
 |-  ( { X , Y } e. ( Pairs ` V ) -> ( ( X e. U /\ Y e. W ) -> ( X e. V /\ Y e. V ) ) )
24 23 imp 
 |-  ( ( { X , Y } e. ( Pairs ` V ) /\ ( X e. U /\ Y e. W ) ) -> ( X e. V /\ Y e. V ) )