Theorem fnwe2lem1

Description: Lemma for fnwe2 . Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015)

	Ref	Expression
Hypotheses	fnwe2.su	|- ( z = ( F ` x ) -> S = U )
	fnwe2.t	|- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }
	fnwe2.s	|- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )
Assertion	fnwe2lem1	|- ( ( ph /\ a e. A ) -> [_ ( F ` a ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` a ) } )

Proof

Step	Hyp	Ref	Expression
1		fnwe2.su	|- ( z = ( F ` x ) -> S = U )
2		fnwe2.t	|- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }
3		fnwe2.s	|- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )
4	3	ralrimiva	|- ( ph -> A. x e. A U We { y e. A | ( F ` y ) = ( F ` x ) } )
5		fveq2	|- ( a = x -> ( F ` a ) = ( F ` x ) )
6	5	csbeq1d	|- ( a = x -> [_ ( F ` a ) / z ]_ S = [_ ( F ` x ) / z ]_ S )
7		fvex	|- ( F ` x ) e. _V
8	7 1	csbie	|- [_ ( F ` x ) / z ]_ S = U
9	6 8	eqtrdi	|- ( a = x -> [_ ( F ` a ) / z ]_ S = U )
10	5	eqeq2d	|- ( a = x -> ( ( F ` y ) = ( F ` a ) <-> ( F ` y ) = ( F ` x ) ) )
11	10	rabbidv	|- ( a = x -> { y e. A | ( F ` y ) = ( F ` a ) } = { y e. A | ( F ` y ) = ( F ` x ) } )
12	9 11	weeq12d	|- ( a = x -> ( [_ ( F ` a ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` a ) } <-> U We { y e. A | ( F ` y ) = ( F ` x ) } ) )
13	12	cbvralvw	|- ( A. a e. A [_ ( F ` a ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` a ) } <-> A. x e. A U We { y e. A | ( F ` y ) = ( F ` x ) } )
14	4 13	sylibr	|- ( ph -> A. a e. A [_ ( F ` a ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` a ) } )
15	14	r19.21bi	|- ( ( ph /\ a e. A ) -> [_ ( F ` a ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` a ) } )