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 ∈ V ∧ I ∈ ℕ ∧ Y = if I ≤ 1 st ⁡ X I 1 st ⁡ X if I ≤ 2 nd ⁡ X 2 nd ⁡ X I → G sSet I E Struct Y

Proof

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