Metamath Proof Explorer

Theorem pr2cv

Description: If an unordered pair is equinumerous to ordinal two, then both parts are sets. (Contributed by RP, 8-Oct-2023)

Ref Expression
Assertion pr2cv 
|- ( { A , B } ~~ 2o -> ( A e. _V /\ B e. _V ) )

Proof

Step Hyp Ref Expression
1 en2 
 |-  ( { A , B } ~~ 2o -> E. x E. y { A , B } = { x , y } )
2 breq1 
 |-  ( { A , B } = { x , y } -> ( { A , B } ~~ 2o <-> { x , y } ~~ 2o ) )
3 vex 
 |-  x e. _V
4 vex 
 |-  y e. _V
5 pr2ne 
 |-  ( ( x e. _V /\ y e. _V ) -> ( { x , y } ~~ 2o <-> x =/= y ) )
6 5 el2v 
 |-  ( { x , y } ~~ 2o <-> x =/= y )
7 6 biimpi 
 |-  ( { x , y } ~~ 2o -> x =/= y )
8 preq12nebg 
 |-  ( ( x e. _V /\ y e. _V /\ x =/= y ) -> ( { x , y } = { A , B } <-> ( ( x = A /\ y = B ) \/ ( x = B /\ y = A ) ) ) )
9 eqvisset 
 |-  ( x = A -> A e. _V )
10 eqvisset 
 |-  ( y = B -> B e. _V )
11 9 10 anim12i 
 |-  ( ( x = A /\ y = B ) -> ( A e. _V /\ B e. _V ) )
12 eqvisset 
 |-  ( x = B -> B e. _V )
13 eqvisset 
 |-  ( y = A -> A e. _V )
14 12 13 anim12ci 
 |-  ( ( x = B /\ y = A ) -> ( A e. _V /\ B e. _V ) )
15 11 14 jaoi 
 |-  ( ( ( x = A /\ y = B ) \/ ( x = B /\ y = A ) ) -> ( A e. _V /\ B e. _V ) )
16 8 15 syl6bi 
 |-  ( ( x e. _V /\ y e. _V /\ x =/= y ) -> ( { x , y } = { A , B } -> ( A e. _V /\ B e. _V ) ) )
17 3 4 7 16 mp3an12i 
 |-  ( { x , y } ~~ 2o -> ( { x , y } = { A , B } -> ( A e. _V /\ B e. _V ) ) )
18 17 com12 
 |-  ( { x , y } = { A , B } -> ( { x , y } ~~ 2o -> ( A e. _V /\ B e. _V ) ) )
19 18 eqcoms 
 |-  ( { A , B } = { x , y } -> ( { x , y } ~~ 2o -> ( A e. _V /\ B e. _V ) ) )
20 2 19 sylbid 
 |-  ( { A , B } = { x , y } -> ( { A , B } ~~ 2o -> ( A e. _V /\ B e. _V ) ) )
21 20 exlimivv 
 |-  ( E. x E. y { A , B } = { x , y } -> ( { A , B } ~~ 2o -> ( A e. _V /\ B e. _V ) ) )
22 1 21 mpcom 
 |-  ( { A , B } ~~ 2o -> ( A e. _V /\ B e. _V ) )