Metamath Proof Explorer


Theorem strfv3

Description: Variant on strfv for large structures. (Contributed by Mario Carneiro, 10-Jan-2017)

Ref Expression
Hypotheses strfv3.u
|- ( ph -> U = S )
strfv3.s
|- S Struct X
strfv3.e
|- E = Slot ( E ` ndx )
strfv3.n
|- { <. ( E ` ndx ) , C >. } C_ S
strfv3.c
|- ( ph -> C e. V )
strfv3.a
|- A = ( E ` U )
Assertion strfv3
|- ( ph -> A = C )

Proof

Step Hyp Ref Expression
1 strfv3.u
 |-  ( ph -> U = S )
2 strfv3.s
 |-  S Struct X
3 strfv3.e
 |-  E = Slot ( E ` ndx )
4 strfv3.n
 |-  { <. ( E ` ndx ) , C >. } C_ S
5 strfv3.c
 |-  ( ph -> C e. V )
6 strfv3.a
 |-  A = ( E ` U )
7 2 3 4 strfv
 |-  ( C e. V -> C = ( E ` S ) )
8 5 7 syl
 |-  ( ph -> C = ( E ` S ) )
9 1 fveq2d
 |-  ( ph -> ( E ` U ) = ( E ` S ) )
10 8 9 eqtr4d
 |-  ( ph -> C = ( E ` U ) )
11 6 10 eqtr4id
 |-  ( ph -> A = C )