Metamath Proof Explorer

Theorem setsexstruct2

Description: An extensible structure with a replaced slot is an extensible structure. (Contributed by AV, 14-Nov-2021)

Ref Expression
Assertion setsexstruct2 
|- ( ( G Struct X /\ E e. V /\ I e. NN ) -> E. y ( G sSet <. I , E >. ) Struct y )

Proof

Step Hyp Ref Expression
1 opex 
 |-  <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. _V
2 1 a1i 
 |-  ( ( G Struct X /\ E e. V /\ I e. NN ) -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. _V )
3 eqidd 
 |-  ( ( G Struct X /\ E e. V /\ I e. NN ) -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. = <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. )
4 setsstruct2 
 |-  ( ( ( G Struct X /\ E e. V /\ I e. NN ) /\ <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. = <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) -> ( G sSet <. I , E >. ) Struct <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. )
5 3 4 mpdan 
 |-  ( ( G Struct X /\ E e. V /\ I e. NN ) -> ( G sSet <. I , E >. ) Struct <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. )
6 breq2 
 |-  ( y = <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. -> ( ( G sSet <. I , E >. ) Struct y <-> ( G sSet <. I , E >. ) Struct <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) )
7 2 5 6 spcedv 
 |-  ( ( G Struct X /\ E e. V /\ I e. NN ) -> E. y ( G sSet <. I , E >. ) Struct y )