Theorem ssfzunsnext 12386

Description: A subset of a finite sequence of integers extended by an integer is a subset of a (possibly extended) finite sequence of integers. (Contributed by AV, 13-Nov-2021.)

Assertion

Ref	Expression
ssfzunsnext	⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝑆 ∪ {𝐼}) ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))

Proof of Theorem ssfzunsnext

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 473	. . 3 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → 𝑆 ⊆ (𝑀...𝑁))
2		simp3 1063	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → 𝐼 ∈ ℤ)
3		simp1 1061	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → 𝑀 ∈ ℤ)
4	2, 3	ifcld 4131	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ∈ ℤ)
5	4	adantr 481	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ∈ ℤ)
6		elfzelz 12342	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ)
7	6	adantl 482	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ ℤ)
8	4	zred 11482	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ∈ ℝ)
9	8	adantr 481	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ∈ ℝ)
10		zre 11381	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
11	10	3ad2ant1 1082	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → 𝑀 ∈ ℝ)
12	11	adantr 481	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℝ)
13	6	zred 11482	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℝ)
14	13	adantl 482	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ ℝ)
15		zre 11381	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ ℝ)
16	10, 15	anim12i 590	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑀 ∈ ℝ ∧ 𝐼 ∈ ℝ))
17	16	ancomd 467	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ))
18	17	3adant2 1080	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ))
19	18	adantr 481	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ))
20		min2 12021	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ≤ 𝑀)
21	19, 20	syl 17	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ≤ 𝑀)
22		elfzle1 12344	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝑘)
23	22	adantl 482	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑀 ≤ 𝑘)
24	9, 12, 14, 21, 23	letrd 10194	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ≤ 𝑘)
25		eluz2 11693	. . . . . . . 8 ⊢ (𝑘 ∈ (ℤ≥‘if(𝐼 ≤ 𝑀, 𝐼, 𝑀)) ↔ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ≤ 𝑘))
26	5, 7, 24, 25	syl3anbrc 1246	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ (ℤ≥‘if(𝐼 ≤ 𝑀, 𝐼, 𝑀)))
27		simp2 1062	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → 𝑁 ∈ ℤ)
28	27, 2	ifcld 4131	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ)
29	28	adantr 481	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ)
30		zre 11381	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
31	30	3ad2ant2 1083	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → 𝑁 ∈ ℝ)
32	31	adantr 481	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ)
33	28	zred 11482	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℝ)
34	33	adantr 481	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℝ)
35		elfzle2 12345	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ≤ 𝑁)
36	35	adantl 482	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ≤ 𝑁)
37	30, 15	anim12i 590	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ))
38	37	3adant1 1079	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ))
39	38	ancomd 467	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ))
40		max2 12018	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑁 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼))
41	39, 40	syl 17	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → 𝑁 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼))
42	41	adantr 481	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑁 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼))
43	14, 32, 34, 36, 42	letrd 10194	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼))
44		eluz2 11693	. . . . . . . 8 ⊢ (if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ (ℤ≥‘𝑘) ↔ (𝑘 ∈ ℤ ∧ if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ ∧ 𝑘 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))
45	7, 29, 43, 44	syl3anbrc 1246	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ (ℤ≥‘𝑘))
46		elfzuzb 12336	. . . . . . 7 ⊢ (𝑘 ∈ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) ↔ (𝑘 ∈ (ℤ≥‘if(𝐼 ≤ 𝑀, 𝐼, 𝑀)) ∧ if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ (ℤ≥‘𝑘)))
47	26, 45, 46	sylanbrc 698	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))
48	47	ex 450	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))))
49	48	ssrdv 3609	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑀...𝑁) ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))
50	49	adantl 482	. . 3 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝑀...𝑁) ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))
51	1, 50	sstrd 3613	. 2 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → 𝑆 ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))
52	4	adantl 482	. . . . 5 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ∈ ℤ)
53	28	adantl 482	. . . . 5 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ)
54	2	adantl 482	. . . . 5 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → 𝐼 ∈ ℤ)
55	52, 53, 54	3jca 1242	. . . 4 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ∈ ℤ ∧ if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ ∧ 𝐼 ∈ ℤ))
56	16	3adant2 1080	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑀 ∈ ℝ ∧ 𝐼 ∈ ℝ))
57	56	adantl 482	. . . . . . 7 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝑀 ∈ ℝ ∧ 𝐼 ∈ ℝ))
58	57	ancomd 467	. . . . . 6 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ))
59		min1 12020	. . . . . 6 ⊢ ((𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ≤ 𝐼)
60	58, 59	syl 17	. . . . 5 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ≤ 𝐼)
61	38	adantl 482	. . . . . . 7 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ))
62	61	ancomd 467	. . . . . 6 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ))
63		max1 12016	. . . . . 6 ⊢ ((𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝐼 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼))
64	62, 63	syl 17	. . . . 5 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → 𝐼 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼))
65	60, 64	jca 554	. . . 4 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ≤ 𝐼 ∧ 𝐼 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))
66		elfz2 12333	. . . 4 ⊢ (𝐼 ∈ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) ↔ ((if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ∈ ℤ ∧ if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ≤ 𝐼 ∧ 𝐼 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼))))
67	55, 65, 66	sylanbrc 698	. . 3 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → 𝐼 ∈ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))
68	67	snssd 4340	. 2 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → {𝐼} ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))
69	51, 68	unssd 3789	1 ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝑆 ∪ {𝐼}) ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037   ∈ wcel 1990   ∪ cun 3572   ⊆ wss 3574  ifcif 4086  {csn 4177   class class class wbr 4653  ‘cfv 5888  (class class class)co 6650  ℝcr 9935   ≤ cle 10075  ℤcz 11377  ℤ_≥cuz 11687  ...cfz 12326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-pre-lttri 10010  ax-pre-lttrn 10011

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-neg 10269  df-z 11378  df-uz 11688  df-fz 12327

This theorem is referenced by:  ssfzunsn  12387  setsstruct2  15896