Metamath Proof Explorer

Theorem f1iun

Description: The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013) (Revised by Mario Carneiro, 24-Jun-2015) (Proof shortened by AV, 5-Nov-2023)

Ref Expression
Hypotheses fiun.1 ⊢x=y→B=C
fiun.2 ⊢B∈V
Assertion f1iun ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→⋃x∈AB:⋃x∈AD⟶1-1S

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⟶1-1S∧∀y∈AB⊆C∨C⊆B∧∃x∈Au=B→∃x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B∧u=B
8 nfv ⊢ℲxFun⁡u∧Fun⁡u-1
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∧Fun⁡u-1∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
14 f1eq1 ⊢u=B→u:D⟶1-1S↔B:D⟶1-1S
15 14 biimparc ⊢B:D⟶1-1S∧u=B→u:D⟶1-1S
16 df-f1 ⊢u:D⟶1-1S↔u:D⟶S∧Fun⁡u-1
17 ffun ⊢u:D⟶S→Fun⁡u
18 17 anim1i ⊢u:D⟶S∧Fun⁡u-1→Fun⁡u∧Fun⁡u-1
19 16 18 sylbi ⊢u:D⟶1-1S→Fun⁡u∧Fun⁡u-1
20 15 19 syl ⊢B:D⟶1-1S∧u=B→Fun⁡u∧Fun⁡u-1
21 20 adantlr ⊢B:D⟶1-1S∧∀y∈AB⊆C∨C⊆B∧u=B→Fun⁡u∧Fun⁡u-1
22 f1f ⊢B:D⟶1-1S→B:D⟶S
23 1 fiunlem ⊢B:D⟶S∧∀y∈AB⊆C∨C⊆B∧u=B→∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
24 22 23 sylanl1 ⊢B:D⟶1-1S∧∀y∈AB⊆C∨C⊆B∧u=B→∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
25 21 24 jca ⊢B:D⟶1-1S∧∀y∈AB⊆C∨C⊆B∧u=B→Fun⁡u∧Fun⁡u-1∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
26 25 a1i ⊢x∈A→B:D⟶1-1S∧∀y∈AB⊆C∨C⊆B∧u=B→Fun⁡u∧Fun⁡u-1∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
27 13 26 rexlimi ⊢∃x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B∧u=B→Fun⁡u∧Fun⁡u-1∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
28 7 27 syl ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B∧∃x∈Au=B→Fun⁡u∧Fun⁡u-1∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
29 6 28 sylan2b ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B∧u∈z|∃x∈Az=B→Fun⁡u∧Fun⁡u-1∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
30 29 ralrimiva ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→∀u∈z|∃x∈Az=BFun⁡u∧Fun⁡u-1∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u
31 fun11uni ⊢∀u∈z|∃x∈Az=BFun⁡u∧Fun⁡u-1∧∀v∈z|∃x∈Az=Bu⊆v∨v⊆u→Fun⁡⋃z|∃x∈Az=B∧Fun⁡⋃z|∃x∈Az=B-1
32 30 31 syl ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→Fun⁡⋃z|∃x∈Az=B∧Fun⁡⋃z|∃x∈Az=B-1
33 32 simpld ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→Fun⁡⋃z|∃x∈Az=B
34 2 dfiun2 ⊢⋃x∈AB=⋃z|∃x∈Az=B
35 34 funeqi ⊢Fun⁡⋃x∈AB↔Fun⁡⋃z|∃x∈Az=B
36 33 35 sylibr ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→Fun⁡⋃x∈AB
37 3 eldm2 ⊢u∈dom⁡B↔∃vuv∈B
38 f1dm ⊢B:D⟶1-1S→dom⁡B=D
39 38 eleq2d ⊢B:D⟶1-1S→u∈dom⁡B↔u∈D
40 37 39 bitr3id ⊢B:D⟶1-1S→∃vuv∈B↔u∈D
41 40 adantr ⊢B:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→∃vuv∈B↔u∈D
42 41 ralrexbid ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→∃x∈A∃vuv∈B↔∃x∈Au∈D
43 eliun ⊢uv∈⋃x∈AB↔∃x∈Auv∈B
44 43 exbii ⊢∃vuv∈⋃x∈AB↔∃v∃x∈Auv∈B
45 3 eldm2 ⊢u∈dom⁡⋃x∈AB↔∃vuv∈⋃x∈AB
46 rexcom4 ⊢∃x∈A∃vuv∈B↔∃v∃x∈Auv∈B
47 44 45 46 3bitr4i ⊢u∈dom⁡⋃x∈AB↔∃x∈A∃vuv∈B
48 eliun ⊢u∈⋃x∈AD↔∃x∈Au∈D
49 42 47 48 3bitr4g ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→u∈dom⁡⋃x∈AB↔u∈⋃x∈AD
50 49 eqrdv ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→dom⁡⋃x∈AB=⋃x∈AD
51 df-fn ⊢⋃x∈ABFn⋃x∈AD↔Fun⁡⋃x∈AB∧dom⁡⋃x∈AB=⋃x∈AD
52 36 50 51 sylanbrc ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→⋃x∈ABFn⋃x∈AD
53 rniun ⊢ran⁡⋃x∈AB=⋃x∈Aran⁡B
54 22 frnd ⊢B:D⟶1-1S→ran⁡B⊆S
55 54 adantr ⊢B:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→ran⁡B⊆S
56 55 ralimi ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→∀x∈Aran⁡B⊆S
57 iunss ⊢⋃x∈Aran⁡B⊆S↔∀x∈Aran⁡B⊆S
58 56 57 sylibr ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→⋃x∈Aran⁡B⊆S
59 53 58 eqsstrid ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→ran⁡⋃x∈AB⊆S
60 df-f ⊢⋃x∈AB:⋃x∈AD⟶S↔⋃x∈ABFn⋃x∈AD∧ran⁡⋃x∈AB⊆S
61 52 59 60 sylanbrc ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→⋃x∈AB:⋃x∈AD⟶S
62 32 simprd ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→Fun⁡⋃z|∃x∈Az=B-1
63 34 cnveqi ⊢⋃x∈AB-1=⋃z|∃x∈Az=B-1
64 63 funeqi ⊢Fun⁡⋃x∈AB-1↔Fun⁡⋃z|∃x∈Az=B-1
65 62 64 sylibr ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→Fun⁡⋃x∈AB-1
66 df-f1 ⊢⋃x∈AB:⋃x∈AD⟶1-1S↔⋃x∈AB:⋃x∈AD⟶S∧Fun⁡⋃x∈AB-1
67 61 65 66 sylanbrc ⊢∀x∈AB:D⟶1-1S∧∀y∈AB⊆C∨C⊆B→⋃x∈AB:⋃x∈AD⟶1-1S