Metamath Proof Explorer

Theorem upgr1elem

Description: Lemma for upgr1e and uspgr1e . (Contributed by AV, 16-Oct-2020)

Ref Expression
Hypotheses upgr1elem.s 
|- ( ph -> { B , C } e. S )
upgr1elem.b 
|- ( ph -> B e. W )
Assertion upgr1elem 
|- ( ph -> { { B , C } } C_ { x e. ( S \ { (/) } ) | ( # ` x ) <_ 2 } )

Proof

Step Hyp Ref Expression
1 upgr1elem.s 
 |-  ( ph -> { B , C } e. S )
2 upgr1elem.b 
 |-  ( ph -> B e. W )
3 fveq2 
 |-  ( x = { B , C } -> ( # ` x ) = ( # ` { B , C } ) )
4 3 breq1d 
 |-  ( x = { B , C } -> ( ( # ` x ) <_ 2 <-> ( # ` { B , C } ) <_ 2 ) )
5 prnzg 
 |-  ( B e. W -> { B , C } =/= (/) )
6 2 5 syl 
 |-  ( ph -> { B , C } =/= (/) )
7 eldifsn 
 |-  ( { B , C } e. ( S \ { (/) } ) <-> ( { B , C } e. S /\ { B , C } =/= (/) ) )
8 1 6 7 sylanbrc 
 |-  ( ph -> { B , C } e. ( S \ { (/) } ) )
9 hashprlei 
 |-  ( { B , C } e. Fin /\ ( # ` { B , C } ) <_ 2 )
10 9 simpri 
 |-  ( # ` { B , C } ) <_ 2
11 10 a1i 
 |-  ( ph -> ( # ` { B , C } ) <_ 2 )
12 4 8 11 elrabd 
 |-  ( ph -> { B , C } e. { x e. ( S \ { (/) } ) | ( # ` x ) <_ 2 } )
13 12 snssd 
 |-  ( ph -> { { B , C } } C_ { x e. ( S \ { (/) } ) | ( # ` x ) <_ 2 } )