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 ( ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) Struct ⟨ 𝑀 , if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ⟩ )

Proof

Step Hyp Ref Expression
1 isstruct ⊢ ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ Fun ( 𝐺 ∖ { ∅ } ) ∧ dom 𝐺 ⊆ ( 𝑀 ... 𝑁 ) ) )
2 simp2 ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) ) → 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ )
3 simp3l ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) ) → 𝐸 ∈ 𝑉 )
4 1z ⊢ 1 ∈ ℤ
5 nnge1 ⊢ ( 𝑀 ∈ ℕ → 1 ≤ 𝑀 )
6 eluzuzle ⊢ ( ( 1 ∈ ℤ ∧ 1 ≤ 𝑀 ) → ( 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐼 ∈ ( ℤ≥ ‘ 1 ) ) )
7 4 5 6 sylancr ⊢ ( 𝑀 ∈ ℕ → ( 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐼 ∈ ( ℤ≥ ‘ 1 ) ) )
8 elnnuz ⊢ ( 𝐼 ∈ ℕ ↔ 𝐼 ∈ ( ℤ≥ ‘ 1 ) )
9 7 8 imbitrrdi ⊢ ( 𝑀 ∈ ℕ → ( 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐼 ∈ ℕ ) )
10 9 adantld ⊢ ( 𝑀 ∈ ℕ → ( ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐼 ∈ ℕ ) )
11 10 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) → ( ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐼 ∈ ℕ ) )
12 11 a1d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) → ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ → ( ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐼 ∈ ℕ ) ) )
13 12 3imp ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) ) → 𝐼 ∈ ℕ )
14 2 3 13 3jca ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) ) → ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) )
15 op1stg ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
16 15 breq2d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ↔ 𝐼 ≤ 𝑀 ) )
17 eqidd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐼 = 𝐼 )
18 16 17 15 ifbieq12d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) = if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) )
19 18 3adant3 ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) → if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) = if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) )
20 19 adantr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) ) → if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) = if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) )
21 eluz2 ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼 ) )
22 zre ⊢ ( 𝐼 ∈ ℤ → 𝐼 ∈ ℝ )
23 22 rexrd ⊢ ( 𝐼 ∈ ℤ → 𝐼 ∈ ℝ* )
24 23 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼 ) → 𝐼 ∈ ℝ* )
25 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
26 25 rexrd ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ* )
27 26 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼 ) → 𝑀 ∈ ℝ* )
28 simp3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼 ) → 𝑀 ≤ 𝐼 )
29 24 27 28 3jca ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼 ) → ( 𝐼 ∈ ℝ* ∧ 𝑀 ∈ ℝ* ∧ 𝑀 ≤ 𝐼 ) )
30 29 a1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼 ) → ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) → ( 𝐼 ∈ ℝ* ∧ 𝑀 ∈ ℝ* ∧ 𝑀 ≤ 𝐼 ) ) )
31 21 30 sylbi ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) → ( 𝐼 ∈ ℝ* ∧ 𝑀 ∈ ℝ* ∧ 𝑀 ≤ 𝐼 ) ) )
32 31 adantl ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) → ( 𝐼 ∈ ℝ* ∧ 𝑀 ∈ ℝ* ∧ 𝑀 ≤ 𝐼 ) ) )
33 32 impcom ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) ) → ( 𝐼 ∈ ℝ* ∧ 𝑀 ∈ ℝ* ∧ 𝑀 ≤ 𝐼 ) )
34 xrmineq ⊢ ( ( 𝐼 ∈ ℝ* ∧ 𝑀 ∈ ℝ* ∧ 𝑀 ≤ 𝐼 ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) = 𝑀 )
35 33 34 syl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) = 𝑀 )
36 20 35 eqtr2d ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) ) → 𝑀 = if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) )
37 36 3adant2 ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) ) → 𝑀 = if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) )
38 op2ndg ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑁 )
39 38 eqcomd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 = ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) )
40 39 breq2d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐼 ≤ 𝑁 ↔ 𝐼 ≤ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) )
41 40 39 17 ifbieq12d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) = if ( 𝐼 ≤ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 ) )
42 41 3adant3 ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) = if ( 𝐼 ≤ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 ) )
43 42 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) = if ( 𝐼 ≤ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 ) )
44 37 43 opeq12d ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) ) → ⟨ 𝑀 , if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ⟩ = ⟨ if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) , if ( 𝐼 ≤ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 ) ⟩ )
45 14 44 jca ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) ) → ( ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) ∧ ⟨ 𝑀 , if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ⟩ = ⟨ if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) , if ( 𝐼 ≤ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 ) ⟩ ) )
46 45 3exp ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) → ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ → ( ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) ∧ ⟨ 𝑀 , if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ⟩ = ⟨ if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) , if ( 𝐼 ≤ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 ) ⟩ ) ) ) )
47 46 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ Fun ( 𝐺 ∖ { ∅ } ) ∧ dom 𝐺 ⊆ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ → ( ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) ∧ ⟨ 𝑀 , if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ⟩ = ⟨ if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) , if ( 𝐼 ≤ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 ) ⟩ ) ) ) )
48 1 47 sylbi ⊢ ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ → ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ → ( ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) ∧ ⟨ 𝑀 , if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ⟩ = ⟨ if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) , if ( 𝐼 ≤ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 ) ⟩ ) ) ) )
49 48 pm2.43i ⊢ ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ → ( ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) ∧ ⟨ 𝑀 , if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ⟩ = ⟨ if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) , if ( 𝐼 ≤ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 ) ⟩ ) ) )
50 49 expdcom ⊢ ( 𝐸 ∈ 𝑉 → ( 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ → ( ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) ∧ ⟨ 𝑀 , if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ⟩ = ⟨ if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) , if ( 𝐼 ≤ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 ) ⟩ ) ) ) )
51 50 3imp ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ) → ( ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) ∧ ⟨ 𝑀 , if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ⟩ = ⟨ if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) , if ( 𝐼 ≤ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 ) ⟩ ) )
52 setsstruct2 ⊢ ( ( ( 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) ∧ ⟨ 𝑀 , if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ⟩ = ⟨ if ( 𝐼 ≤ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 , ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) , if ( 𝐼 ≤ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , 𝐼 ) ⟩ ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) Struct ⟨ 𝑀 , if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ⟩ )
53 51 52 syl ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐺 Struct ⟨ 𝑀 , 𝑁 ⟩ ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) Struct ⟨ 𝑀 , if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ⟩ )