Metamath Proof Explorer

Theorem setsstruct2

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

Ref Expression
Assertion setsstruct2 
|- ( ( ( G Struct X /\ E e. V /\ I e. NN ) /\ Y = <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) -> ( G sSet <. I , E >. ) Struct Y )

Proof

Step Hyp Ref Expression
1 isstruct2 
 |-  ( G Struct X <-> ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( G \ { (/) } ) /\ dom G C_ ( ... ` X ) ) )
2 elin 
 |-  ( X e. ( <_ i^i ( NN X. NN ) ) <-> ( X e. <_ /\ X e. ( NN X. NN ) ) )
3 elxp6 
 |-  ( X e. ( NN X. NN ) <-> ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) ) )
4 eleq1 
 |-  ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. -> ( X e. <_ <-> <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ ) )
5 4 adantr 
 |-  ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) ) -> ( X e. <_ <-> <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ ) )
6 simp3 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> I e. NN )
7 simp1l 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> ( 1st ` X ) e. NN )
8 6 7 ifcld 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) e. NN )
9 8 nnred 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) e. RR )
10 6 nnred 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> I e. RR )
11 simp1r 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> ( 2nd ` X ) e. NN )
12 11 6 ifcld 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) e. NN )
13 12 nnred 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) e. RR )
14 nnre 
 |-  ( ( 1st ` X ) e. NN -> ( 1st ` X ) e. RR )
15 14 adantr 
 |-  ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) -> ( 1st ` X ) e. RR )
16 nnre 
 |-  ( I e. NN -> I e. RR )
17 15 16 anim12i 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ I e. NN ) -> ( ( 1st ` X ) e. RR /\ I e. RR ) )
18 17 3adant2 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> ( ( 1st ` X ) e. RR /\ I e. RR ) )
19 18 ancomd 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> ( I e. RR /\ ( 1st ` X ) e. RR ) )
20 min1 
 |-  ( ( I e. RR /\ ( 1st ` X ) e. RR ) -> if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) <_ I )
21 19 20 syl 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) <_ I )
22 nnre 
 |-  ( ( 2nd ` X ) e. NN -> ( 2nd ` X ) e. RR )
23 22 adantl 
 |-  ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) -> ( 2nd ` X ) e. RR )
24 23 16 anim12i 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ I e. NN ) -> ( ( 2nd ` X ) e. RR /\ I e. RR ) )
25 24 3adant2 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> ( ( 2nd ` X ) e. RR /\ I e. RR ) )
26 25 ancomd 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> ( I e. RR /\ ( 2nd ` X ) e. RR ) )
27 max1 
 |-  ( ( I e. RR /\ ( 2nd ` X ) e. RR ) -> I <_ if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) )
28 26 27 syl 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> I <_ if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) )
29 9 10 13 21 28 letrd 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) <_ if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) )
30 df-br 
 |-  ( 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 ) >. e. <_ )
31 29 30 sylib 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. <_ )
32 8 12 opelxpd 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. ( NN X. NN ) )
33 31 32 elind 
 |-  ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ /\ I e. NN ) -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. ( <_ i^i ( NN X. NN ) ) )
34 33 3exp 
 |-  ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) -> ( <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ -> ( I e. NN -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. ( <_ i^i ( NN X. NN ) ) ) ) )
35 34 adantl 
 |-  ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) ) -> ( <. ( 1st ` X ) , ( 2nd ` X ) >. e. <_ -> ( I e. NN -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. ( <_ i^i ( NN X. NN ) ) ) ) )
36 5 35 sylbid 
 |-  ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) ) -> ( X e. <_ -> ( I e. NN -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. ( <_ i^i ( NN X. NN ) ) ) ) )
37 3 36 sylbi 
 |-  ( X e. ( NN X. NN ) -> ( X e. <_ -> ( I e. NN -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. ( <_ i^i ( NN X. NN ) ) ) ) )
38 37 impcom 
 |-  ( ( X e. <_ /\ X e. ( NN X. NN ) ) -> ( I e. NN -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. ( <_ i^i ( NN X. NN ) ) ) )
39 2 38 sylbi 
 |-  ( X e. ( <_ i^i ( NN X. NN ) ) -> ( I e. NN -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. ( <_ i^i ( NN X. NN ) ) ) )
40 39 3ad2ant1 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( G \ { (/) } ) /\ dom G C_ ( ... ` X ) ) -> ( I e. NN -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. ( <_ i^i ( NN X. NN ) ) ) )
41 1 40 sylbi 
 |-  ( G Struct X -> ( I e. NN -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. ( <_ i^i ( NN X. NN ) ) ) )
42 41 imp 
 |-  ( ( G Struct X /\ I e. NN ) -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. ( <_ i^i ( NN X. NN ) ) )
43 42 3adant2 
 |-  ( ( G Struct X /\ E e. V /\ I e. NN ) -> <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. e. ( <_ i^i ( NN X. NN ) ) )
44 structex 
 |-  ( G Struct X -> G e. _V )
45 structn0fun 
 |-  ( G Struct X -> Fun ( G \ { (/) } ) )
46 44 45 jca 
 |-  ( G Struct X -> ( G e. _V /\ Fun ( G \ { (/) } ) ) )
47 46 3ad2ant1 
 |-  ( ( G Struct X /\ E e. V /\ I e. NN ) -> ( G e. _V /\ Fun ( G \ { (/) } ) ) )
48 simp3 
 |-  ( ( G Struct X /\ E e. V /\ I e. NN ) -> I e. NN )
49 simp2 
 |-  ( ( G Struct X /\ E e. V /\ I e. NN ) -> E e. V )
50 setsfun0 
 |-  ( ( ( G e. _V /\ Fun ( G \ { (/) } ) ) /\ ( I e. NN /\ E e. V ) ) -> Fun ( ( G sSet <. I , E >. ) \ { (/) } ) )
51 47 48 49 50 syl12anc 
 |-  ( ( G Struct X /\ E e. V /\ I e. NN ) -> Fun ( ( G sSet <. I , E >. ) \ { (/) } ) )
52 44 3ad2ant1 
 |-  ( ( G Struct X /\ E e. V /\ I e. NN ) -> G e. _V )
53 setsdm 
 |-  ( ( G e. _V /\ E e. V ) -> dom ( G sSet <. I , E >. ) = ( dom G u. { I } ) )
54 52 49 53 syl2anc 
 |-  ( ( G Struct X /\ E e. V /\ I e. NN ) -> dom ( G sSet <. I , E >. ) = ( dom G u. { I } ) )
55 fveq2 
 |-  ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. -> ( ... ` X ) = ( ... ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) )
56 df-ov 
 |-  ( ( 1st ` X ) ... ( 2nd ` X ) ) = ( ... ` <. ( 1st ` X ) , ( 2nd ` X ) >. )
57 55 56 eqtr4di 
 |-  ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. -> ( ... ` X ) = ( ( 1st ` X ) ... ( 2nd ` X ) ) )
58 57 sseq2d 
 |-  ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. -> ( dom G C_ ( ... ` X ) <-> dom G C_ ( ( 1st ` X ) ... ( 2nd ` X ) ) ) )
59 58 adantr 
 |-  ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) ) -> ( dom G C_ ( ... ` X ) <-> dom G C_ ( ( 1st ` X ) ... ( 2nd ` X ) ) ) )
60 df-3an 
 |-  ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN /\ I e. NN ) <-> ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ I e. NN ) )
61 nnz 
 |-  ( ( 1st ` X ) e. NN -> ( 1st ` X ) e. ZZ )
62 nnz 
 |-  ( ( 2nd ` X ) e. NN -> ( 2nd ` X ) e. ZZ )
63 nnz 
 |-  ( I e. NN -> I e. ZZ )
64 61 62 63 3anim123i 
 |-  ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN /\ I e. NN ) -> ( ( 1st ` X ) e. ZZ /\ ( 2nd ` X ) e. ZZ /\ I e. ZZ ) )
65 ssfzunsnext 
 |-  ( ( dom G C_ ( ( 1st ` X ) ... ( 2nd ` X ) ) /\ ( ( 1st ` X ) e. ZZ /\ ( 2nd ` X ) e. ZZ /\ I e. ZZ ) ) -> ( dom G u. { I } ) C_ ( if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) ... if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) ) )
66 df-ov 
 |-  ( 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 ) >. )
67 65 66 sseqtrdi 
 |-  ( ( dom G C_ ( ( 1st ` X ) ... ( 2nd ` X ) ) /\ ( ( 1st ` X ) e. ZZ /\ ( 2nd ` X ) e. ZZ /\ I e. ZZ ) ) -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) )
68 64 67 sylan2 
 |-  ( ( dom G C_ ( ( 1st ` X ) ... ( 2nd ` X ) ) /\ ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN /\ I e. NN ) ) -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) )
69 68 ex 
 |-  ( dom G C_ ( ( 1st ` X ) ... ( 2nd ` X ) ) -> ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN /\ I e. NN ) -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) ) )
70 60 69 biimtrrid 
 |-  ( dom G C_ ( ( 1st ` X ) ... ( 2nd ` X ) ) -> ( ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) /\ I e. NN ) -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) ) )
71 70 expd 
 |-  ( dom G C_ ( ( 1st ` X ) ... ( 2nd ` X ) ) -> ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) -> ( I e. NN -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) ) ) )
72 71 com12 
 |-  ( ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) -> ( dom G C_ ( ( 1st ` X ) ... ( 2nd ` X ) ) -> ( I e. NN -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) ) ) )
73 72 adantl 
 |-  ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) ) -> ( dom G C_ ( ( 1st ` X ) ... ( 2nd ` X ) ) -> ( I e. NN -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) ) ) )
74 59 73 sylbid 
 |-  ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. NN /\ ( 2nd ` X ) e. NN ) ) -> ( dom G C_ ( ... ` X ) -> ( I e. NN -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) ) ) )
75 3 74 sylbi 
 |-  ( X e. ( NN X. NN ) -> ( dom G C_ ( ... ` X ) -> ( I e. NN -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) ) ) )
76 75 adantl 
 |-  ( ( X e. <_ /\ X e. ( NN X. NN ) ) -> ( dom G C_ ( ... ` X ) -> ( I e. NN -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) ) ) )
77 2 76 sylbi 
 |-  ( X e. ( <_ i^i ( NN X. NN ) ) -> ( dom G C_ ( ... ` X ) -> ( I e. NN -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) ) ) )
78 77 imp 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ dom G C_ ( ... ` X ) ) -> ( I e. NN -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) ) )
79 78 3adant2 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( G \ { (/) } ) /\ dom G C_ ( ... ` X ) ) -> ( I e. NN -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) ) )
80 1 79 sylbi 
 |-  ( G Struct X -> ( I e. NN -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) ) )
81 80 imp 
 |-  ( ( G Struct X /\ I e. NN ) -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) )
82 81 3adant2 
 |-  ( ( G Struct X /\ E e. V /\ I e. NN ) -> ( dom G u. { I } ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) )
83 54 82 eqsstrd 
 |-  ( ( G Struct X /\ E e. V /\ I e. NN ) -> dom ( G sSet <. I , E >. ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) )
84 isstruct2 
 |-  ( ( G sSet <. I , E >. ) Struct <. 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 ) >. e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( ( G sSet <. I , E >. ) \ { (/) } ) /\ dom ( G sSet <. I , E >. ) C_ ( ... ` <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) ) )
85 43 51 83 84 syl3anbrc 
 |-  ( ( 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 ) >. )
86 85 adantr 
 |-  ( ( ( G Struct X /\ E e. V /\ I e. NN ) /\ Y = <. 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 ) >. )
87 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 ) >. ) )
88 87 adantl 
 |-  ( ( ( G Struct X /\ E e. V /\ I e. NN ) /\ 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 ) >. ) )
89 86 88 mpbird 
 |-  ( ( ( G Struct X /\ E e. V /\ I e. NN ) /\ Y = <. if ( I <_ ( 1st ` X ) , I , ( 1st ` X ) ) , if ( I <_ ( 2nd ` X ) , ( 2nd ` X ) , I ) >. ) -> ( G sSet <. I , E >. ) Struct Y )