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