This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) } )