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 )