Metamath Proof Explorer

Theorem setsstruct

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

Ref Expression
Assertion setsstruct 
|- ( ( E e. V /\ I e. ( ZZ>= ` M ) /\ G Struct <. M , N >. ) -> ( G sSet <. I , E >. ) Struct <. M , if ( I <_ N , N , I ) >. )

Proof

Step Hyp Ref Expression
1 isstruct 
 |-  ( G Struct <. M , N >. <-> ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ Fun ( G \ { (/) } ) /\ dom G C_ ( M ... N ) ) )
2 simp2 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ G Struct <. M , N >. /\ ( E e. V /\ I e. ( ZZ>= ` M ) ) ) -> G Struct <. M , N >. )
3 simp3l 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ G Struct <. M , N >. /\ ( E e. V /\ I e. ( ZZ>= ` M ) ) ) -> E e. V )
4 1z 
 |-  1 e. ZZ
5 nnge1 
 |-  ( M e. NN -> 1 <_ M )
6 eluzuzle 
 |-  ( ( 1 e. ZZ /\ 1 <_ M ) -> ( I e. ( ZZ>= ` M ) -> I e. ( ZZ>= ` 1 ) ) )
7 4 5 6 sylancr 
 |-  ( M e. NN -> ( I e. ( ZZ>= ` M ) -> I e. ( ZZ>= ` 1 ) ) )
8 elnnuz 
 |-  ( I e. NN <-> I e. ( ZZ>= ` 1 ) )
9 7 8 syl6ibr 
 |-  ( M e. NN -> ( I e. ( ZZ>= ` M ) -> I e. NN ) )
10 9 adantld 
 |-  ( M e. NN -> ( ( E e. V /\ I e. ( ZZ>= ` M ) ) -> I e. NN ) )
11 10 3ad2ant1 
 |-  ( ( M e. NN /\ N e. NN /\ M <_ N ) -> ( ( E e. V /\ I e. ( ZZ>= ` M ) ) -> I e. NN ) )
12 11 a1d 
 |-  ( ( M e. NN /\ N e. NN /\ M <_ N ) -> ( G Struct <. M , N >. -> ( ( E e. V /\ I e. ( ZZ>= ` M ) ) -> I e. NN ) ) )
13 12 3imp 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ G Struct <. M , N >. /\ ( E e. V /\ I e. ( ZZ>= ` M ) ) ) -> I e. NN )
14 2 3 13 3jca 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ G Struct <. M , N >. /\ ( E e. V /\ I e. ( ZZ>= ` M ) ) ) -> ( G Struct <. M , N >. /\ E e. V /\ I e. NN ) )
15 op1stg 
 |-  ( ( M e. NN /\ N e. NN ) -> ( 1st ` <. M , N >. ) = M )
16 15 breq2d 
 |-  ( ( M e. NN /\ N e. NN ) -> ( I <_ ( 1st ` <. M , N >. ) <-> I <_ M ) )
17 eqidd 
 |-  ( ( M e. NN /\ N e. NN ) -> I = I )
18 16 17 15 ifbieq12d 
 |-  ( ( M e. NN /\ N e. NN ) -> if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) = if ( I <_ M , I , M ) )
19 18 3adant3 
 |-  ( ( M e. NN /\ N e. NN /\ M <_ N ) -> if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) = if ( I <_ M , I , M ) )
20 19 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ ( E e. V /\ I e. ( ZZ>= ` M ) ) ) -> if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) = if ( I <_ M , I , M ) )
21 eluz2 
 |-  ( I e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ I e. ZZ /\ M <_ I ) )
22 zre 
 |-  ( I e. ZZ -> I e. RR )
23 22 rexrd 
 |-  ( I e. ZZ -> I e. RR* )
24 23 3ad2ant2 
 |-  ( ( M e. ZZ /\ I e. ZZ /\ M <_ I ) -> I e. RR* )
25 zre 
 |-  ( M e. ZZ -> M e. RR )
26 25 rexrd 
 |-  ( M e. ZZ -> M e. RR* )
27 26 3ad2ant1 
 |-  ( ( M e. ZZ /\ I e. ZZ /\ M <_ I ) -> M e. RR* )
28 simp3 
 |-  ( ( M e. ZZ /\ I e. ZZ /\ M <_ I ) -> M <_ I )
29 24 27 28 3jca 
 |-  ( ( M e. ZZ /\ I e. ZZ /\ M <_ I ) -> ( I e. RR* /\ M e. RR* /\ M <_ I ) )
30 29 a1d 
 |-  ( ( M e. ZZ /\ I e. ZZ /\ M <_ I ) -> ( ( M e. NN /\ N e. NN /\ M <_ N ) -> ( I e. RR* /\ M e. RR* /\ M <_ I ) ) )
31 21 30 sylbi 
 |-  ( I e. ( ZZ>= ` M ) -> ( ( M e. NN /\ N e. NN /\ M <_ N ) -> ( I e. RR* /\ M e. RR* /\ M <_ I ) ) )
32 31 adantl 
 |-  ( ( E e. V /\ I e. ( ZZ>= ` M ) ) -> ( ( M e. NN /\ N e. NN /\ M <_ N ) -> ( I e. RR* /\ M e. RR* /\ M <_ I ) ) )
33 32 impcom 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ ( E e. V /\ I e. ( ZZ>= ` M ) ) ) -> ( I e. RR* /\ M e. RR* /\ M <_ I ) )
34 xrmineq 
 |-  ( ( I e. RR* /\ M e. RR* /\ M <_ I ) -> if ( I <_ M , I , M ) = M )
35 33 34 syl 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ ( E e. V /\ I e. ( ZZ>= ` M ) ) ) -> if ( I <_ M , I , M ) = M )
36 20 35 eqtr2d 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ ( E e. V /\ I e. ( ZZ>= ` M ) ) ) -> M = if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) )
37 36 3adant2 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ G Struct <. M , N >. /\ ( E e. V /\ I e. ( ZZ>= ` M ) ) ) -> M = if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) )
38 op2ndg 
 |-  ( ( M e. NN /\ N e. NN ) -> ( 2nd ` <. M , N >. ) = N )
39 38 eqcomd 
 |-  ( ( M e. NN /\ N e. NN ) -> N = ( 2nd ` <. M , N >. ) )
40 39 breq2d 
 |-  ( ( M e. NN /\ N e. NN ) -> ( I <_ N <-> I <_ ( 2nd ` <. M , N >. ) ) )
41 40 39 17 ifbieq12d 
 |-  ( ( M e. NN /\ N e. NN ) -> if ( I <_ N , N , I ) = if ( I <_ ( 2nd ` <. M , N >. ) , ( 2nd ` <. M , N >. ) , I ) )
42 41 3adant3 
 |-  ( ( M e. NN /\ N e. NN /\ M <_ N ) -> if ( I <_ N , N , I ) = if ( I <_ ( 2nd ` <. M , N >. ) , ( 2nd ` <. M , N >. ) , I ) )
43 42 3ad2ant1 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ G Struct <. M , N >. /\ ( E e. V /\ I e. ( ZZ>= ` M ) ) ) -> if ( I <_ N , N , I ) = if ( I <_ ( 2nd ` <. M , N >. ) , ( 2nd ` <. M , N >. ) , I ) )
44 37 43 opeq12d 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ G Struct <. M , N >. /\ ( E e. V /\ I e. ( ZZ>= ` M ) ) ) -> <. M , if ( I <_ N , N , I ) >. = <. if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) , if ( I <_ ( 2nd ` <. M , N >. ) , ( 2nd ` <. M , N >. ) , I ) >. )
45 14 44 jca 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ G Struct <. M , N >. /\ ( E e. V /\ I e. ( ZZ>= ` M ) ) ) -> ( ( G Struct <. M , N >. /\ E e. V /\ I e. NN ) /\ <. M , if ( I <_ N , N , I ) >. = <. if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) , if ( I <_ ( 2nd ` <. M , N >. ) , ( 2nd ` <. M , N >. ) , I ) >. ) )
46 45 3exp 
 |-  ( ( M e. NN /\ N e. NN /\ M <_ N ) -> ( G Struct <. M , N >. -> ( ( E e. V /\ I e. ( ZZ>= ` M ) ) -> ( ( G Struct <. M , N >. /\ E e. V /\ I e. NN ) /\ <. M , if ( I <_ N , N , I ) >. = <. if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) , if ( I <_ ( 2nd ` <. M , N >. ) , ( 2nd ` <. M , N >. ) , I ) >. ) ) ) )
47 46 3ad2ant1 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ Fun ( G \ { (/) } ) /\ dom G C_ ( M ... N ) ) -> ( G Struct <. M , N >. -> ( ( E e. V /\ I e. ( ZZ>= ` M ) ) -> ( ( G Struct <. M , N >. /\ E e. V /\ I e. NN ) /\ <. M , if ( I <_ N , N , I ) >. = <. if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) , if ( I <_ ( 2nd ` <. M , N >. ) , ( 2nd ` <. M , N >. ) , I ) >. ) ) ) )
48 1 47 sylbi 
 |-  ( G Struct <. M , N >. -> ( G Struct <. M , N >. -> ( ( E e. V /\ I e. ( ZZ>= ` M ) ) -> ( ( G Struct <. M , N >. /\ E e. V /\ I e. NN ) /\ <. M , if ( I <_ N , N , I ) >. = <. if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) , if ( I <_ ( 2nd ` <. M , N >. ) , ( 2nd ` <. M , N >. ) , I ) >. ) ) ) )
49 48 pm2.43i 
 |-  ( G Struct <. M , N >. -> ( ( E e. V /\ I e. ( ZZ>= ` M ) ) -> ( ( G Struct <. M , N >. /\ E e. V /\ I e. NN ) /\ <. M , if ( I <_ N , N , I ) >. = <. if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) , if ( I <_ ( 2nd ` <. M , N >. ) , ( 2nd ` <. M , N >. ) , I ) >. ) ) )
50 49 expdcom 
 |-  ( E e. V -> ( I e. ( ZZ>= ` M ) -> ( G Struct <. M , N >. -> ( ( G Struct <. M , N >. /\ E e. V /\ I e. NN ) /\ <. M , if ( I <_ N , N , I ) >. = <. if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) , if ( I <_ ( 2nd ` <. M , N >. ) , ( 2nd ` <. M , N >. ) , I ) >. ) ) ) )
51 50 3imp 
 |-  ( ( E e. V /\ I e. ( ZZ>= ` M ) /\ G Struct <. M , N >. ) -> ( ( G Struct <. M , N >. /\ E e. V /\ I e. NN ) /\ <. M , if ( I <_ N , N , I ) >. = <. if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) , if ( I <_ ( 2nd ` <. M , N >. ) , ( 2nd ` <. M , N >. ) , I ) >. ) )
52 setsstruct2 
 |-  ( ( ( G Struct <. M , N >. /\ E e. V /\ I e. NN ) /\ <. M , if ( I <_ N , N , I ) >. = <. if ( I <_ ( 1st ` <. M , N >. ) , I , ( 1st ` <. M , N >. ) ) , if ( I <_ ( 2nd ` <. M , N >. ) , ( 2nd ` <. M , N >. ) , I ) >. ) -> ( G sSet <. I , E >. ) Struct <. M , if ( I <_ N , N , I ) >. )
53 51 52 syl 
 |-  ( ( E e. V /\ I e. ( ZZ>= ` M ) /\ G Struct <. M , N >. ) -> ( G sSet <. I , E >. ) Struct <. M , if ( I <_ N , N , I ) >. )