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 A B : D 1-1 S y A B C C B x A B : x A D 1-1 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 1-1 S y A B C C B x A u = B x A B : D 1-1 S y A B C C B u = B
8 nfv x Fun u Fun u -1
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 Fun u -1 v z | x A z = B u v v u
14 f1eq1 u = B u : D 1-1 S B : D 1-1 S
15 14 biimparc B : D 1-1 S u = B u : D 1-1 S
16 df-f1 u : D 1-1 S 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-1 S Fun u Fun u -1
20 15 19 syl B : D 1-1 S u = B Fun u Fun u -1
21 20 adantlr B : D 1-1 S y A B C C B u = B Fun u Fun u -1
22 f1f B : D 1-1 S B : D S
23 1 fiunlem B : D S y A B C C B u = B v z | x A z = B u v v u
24 22 23 sylanl1 B : D 1-1 S y A B C C B u = B v z | x A z = B u v v u
25 21 24 jca B : D 1-1 S y A B C C B u = B Fun u Fun u -1 v z | x A z = B u v v u
26 25 a1i x A B : D 1-1 S y A B C C B u = B Fun u Fun u -1 v z | x A z = B u v v u
27 13 26 rexlimi x A B : D 1-1 S y A B C C B u = B Fun u Fun u -1 v z | x A z = B u v v u
28 7 27 syl x A B : D 1-1 S y A B C C B x A u = B Fun u Fun u -1 v z | x A z = B u v v u
29 6 28 sylan2b x A B : D 1-1 S y A B C C B u z | x A z = B Fun u Fun u -1 v z | x A z = B u v v u
30 29 ralrimiva x A B : D 1-1 S y A B C C B u z | x A z = B Fun u Fun u -1 v z | x A z = B u v v u
31 fun11uni u z | x A z = B Fun u Fun u -1 v z | x A z = B u v v u Fun z | x A z = B Fun z | x A z = B -1
32 30 31 syl x A B : D 1-1 S y A B C C B Fun z | x A z = B Fun z | x A z = B -1
33 32 simpld x A B : D 1-1 S y A B C C B Fun z | x A z = B
34 2 dfiun2 x A B = z | x A z = B
35 34 funeqi Fun x A B Fun z | x A z = B
36 33 35 sylibr x A B : D 1-1 S y A B C C B Fun x A B
37 3 eldm2 u dom B v u v B
38 f1dm B : D 1-1 S dom B = D
39 38 eleq2d B : D 1-1 S u dom B u D
40 37 39 bitr3id B : D 1-1 S v u v B u D
41 40 adantr B : D 1-1 S y A B C C B v u v B u D
42 41 ralrexbid x A B : D 1-1 S y A B C C B x A v u v B x A u D
43 eliun u v x A B x A u v B
44 43 exbii v u v x A B v x A u v B
45 3 eldm2 u dom x A B v u v x A B
46 rexcom4 x A v u v B v x A u v B
47 44 45 46 3bitr4i u dom x A B x A v u v B
48 eliun u x A D x A u D
49 42 47 48 3bitr4g x A B : D 1-1 S y A B C C B u dom x A B u x A D
50 49 eqrdv x A B : D 1-1 S y A B C C B dom x A B = x A D
51 df-fn x A B Fn x A D Fun x A B dom x A B = x A D
52 36 50 51 sylanbrc x A B : D 1-1 S y A B C C B x A B Fn x A D
53 rniun ran x A B = x A ran B
54 22 frnd B : D 1-1 S ran B S
55 54 adantr B : D 1-1 S y A B C C B ran B S
56 55 ralimi x A B : D 1-1 S y A B C C B x A ran B S
57 iunss x A ran B S x A ran B S
58 56 57 sylibr x A B : D 1-1 S y A B C C B x A ran B S
59 53 58 eqsstrid x A B : D 1-1 S y A B C C B ran x A B S
60 df-f x A B : x A D S x A B Fn x A D ran x A B S
61 52 59 60 sylanbrc x A B : D 1-1 S y A B C C B x A B : x A D S
62 32 simprd x A B : D 1-1 S y A B C C B Fun z | x A z = B -1
63 34 cnveqi x A B -1 = z | x A z = B -1
64 63 funeqi Fun x A B -1 Fun z | x A z = B -1
65 62 64 sylibr x A B : D 1-1 S y A B C C B Fun x A B -1
66 df-f1 x A B : x A D 1-1 S x A B : x A D S Fun x A B -1
67 61 65 66 sylanbrc x A B : D 1-1 S y A B C C B x A B : x A D 1-1 S