Theorem rusgrnumwwlkslem

Description: Lemma for rusgrnumwwlks . (Contributed by Alexander van der Vekens, 23-Aug-2018)

	Ref	Expression
Assertion	rusgrnumwwlkslem	|- ( Y e. { w e. Z | ( w ` 0 ) = P } -> { w e. X | ( ph /\ ps ) } = { w e. X | ( ph /\ ( Y ` 0 ) = P /\ ps ) } )

Proof

Step	Hyp	Ref	Expression
1		fveq1	|- ( w = Y -> ( w ` 0 ) = ( Y ` 0 ) )
2	1	eqeq1d	|- ( w = Y -> ( ( w ` 0 ) = P <-> ( Y ` 0 ) = P ) )
3	2	elrab	|- ( Y e. { w e. Z | ( w ` 0 ) = P } <-> ( Y e. Z /\ ( Y ` 0 ) = P ) )
4		ibar	|- ( ( Y ` 0 ) = P -> ( ( ph /\ ps ) <-> ( ( Y ` 0 ) = P /\ ( ph /\ ps ) ) ) )
5		3anass	|- ( ( ( Y ` 0 ) = P /\ ph /\ ps ) <-> ( ( Y ` 0 ) = P /\ ( ph /\ ps ) ) )
6		3ancoma	|- ( ( ( Y ` 0 ) = P /\ ph /\ ps ) <-> ( ph /\ ( Y ` 0 ) = P /\ ps ) )
7	5 6	bitr3i	|- ( ( ( Y ` 0 ) = P /\ ( ph /\ ps ) ) <-> ( ph /\ ( Y ` 0 ) = P /\ ps ) )
8	4 7	bitrdi	|- ( ( Y ` 0 ) = P -> ( ( ph /\ ps ) <-> ( ph /\ ( Y ` 0 ) = P /\ ps ) ) )
9	8	ad2antlr	|- ( ( ( Y e. Z /\ ( Y ` 0 ) = P ) /\ w e. X ) -> ( ( ph /\ ps ) <-> ( ph /\ ( Y ` 0 ) = P /\ ps ) ) )
10	9	rabbidva	|- ( ( Y e. Z /\ ( Y ` 0 ) = P ) -> { w e. X | ( ph /\ ps ) } = { w e. X | ( ph /\ ( Y ` 0 ) = P /\ ps ) } )
11	3 10	sylbi	|- ( Y e. { w e. Z | ( w ` 0 ) = P } -> { w e. X | ( ph /\ ps ) } = { w e. X | ( ph /\ ( Y ` 0 ) = P /\ ps ) } )