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	⊢ ( ( 𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) → ∃ 𝑦 ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) Struct 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		opex	⊢ ⟨ if ( 𝐼 ≤ ( 1^st ‘ 𝑋 ) , 𝐼 , ( 1^st ‘ 𝑋 ) ) , if ( 𝐼 ≤ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) , 𝐼 ) ⟩ ∈ V
2	1	a1i	⊢ ( ( 𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) → ⟨ if ( 𝐼 ≤ ( 1^st ‘ 𝑋 ) , 𝐼 , ( 1^st ‘ 𝑋 ) ) , if ( 𝐼 ≤ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) , 𝐼 ) ⟩ ∈ V )
3		eqidd	⊢ ( ( 𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) → ⟨ if ( 𝐼 ≤ ( 1^st ‘ 𝑋 ) , 𝐼 , ( 1^st ‘ 𝑋 ) ) , if ( 𝐼 ≤ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) , 𝐼 ) ⟩ = ⟨ if ( 𝐼 ≤ ( 1^st ‘ 𝑋 ) , 𝐼 , ( 1^st ‘ 𝑋 ) ) , if ( 𝐼 ≤ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) , 𝐼 ) ⟩ )
4		setsstruct2	⊢ ( ( ( 𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) ∧ ⟨ if ( 𝐼 ≤ ( 1^st ‘ 𝑋 ) , 𝐼 , ( 1^st ‘ 𝑋 ) ) , if ( 𝐼 ≤ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) , 𝐼 ) ⟩ = ⟨ if ( 𝐼 ≤ ( 1^st ‘ 𝑋 ) , 𝐼 , ( 1^st ‘ 𝑋 ) ) , if ( 𝐼 ≤ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) , 𝐼 ) ⟩ ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) Struct ⟨ if ( 𝐼 ≤ ( 1^st ‘ 𝑋 ) , 𝐼 , ( 1^st ‘ 𝑋 ) ) , if ( 𝐼 ≤ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) , 𝐼 ) ⟩ )
5	3 4	mpdan	⊢ ( ( 𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) Struct ⟨ if ( 𝐼 ≤ ( 1^st ‘ 𝑋 ) , 𝐼 , ( 1^st ‘ 𝑋 ) ) , if ( 𝐼 ≤ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) , 𝐼 ) ⟩ )
6		breq2	⊢ ( 𝑦 = ⟨ if ( 𝐼 ≤ ( 1^st ‘ 𝑋 ) , 𝐼 , ( 1^st ‘ 𝑋 ) ) , if ( 𝐼 ≤ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) , 𝐼 ) ⟩ → ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) Struct 𝑦 ↔ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) Struct ⟨ if ( 𝐼 ≤ ( 1^st ‘ 𝑋 ) , 𝐼 , ( 1^st ‘ 𝑋 ) ) , if ( 𝐼 ≤ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) , 𝐼 ) ⟩ ) )
7	2 5 6	spcedv	⊢ ( ( 𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ ) → ∃ 𝑦 ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) Struct 𝑦 )