This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem exprelprel

Description: If there is an element of the set of subsets with two elements in a set, an unordered pair of sets is in the set. (Contributed by Alexander van der Vekens, 12-Jul-2018)

Ref Expression
Assertion exprelprel 
|- ( E. p e. { e e. ~P V | ( # ` e ) = 2 } p e. X -> E. v e. V E. w e. V { v , w } e. X )

Proof

Step Hyp Ref Expression
1 elss2prb 
 |-  ( p e. { e e. ~P V | ( # ` e ) = 2 } <-> E. v e. V E. w e. V ( v =/= w /\ p = { v , w } ) )
2 eleq1 
 |-  ( p = { v , w } -> ( p e. X <-> { v , w } e. X ) )
3 2 adantl 
 |-  ( ( v =/= w /\ p = { v , w } ) -> ( p e. X <-> { v , w } e. X ) )
4 3 biimpcd 
 |-  ( p e. X -> ( ( v =/= w /\ p = { v , w } ) -> { v , w } e. X ) )
5 4 reximdv 
 |-  ( p e. X -> ( E. w e. V ( v =/= w /\ p = { v , w } ) -> E. w e. V { v , w } e. X ) )
6 5 reximdv 
 |-  ( p e. X -> ( E. v e. V E. w e. V ( v =/= w /\ p = { v , w } ) -> E. v e. V E. w e. V { v , w } e. X ) )
7 6 com12 
 |-  ( E. v e. V E. w e. V ( v =/= w /\ p = { v , w } ) -> ( p e. X -> E. v e. V E. w e. V { v , w } e. X ) )
8 1 7 sylbi 
 |-  ( p e. { e e. ~P V | ( # ` e ) = 2 } -> ( p e. X -> E. v e. V E. w e. V { v , w } e. X ) )
9 8 rexlimiv 
 |-  ( E. p e. { e e. ~P V | ( # ` e ) = 2 } p e. X -> E. v e. V E. w e. V { v , w } e. X )