This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
fiun.2 ⊢ 𝐵 ∈ V
Assertion fiun ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 : ∪ 𝑥 ∈ 𝐴 𝐷 ⟶ 𝑆 )

Proof

Step Hyp Ref Expression
1 fiun.1 ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
2 fiun.2 ⊢ 𝐵 ∈ V
3 vex ⊢ 𝑢 ∈ V
4 eqeq1 ⊢ ( 𝑧 = 𝑢 → ( 𝑧 = 𝐵 ↔ 𝑢 = 𝐵 ) )
5 4 rexbidv ⊢ ( 𝑧 = 𝑢 → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑢 = 𝐵 ) )
6 3 5 elab ⊢ ( 𝑢 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑢 = 𝐵 )
7 r19.29 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐴 𝑢 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) )
8 nfv ⊢ Ⅎ 𝑥 Fun 𝑢
9 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵
10 9 nfab ⊢ Ⅎ 𝑥 { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 }
11 nfv ⊢ Ⅎ 𝑥 ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 )
12 10 11 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 )
13 8 12 nfan ⊢ Ⅎ 𝑥 ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) )
14 ffun ⊢ ( 𝐵 : 𝐷 ⟶ 𝑆 → Fun 𝐵 )
15 funeq ⊢ ( 𝑢 = 𝐵 → ( Fun 𝑢 ↔ Fun 𝐵 ) )
16 bianir ⊢ ( ( Fun 𝐵 ∧ ( Fun 𝑢 ↔ Fun 𝐵 ) ) → Fun 𝑢 )
17 14 15 16 syl2an ⊢ ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ 𝑢 = 𝐵 ) → Fun 𝑢 )
18 17 adantlr ⊢ ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → Fun 𝑢 )
19 1 fiunlem ⊢ ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) )
20 18 19 jca ⊢ ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
21 20 a1i ⊢ ( 𝑥 ∈ 𝐴 → ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) )
22 13 21 rexlimi ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
23 7 22 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐴 𝑢 = 𝐵 ) → ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
24 6 23 sylan2b ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ) → ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
25 24 ralrimiva ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∀ 𝑢 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
26 fununi ⊢ ( ∀ 𝑢 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( Fun 𝑢 ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) → Fun ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } )
27 25 26 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → Fun ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } )
28 2 dfiun2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 }
29 28 funeqi ⊢ ( Fun ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } )
30 27 29 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → Fun ∪ 𝑥 ∈ 𝐴 𝐵 )
31 3 eldm2 ⊢ ( 𝑢 ∈ dom 𝐵 ↔ ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
32 fdm ⊢ ( 𝐵 : 𝐷 ⟶ 𝑆 → dom 𝐵 = 𝐷 )
33 32 eleq2d ⊢ ( 𝐵 : 𝐷 ⟶ 𝑆 → ( 𝑢 ∈ dom 𝐵 ↔ 𝑢 ∈ 𝐷 ) )
34 31 33 bitr3id ⊢ ( 𝐵 : 𝐷 ⟶ 𝑆 → ( ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷 ) )
35 34 adantr ⊢ ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ( ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷 ) )
36 35 ralrexbid ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑢 ∈ 𝐷 ) )
37 eliun ⊢ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
38 37 exbii ⊢ ( ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑣 ∃ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
39 3 eldm2 ⊢ ( 𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
40 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ↔ ∃ 𝑣 ∃ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
41 38 39 40 3bitr4i ⊢ ( 𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
42 eliun ⊢ ( 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷 ↔ ∃ 𝑥 ∈ 𝐴 𝑢 ∈ 𝐷 )
43 36 41 42 3bitr4g ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ( 𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷 ) )
44 43 eqrdv ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷 )
45 df-fn ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ↔ ( Fun ∪ 𝑥 ∈ 𝐴 𝐵 ∧ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷 ) )
46 30 44 45 sylanbrc ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 )
47 rniun ⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵
48 frn ⊢ ( 𝐵 : 𝐷 ⟶ 𝑆 → ran 𝐵 ⊆ 𝑆 )
49 48 adantr ⊢ ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ran 𝐵 ⊆ 𝑆 )
50 49 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 )
51 iunss ⊢ ( ∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 ↔ ∀ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 )
52 50 51 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 )
53 47 52 eqsstrid ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆 )
54 df-f ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 : ∪ 𝑥 ∈ 𝐴 𝐷 ⟶ 𝑆 ↔ ( ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ∧ ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆 ) )
55 46 53 54 sylanbrc ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 : ∪ 𝑥 ∈ 𝐴 𝐷 ⟶ 𝑆 )