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 ( ( ( 𝐺 Struct 𝑋𝐸𝑉𝐼 ∈ ℕ ) ∧ 𝑌 = ⟨ if ( 𝐼 ≤ ( 1st𝑋 ) , 𝐼 , ( 1st𝑋 ) ) , if ( 𝐼 ≤ ( 2nd𝑋 ) , ( 2nd𝑋 ) , 𝐼 ) ⟩ ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) Struct 𝑌 )

Proof

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