Metamath Proof Explorer

Theorem cusgrexilem2

Description: Lemma 2 for cusgrexi . (Contributed by AV, 12-Jan-2018) (Revised by AV, 10-Nov-2021)

Ref Expression
Hypothesis usgrexi.p 
|- P = { x e. ~P V | ( # ` x ) = 2 }
Assertion cusgrexilem2 
|- ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> E. e e. ran ( _I |` P ) { v , n } C_ e )

Proof

Step Hyp Ref Expression
1 usgrexi.p 
 |-  P = { x e. ~P V | ( # ` x ) = 2 }
2 simpr 
 |-  ( ( V e. W /\ v e. V ) -> v e. V )
3 eldifi 
 |-  ( n e. ( V \ { v } ) -> n e. V )
4 prelpwi 
 |-  ( ( v e. V /\ n e. V ) -> { v , n } e. ~P V )
5 2 3 4 syl2an 
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> { v , n } e. ~P V )
6 eldifsni 
 |-  ( n e. ( V \ { v } ) -> n =/= v )
7 6 necomd 
 |-  ( n e. ( V \ { v } ) -> v =/= n )
8 7 adantl 
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> v =/= n )
9 hashprg 
 |-  ( ( v e. V /\ n e. V ) -> ( v =/= n <-> ( # ` { v , n } ) = 2 ) )
10 2 3 9 syl2an 
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> ( v =/= n <-> ( # ` { v , n } ) = 2 ) )
11 8 10 mpbid 
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> ( # ` { v , n } ) = 2 )
12 fveqeq2 
 |-  ( x = { v , n } -> ( ( # ` x ) = 2 <-> ( # ` { v , n } ) = 2 ) )
13 rnresi 
 |-  ran ( _I |` P ) = P
14 13 1 eqtri 
 |-  ran ( _I |` P ) = { x e. ~P V | ( # ` x ) = 2 }
15 12 14 elrab2 
 |-  ( { v , n } e. ran ( _I |` P ) <-> ( { v , n } e. ~P V /\ ( # ` { v , n } ) = 2 ) )
16 5 11 15 sylanbrc 
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> { v , n } e. ran ( _I |` P ) )
17 sseq2 
 |-  ( e = { v , n } -> ( { v , n } C_ e <-> { v , n } C_ { v , n } ) )
18 17 adantl 
 |-  ( ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) /\ e = { v , n } ) -> ( { v , n } C_ e <-> { v , n } C_ { v , n } ) )
19 ssidd 
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> { v , n } C_ { v , n } )
20 16 18 19 rspcedvd 
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> E. e e. ran ( _I |` P ) { v , n } C_ e )