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 )

Metamath Proof Explorer

Theorem cusgrexilem2

Proof