Metamath Proof Explorer

Theorem setsexstruct2

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

Ref Expression
Assertion setsexstruct2 ⊢ G Struct X ∧ E ∈ V ∧ I ∈ ℕ → ∃ y G sSet I E Struct y

Proof

Step Hyp Ref Expression
1 opex ⊢ if I ≤ 1 st ⁡ X I 1 st ⁡ X if I ≤ 2 nd ⁡ X 2 nd ⁡ X I ∈ V
2 1 a1i ⊢ G Struct X ∧ E ∈ V ∧ I ∈ ℕ → if I ≤ 1 st ⁡ X I 1 st ⁡ X if I ≤ 2 nd ⁡ X 2 nd ⁡ X I ∈ V
3 eqidd ⊢ G Struct X ∧ E ∈ V ∧ I ∈ ℕ → 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
4 setsstruct2 ⊢ G Struct X ∧ E ∈ V ∧ I ∈ ℕ ∧ 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 → G sSet I E Struct if I ≤ 1 st ⁡ X I 1 st ⁡ X if I ≤ 2 nd ⁡ X 2 nd ⁡ X I
5 3 4 mpdan ⊢ 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
6 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
7 2 5 6 spcedv ⊢ G Struct X ∧ E ∈ V ∧ I ∈ ℕ → ∃ y G sSet I E Struct y