Metamath Proof Explorer


Theorem fiun

Description: The union of a chain (with respect to inclusion) of functions is a function. Analogous to f1iun . (Contributed by AV, 6-Oct-2023)

Ref Expression
Hypotheses fiun.1 x = y B = C
fiun.2 B V
Assertion fiun x A B : D S y A B C C B x A B : x A D S

Proof

Step Hyp Ref Expression
1 fiun.1 x = y B = C
2 fiun.2 B V
3 vex u V
4 eqeq1 z = u z = B u = B
5 4 rexbidv z = u x A z = B x A u = B
6 3 5 elab u z | x A z = B x A u = B
7 r19.29 x A B : D S y A B C C B x A u = B x A B : D S y A B C C B u = B
8 nfv x Fun u
9 nfre1 x x A z = B
10 9 nfab _ x z | x A z = B
11 nfv x u v v u
12 10 11 nfralw x v z | x A z = B u v v u
13 8 12 nfan x Fun u v z | x A z = B u v v u
14 ffun B : D S Fun B
15 funeq u = B Fun u Fun B
16 bianir Fun B Fun u Fun B Fun u
17 14 15 16 syl2an B : D S u = B Fun u
18 17 adantlr B : D S y A B C C B u = B Fun u
19 1 fiunlem B : D S y A B C C B u = B v z | x A z = B u v v u
20 18 19 jca B : D S y A B C C B u = B Fun u v z | x A z = B u v v u
21 20 a1i x A B : D S y A B C C B u = B Fun u v z | x A z = B u v v u
22 13 21 rexlimi x A B : D S y A B C C B u = B Fun u v z | x A z = B u v v u
23 7 22 syl x A B : D S y A B C C B x A u = B Fun u v z | x A z = B u v v u
24 6 23 sylan2b x A B : D S y A B C C B u z | x A z = B Fun u v z | x A z = B u v v u
25 24 ralrimiva x A B : D S y A B C C B u z | x A z = B Fun u v z | x A z = B u v v u
26 fununi u z | x A z = B Fun u v z | x A z = B u v v u Fun z | x A z = B
27 25 26 syl x A B : D S y A B C C B Fun z | x A z = B
28 2 dfiun2 x A B = z | x A z = B
29 28 funeqi Fun x A B Fun z | x A z = B
30 27 29 sylibr x A B : D S y A B C C B Fun x A B
31 3 eldm2 u dom B v u v B
32 fdm B : D S dom B = D
33 32 eleq2d B : D S u dom B u D
34 31 33 bitr3id B : D S v u v B u D
35 34 adantr B : D S y A B C C B v u v B u D
36 35 ralrexbid x A B : D S y A B C C B x A v u v B x A u D
37 eliun u v x A B x A u v B
38 37 exbii v u v x A B v x A u v B
39 3 eldm2 u dom x A B v u v x A B
40 rexcom4 x A v u v B v x A u v B
41 38 39 40 3bitr4i u dom x A B x A v u v B
42 eliun u x A D x A u D
43 36 41 42 3bitr4g x A B : D S y A B C C B u dom x A B u x A D
44 43 eqrdv x A B : D S y A B C C B dom x A B = x A D
45 df-fn x A B Fn x A D Fun x A B dom x A B = x A D
46 30 44 45 sylanbrc x A B : D S y A B C C B x A B Fn x A D
47 rniun ran x A B = x A ran B
48 frn B : D S ran B S
49 48 adantr B : D S y A B C C B ran B S
50 49 ralimi x A B : D S y A B C C B x A ran B S
51 iunss x A ran B S x A ran B S
52 50 51 sylibr x A B : D S y A B C C B x A ran B S
53 47 52 eqsstrid x A B : D S y A B C C B ran x A B S
54 df-f x A B : x A D S x A B Fn x A D ran x A B S
55 46 53 54 sylanbrc x A B : D S y A B C C B x A B : x A D S