Metamath Proof Explorer


Theorem resunimafz0

Description: TODO-AV: Revise using F e. Word dom I ? Formerly part of proof of eupth2lem3 : The union of a restriction by an image over an open range of nonnegative integers and a singleton of an ordered pair is a restriction by an image over an interval of nonnegative integers. (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 20-Feb-2021)

Ref Expression
Hypotheses resunimafz0.i φ Fun I
resunimafz0.f φ F : 0 ..^ F dom I
resunimafz0.n φ N 0 ..^ F
Assertion resunimafz0 φ I F 0 N = I F 0 ..^ N F N I F N

Proof

Step Hyp Ref Expression
1 resunimafz0.i φ Fun I
2 resunimafz0.f φ F : 0 ..^ F dom I
3 resunimafz0.n φ N 0 ..^ F
4 imaundi F 0 ..^ N N = F 0 ..^ N F N
5 elfzonn0 N 0 ..^ F N 0
6 3 5 syl φ N 0
7 elnn0uz N 0 N 0
8 6 7 sylib φ N 0
9 fzisfzounsn N 0 0 N = 0 ..^ N N
10 8 9 syl φ 0 N = 0 ..^ N N
11 10 imaeq2d φ F 0 N = F 0 ..^ N N
12 2 ffnd φ F Fn 0 ..^ F
13 fnsnfv F Fn 0 ..^ F N 0 ..^ F F N = F N
14 12 3 13 syl2anc φ F N = F N
15 14 uneq2d φ F 0 ..^ N F N = F 0 ..^ N F N
16 4 11 15 3eqtr4a φ F 0 N = F 0 ..^ N F N
17 16 reseq2d φ I F 0 N = I F 0 ..^ N F N
18 resundi I F 0 ..^ N F N = I F 0 ..^ N I F N
19 17 18 syl6eq φ I F 0 N = I F 0 ..^ N I F N
20 1 funfnd φ I Fn dom I
21 2 3 ffvelrnd φ F N dom I
22 fnressn I Fn dom I F N dom I I F N = F N I F N
23 20 21 22 syl2anc φ I F N = F N I F N
24 23 uneq2d φ I F 0 ..^ N I F N = I F 0 ..^ N F N I F N
25 19 24 eqtrd φ I F 0 N = I F 0 ..^ N F N I F N