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∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B→⋃x∈AB:⋃x∈AD⟶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∈Az=B↔∃x∈Au=B
6 3 5 elab ⊢u∈z|∃x∈Az=B↔∃x∈Au=B
7 r19.29 ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B∧∃x∈Au=B→∃x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B∧u=B
8 nfv ⊢ℲxFun⁡u
9 nfre1 ⊢Ⅎx∃x∈Az=B
10 9 nfab ⊢Ⅎ_xz|∃x∈Az=B
11 nfv ⊢Ⅎxu⊆v∨v⊆u
12 10 11 nfralw ⊢Ⅎx∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
13 8 12 nfan ⊢ℲxFun⁡u∧∀v∈z|∃x∈Az=Bu⊆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∈AB⊆C∨C⊆B∧u=B→Fun⁡u
19 1 fiunlem ⊢B:D⟶S∧∀y∈AB⊆C∨C⊆B∧u=B→∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
20 18 19 jca ⊢B:D⟶S∧∀y∈AB⊆C∨C⊆B∧u=B→Fun⁡u∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
21 20 a1i ⊢x∈A→B:D⟶S∧∀y∈AB⊆C∨C⊆B∧u=B→Fun⁡u∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
22 13 21 rexlimi ⊢∃x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B∧u=B→Fun⁡u∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
23 7 22 syl ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B∧∃x∈Au=B→Fun⁡u∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
24 6 23 sylan2b ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B∧u∈z|∃x∈Az=B→Fun⁡u∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
25 24 ralrimiva ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B→∀u∈z|∃x∈Az=BFun⁡u∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
26 fununi ⊢∀u∈z|∃x∈Az=BFun⁡u∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u→Fun⁡⋃z|∃x∈Az=B
27 25 26 syl ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B→Fun⁡⋃z|∃x∈Az=B
28 2 dfiun2 ⊢⋃x∈AB=⋃z|∃x∈Az=B
29 28 funeqi ⊢Fun⁡⋃x∈AB↔Fun⁡⋃z|∃x∈Az=B
30 27 29 sylibr ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B→Fun⁡⋃x∈AB
31 3 eldm2 ⊢u∈dom⁡B↔∃vuv∈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→∃vuv∈B↔u∈D
35 34 adantr ⊢B:D⟶S∧∀y∈AB⊆C∨C⊆B→∃vuv∈B↔u∈D
36 35 ralrexbid ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B→∃x∈A∃vuv∈B↔∃x∈Au∈D
37 eliun ⊢uv∈⋃x∈AB↔∃x∈Auv∈B
38 37 exbii ⊢∃vuv∈⋃x∈AB↔∃v∃x∈Auv∈B
39 3 eldm2 ⊢u∈dom⁡⋃x∈AB↔∃vuv∈⋃x∈AB
40 rexcom4 ⊢∃x∈A∃vuv∈B↔∃v∃x∈Auv∈B
41 38 39 40 3bitr4i ⊢u∈dom⁡⋃x∈AB↔∃x∈A∃vuv∈B
42 eliun ⊢u∈⋃x∈AD↔∃x∈Au∈D
43 36 41 42 3bitr4g ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B→u∈dom⁡⋃x∈AB↔u∈⋃x∈AD
44 43 eqrdv ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B→dom⁡⋃x∈AB=⋃x∈AD
45 df-fn ⊢⋃x∈ABFn⋃x∈AD↔Fun⁡⋃x∈AB∧dom⁡⋃x∈AB=⋃x∈AD
46 30 44 45 sylanbrc ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B→⋃x∈ABFn⋃x∈AD
47 rniun ⊢ran⁡⋃x∈AB=⋃x∈Aran⁡B
48 frn ⊢B:D⟶S→ran⁡B⊆S
49 48 adantr ⊢B:D⟶S∧∀y∈AB⊆C∨C⊆B→ran⁡B⊆S
50 49 ralimi ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B→∀x∈Aran⁡B⊆S
51 iunss ⊢⋃x∈Aran⁡B⊆S↔∀x∈Aran⁡B⊆S
52 50 51 sylibr ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B→⋃x∈Aran⁡B⊆S
53 47 52 eqsstrid ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B→ran⁡⋃x∈AB⊆S
54 df-f ⊢⋃x∈AB:⋃x∈AD⟶S↔⋃x∈ABFn⋃x∈AD∧ran⁡⋃x∈AB⊆S
55 46 53 54 sylanbrc ⊢∀x∈AB:D⟶S∧∀y∈AB⊆C∨C⊆B→⋃x∈AB:⋃x∈AD⟶S