Metamath Proof Explorer

Theorem prproe

Description: For an element of a proper unordered pair of elements of a class V , there is another (different) element of the class V which is an element of the proper pair. (Contributed by AV, 18-Dec-2021)

Ref Expression
Assertion prproe 
|- ( ( C e. { A , B } /\ A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } )

Proof

Step Hyp Ref Expression
1 elpri 
 |-  ( C e. { A , B } -> ( C = A \/ C = B ) )
2 simprrr 
 |-  ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B e. V )
3 necom 
 |-  ( A =/= B <-> B =/= A )
4 neeq2 
 |-  ( A = C -> ( B =/= A <-> B =/= C ) )
5 4 eqcoms 
 |-  ( C = A -> ( B =/= A <-> B =/= C ) )
6 5 biimpcd 
 |-  ( B =/= A -> ( C = A -> B =/= C ) )
7 3 6 sylbi 
 |-  ( A =/= B -> ( C = A -> B =/= C ) )
8 7 adantr 
 |-  ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> ( C = A -> B =/= C ) )
9 8 impcom 
 |-  ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B =/= C )
10 eldifsn 
 |-  ( B e. ( V \ { C } ) <-> ( B e. V /\ B =/= C ) )
11 2 9 10 sylanbrc 
 |-  ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B e. ( V \ { C } ) )
12 eleq1 
 |-  ( v = B -> ( v e. { A , B } <-> B e. { A , B } ) )
13 12 adantl 
 |-  ( ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) /\ v = B ) -> ( v e. { A , B } <-> B e. { A , B } ) )
14 prid2g 
 |-  ( B e. V -> B e. { A , B } )
15 14 adantl 
 |-  ( ( A e. V /\ B e. V ) -> B e. { A , B } )
16 15 adantl 
 |-  ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> B e. { A , B } )
17 16 adantl 
 |-  ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B e. { A , B } )
18 11 13 17 rspcedvd 
 |-  ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> E. v e. ( V \ { C } ) v e. { A , B } )
19 18 ex 
 |-  ( C = A -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) )
20 simprrl 
 |-  ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A e. V )
21 neeq2 
 |-  ( B = C -> ( A =/= B <-> A =/= C ) )
22 21 eqcoms 
 |-  ( C = B -> ( A =/= B <-> A =/= C ) )
23 22 biimpcd 
 |-  ( A =/= B -> ( C = B -> A =/= C ) )
24 23 adantr 
 |-  ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> ( C = B -> A =/= C ) )
25 24 impcom 
 |-  ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A =/= C )
26 eldifsn 
 |-  ( A e. ( V \ { C } ) <-> ( A e. V /\ A =/= C ) )
27 20 25 26 sylanbrc 
 |-  ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A e. ( V \ { C } ) )
28 eleq1 
 |-  ( v = A -> ( v e. { A , B } <-> A e. { A , B } ) )
29 28 adantl 
 |-  ( ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) /\ v = A ) -> ( v e. { A , B } <-> A e. { A , B } ) )
30 prid1g 
 |-  ( A e. V -> A e. { A , B } )
31 30 adantr 
 |-  ( ( A e. V /\ B e. V ) -> A e. { A , B } )
32 31 adantl 
 |-  ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> A e. { A , B } )
33 32 adantl 
 |-  ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A e. { A , B } )
34 27 29 33 rspcedvd 
 |-  ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> E. v e. ( V \ { C } ) v e. { A , B } )
35 34 ex 
 |-  ( C = B -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) )
36 19 35 jaoi 
 |-  ( ( C = A \/ C = B ) -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) )
37 1 36 syl 
 |-  ( C e. { A , B } -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) )
38 37 3impib 
 |-  ( ( C e. { A , B } /\ A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } )