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 ⊢GStructX∧E∈V∧I∈ℕ∧Y=ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI→GsSetIEStructY

Proof

Step Hyp Ref Expression
1 isstruct2 ⊢GStructX↔X∈≤∩ℕ×ℕ∧Fun⁡G∖∅∧dom⁡G⊆…⁡X
2 elin ⊢X∈≤∩ℕ×ℕ↔X∈≤∧X∈ℕ×ℕ
3 elxp6 ⊢X∈ℕ×ℕ↔X=1st⁡X2nd⁡X∧1st⁡X∈ℕ∧2nd⁡X∈ℕ
4 eleq1 ⊢X=1st⁡X2nd⁡X→X∈≤↔1st⁡X2nd⁡X∈≤
5 4 adantr ⊢X=1st⁡X2nd⁡X∧1st⁡X∈ℕ∧2nd⁡X∈ℕ→X∈≤↔1st⁡X2nd⁡X∈≤
6 simp3 ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→I∈ℕ
7 simp1l ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→1st⁡X∈ℕ
8 6 7 ifcld ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→ifI≤1st⁡XI1st⁡X∈ℕ
9 8 nnred ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→ifI≤1st⁡XI1st⁡X∈ℝ
10 6 nnred ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→I∈ℝ
11 simp1r ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→2nd⁡X∈ℕ
12 11 6 ifcld ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→ifI≤2nd⁡X2nd⁡XI∈ℕ
13 12 nnred ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→ifI≤2nd⁡X2nd⁡XI∈ℝ
14 nnre ⊢1st⁡X∈ℕ→1st⁡X∈ℝ
15 14 adantr ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ→1st⁡X∈ℝ
16 nnre ⊢I∈ℕ→I∈ℝ
17 15 16 anim12i ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧I∈ℕ→1st⁡X∈ℝ∧I∈ℝ
18 17 3adant2 ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→1st⁡X∈ℝ∧I∈ℝ
19 18 ancomd ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→I∈ℝ∧1st⁡X∈ℝ
20 min1 ⊢I∈ℝ∧1st⁡X∈ℝ→ifI≤1st⁡XI1st⁡X≤I
21 19 20 syl ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→ifI≤1st⁡XI1st⁡X≤I
22 nnre ⊢2nd⁡X∈ℕ→2nd⁡X∈ℝ
23 22 adantl ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ→2nd⁡X∈ℝ
24 23 16 anim12i ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧I∈ℕ→2nd⁡X∈ℝ∧I∈ℝ
25 24 3adant2 ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→2nd⁡X∈ℝ∧I∈ℝ
26 25 ancomd ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→I∈ℝ∧2nd⁡X∈ℝ
27 max1 ⊢I∈ℝ∧2nd⁡X∈ℝ→I≤ifI≤2nd⁡X2nd⁡XI
28 26 27 syl ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→I≤ifI≤2nd⁡X2nd⁡XI
29 9 10 13 21 28 letrd ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→ifI≤1st⁡XI1st⁡X≤ifI≤2nd⁡X2nd⁡XI
30 df-br ⊢ifI≤1st⁡XI1st⁡X≤ifI≤2nd⁡X2nd⁡XI↔ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤
31 29 30 sylib ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤
32 8 12 opelxpd ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈ℕ×ℕ
33 31 32 elind ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧1st⁡X2nd⁡X∈≤∧I∈ℕ→ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤∩ℕ×ℕ
34 33 3exp ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ→1st⁡X2nd⁡X∈≤→I∈ℕ→ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤∩ℕ×ℕ
35 34 adantl ⊢X=1st⁡X2nd⁡X∧1st⁡X∈ℕ∧2nd⁡X∈ℕ→1st⁡X2nd⁡X∈≤→I∈ℕ→ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤∩ℕ×ℕ
36 5 35 sylbid ⊢X=1st⁡X2nd⁡X∧1st⁡X∈ℕ∧2nd⁡X∈ℕ→X∈≤→I∈ℕ→ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤∩ℕ×ℕ
37 3 36 sylbi ⊢X∈ℕ×ℕ→X∈≤→I∈ℕ→ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤∩ℕ×ℕ
38 37 impcom ⊢X∈≤∧X∈ℕ×ℕ→I∈ℕ→ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤∩ℕ×ℕ
39 2 38 sylbi ⊢X∈≤∩ℕ×ℕ→I∈ℕ→ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤∩ℕ×ℕ
40 39 3ad2ant1 ⊢X∈≤∩ℕ×ℕ∧Fun⁡G∖∅∧dom⁡G⊆…⁡X→I∈ℕ→ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤∩ℕ×ℕ
41 1 40 sylbi ⊢GStructX→I∈ℕ→ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤∩ℕ×ℕ
42 41 imp ⊢GStructX∧I∈ℕ→ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤∩ℕ×ℕ
43 42 3adant2 ⊢GStructX∧E∈V∧I∈ℕ→ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤∩ℕ×ℕ
44 structex ⊢GStructX→G∈V
45 structn0fun ⊢GStructX→Fun⁡G∖∅
46 44 45 jca ⊢GStructX→G∈V∧Fun⁡G∖∅
47 46 3ad2ant1 ⊢GStructX∧E∈V∧I∈ℕ→G∈V∧Fun⁡G∖∅
48 simp3 ⊢GStructX∧E∈V∧I∈ℕ→I∈ℕ
49 simp2 ⊢GStructX∧E∈V∧I∈ℕ→E∈V
50 setsfun0 ⊢G∈V∧Fun⁡G∖∅∧I∈ℕ∧E∈V→Fun⁡GsSetIE∖∅
51 47 48 49 50 syl12anc ⊢GStructX∧E∈V∧I∈ℕ→Fun⁡GsSetIE∖∅
52 44 3ad2ant1 ⊢GStructX∧E∈V∧I∈ℕ→G∈V
53 setsdm ⊢G∈V∧E∈V→dom⁡GsSetIE=dom⁡G∪I
54 52 49 53 syl2anc ⊢GStructX∧E∈V∧I∈ℕ→dom⁡GsSetIE=dom⁡G∪I
55 fveq2 ⊢X=1st⁡X2nd⁡X→…⁡X=…⁡1st⁡X2nd⁡X
56 df-ov ⊢1st⁡X…2nd⁡X=…⁡1st⁡X2nd⁡X
57 55 56 eqtr4di ⊢X=1st⁡X2nd⁡X→…⁡X=1st⁡X…2nd⁡X
58 57 sseq2d ⊢X=1st⁡X2nd⁡X→dom⁡G⊆…⁡X↔dom⁡G⊆1st⁡X…2nd⁡X
59 58 adantr ⊢X=1st⁡X2nd⁡X∧1st⁡X∈ℕ∧2nd⁡X∈ℕ→dom⁡G⊆…⁡X↔dom⁡G⊆1st⁡X…2nd⁡X
60 df-3an ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧I∈ℕ↔1st⁡X∈ℕ∧2nd⁡X∈ℕ∧I∈ℕ
61 nnz ⊢1st⁡X∈ℕ→1st⁡X∈ℤ
62 nnz ⊢2nd⁡X∈ℕ→2nd⁡X∈ℤ
63 nnz ⊢I∈ℕ→I∈ℤ
64 61 62 63 3anim123i ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ∧I∈ℕ→1st⁡X∈ℤ∧2nd⁡X∈ℤ∧I∈ℤ
65 ssfzunsnext ⊢dom⁡G⊆1st⁡X…2nd⁡X∧1st⁡X∈ℤ∧2nd⁡X∈ℤ∧I∈ℤ→dom⁡G∪I⊆ifI≤1st⁡XI1st⁡X…ifI≤2nd⁡X2nd⁡XI
66 df-ov ⊢ifI≤1st⁡XI1st⁡X…ifI≤2nd⁡X2nd⁡XI=…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
67 65 66 sseqtrdi ⊢dom⁡G⊆1st⁡X…2nd⁡X∧1st⁡X∈ℤ∧2nd⁡X∈ℤ∧I∈ℤ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
68 64 67 sylan2 ⊢dom⁡G⊆1st⁡X…2nd⁡X∧1st⁡X∈ℕ∧2nd⁡X∈ℕ∧I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
69 68 ex ⊢dom⁡G⊆1st⁡X…2nd⁡X→1st⁡X∈ℕ∧2nd⁡X∈ℕ∧I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
70 60 69 biimtrrid ⊢dom⁡G⊆1st⁡X…2nd⁡X→1st⁡X∈ℕ∧2nd⁡X∈ℕ∧I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
71 70 expd ⊢dom⁡G⊆1st⁡X…2nd⁡X→1st⁡X∈ℕ∧2nd⁡X∈ℕ→I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
72 71 com12 ⊢1st⁡X∈ℕ∧2nd⁡X∈ℕ→dom⁡G⊆1st⁡X…2nd⁡X→I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
73 72 adantl ⊢X=1st⁡X2nd⁡X∧1st⁡X∈ℕ∧2nd⁡X∈ℕ→dom⁡G⊆1st⁡X…2nd⁡X→I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
74 59 73 sylbid ⊢X=1st⁡X2nd⁡X∧1st⁡X∈ℕ∧2nd⁡X∈ℕ→dom⁡G⊆…⁡X→I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
75 3 74 sylbi ⊢X∈ℕ×ℕ→dom⁡G⊆…⁡X→I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
76 75 adantl ⊢X∈≤∧X∈ℕ×ℕ→dom⁡G⊆…⁡X→I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
77 2 76 sylbi ⊢X∈≤∩ℕ×ℕ→dom⁡G⊆…⁡X→I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
78 77 imp ⊢X∈≤∩ℕ×ℕ∧dom⁡G⊆…⁡X→I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
79 78 3adant2 ⊢X∈≤∩ℕ×ℕ∧Fun⁡G∖∅∧dom⁡G⊆…⁡X→I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
80 1 79 sylbi ⊢GStructX→I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
81 80 imp ⊢GStructX∧I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
82 81 3adant2 ⊢GStructX∧E∈V∧I∈ℕ→dom⁡G∪I⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
83 54 82 eqsstrd ⊢GStructX∧E∈V∧I∈ℕ→dom⁡GsSetIE⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
84 isstruct2 ⊢GsSetIEStructifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI↔ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI∈≤∩ℕ×ℕ∧Fun⁡GsSetIE∖∅∧dom⁡GsSetIE⊆…⁡ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
85 43 51 83 84 syl3anbrc ⊢GStructX∧E∈V∧I∈ℕ→GsSetIEStructifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
86 85 adantr ⊢GStructX∧E∈V∧I∈ℕ∧Y=ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI→GsSetIEStructifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
87 breq2 ⊢Y=ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI→GsSetIEStructY↔GsSetIEStructifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
88 87 adantl ⊢GStructX∧E∈V∧I∈ℕ∧Y=ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI→GsSetIEStructY↔GsSetIEStructifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI
89 86 88 mpbird ⊢GStructX∧E∈V∧I∈ℕ∧Y=ifI≤1st⁡XI1st⁡XifI≤2nd⁡X2nd⁡XI→GsSetIEStructY