Metamath Proof Explorer

Theorem sprsymrelfolem1

Description: Lemma 1 for sprsymrelfo . (Contributed by AV, 22-Nov-2021)

Ref Expression
Hypothesis sprsymrelfo.q 
|- Q = { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a R b ) }
Assertion sprsymrelfolem1 
|- Q e. ~P ( Pairs ` V )

Proof

Step Hyp Ref Expression
1 sprsymrelfo.q 
 |-  Q = { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a R b ) }
2 fvex 
 |-  ( Pairs ` V ) e. _V
3 ssrab2 
 |-  { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a R b ) } C_ ( Pairs ` V )
4 2 3 elpwi2 
 |-  { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a R b ) } e. ~P ( Pairs ` V )
5 1 4 eqeltri 
 |-  Q e. ~P ( Pairs ` V )