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 ( 𝐼 ≤ ( 1^st ‘ 𝑋 ) , 𝐼 , ( 1^st ‘ 𝑋 ) ) , if ( 𝐼 ≤ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) , 𝐼 ) ⟩ ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) Struct 𝑌 )

Proof

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

Metamath Proof Explorer

Theorem setsstruct2

Proof