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 e. _V
Assertion f1iun
|- ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> U_ x e. A B : U_ x e. A D -1-1-> S )

Proof

Step Hyp Ref Expression
1 fiun.1
 |-  ( x = y -> B = C )
2 fiun.2
 |-  B e. _V
3 vex
 |-  u e. _V
4 eqeq1
 |-  ( z = u -> ( z = B <-> u = B ) )
5 4 rexbidv
 |-  ( z = u -> ( E. x e. A z = B <-> E. x e. A u = B ) )
6 3 5 elab
 |-  ( u e. { z | E. x e. A z = B } <-> E. x e. A u = B )
7 r19.29
 |-  ( ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ E. x e. A u = B ) -> E. x e. A ( ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ u = B ) )
8 nfv
 |-  F/ x ( Fun u /\ Fun `' u )
9 nfre1
 |-  F/ x E. x e. A z = B
10 9 nfab
 |-  F/_ x { z | E. x e. A z = B }
11 nfv
 |-  F/ x ( u C_ v \/ v C_ u )
12 10 11 nfralw
 |-  F/ x A. v e. { z | E. x e. A z = B } ( u C_ v \/ v C_ u )
13 8 12 nfan
 |-  F/ x ( ( Fun u /\ Fun `' u ) /\ A. v e. { z | E. x e. A z = B } ( u C_ v \/ v C_ 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 ) )
17 ffun
 |-  ( u : D --> S -> Fun u )
18 17 anim1i
 |-  ( ( u : D --> S /\ Fun `' u ) -> ( Fun u /\ Fun `' u ) )
19 16 18 sylbi
 |-  ( u : D -1-1-> S -> ( Fun u /\ Fun `' u ) )
20 15 19 syl
 |-  ( ( B : D -1-1-> S /\ u = B ) -> ( Fun u /\ Fun `' u ) )
21 20 adantlr
 |-  ( ( ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ u = B ) -> ( Fun u /\ Fun `' u ) )
22 f1f
 |-  ( B : D -1-1-> S -> B : D --> S )
23 1 fiunlem
 |-  ( ( ( B : D --> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ u = B ) -> A. v e. { z | E. x e. A z = B } ( u C_ v \/ v C_ u ) )
24 22 23 sylanl1
 |-  ( ( ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ u = B ) -> A. v e. { z | E. x e. A z = B } ( u C_ v \/ v C_ u ) )
25 21 24 jca
 |-  ( ( ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ u = B ) -> ( ( Fun u /\ Fun `' u ) /\ A. v e. { z | E. x e. A z = B } ( u C_ v \/ v C_ u ) ) )
26 25 a1i
 |-  ( x e. A -> ( ( ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ u = B ) -> ( ( Fun u /\ Fun `' u ) /\ A. v e. { z | E. x e. A z = B } ( u C_ v \/ v C_ u ) ) ) )
27 13 26 rexlimi
 |-  ( E. x e. A ( ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ u = B ) -> ( ( Fun u /\ Fun `' u ) /\ A. v e. { z | E. x e. A z = B } ( u C_ v \/ v C_ u ) ) )
28 7 27 syl
 |-  ( ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ E. x e. A u = B ) -> ( ( Fun u /\ Fun `' u ) /\ A. v e. { z | E. x e. A z = B } ( u C_ v \/ v C_ u ) ) )
29 6 28 sylan2b
 |-  ( ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ u e. { z | E. x e. A z = B } ) -> ( ( Fun u /\ Fun `' u ) /\ A. v e. { z | E. x e. A z = B } ( u C_ v \/ v C_ u ) ) )
30 29 ralrimiva
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> A. u e. { z | E. x e. A z = B } ( ( Fun u /\ Fun `' u ) /\ A. v e. { z | E. x e. A z = B } ( u C_ v \/ v C_ u ) ) )
31 fun11uni
 |-  ( A. u e. { z | E. x e. A z = B } ( ( Fun u /\ Fun `' u ) /\ A. v e. { z | E. x e. A z = B } ( u C_ v \/ v C_ u ) ) -> ( Fun U. { z | E. x e. A z = B } /\ Fun `' U. { z | E. x e. A z = B } ) )
32 30 31 syl
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> ( Fun U. { z | E. x e. A z = B } /\ Fun `' U. { z | E. x e. A z = B } ) )
33 32 simpld
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> Fun U. { z | E. x e. A z = B } )
34 2 dfiun2
 |-  U_ x e. A B = U. { z | E. x e. A z = B }
35 34 funeqi
 |-  ( Fun U_ x e. A B <-> Fun U. { z | E. x e. A z = B } )
36 33 35 sylibr
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> Fun U_ x e. A B )
37 3 eldm2
 |-  ( u e. dom B <-> E. v <. u , v >. e. B )
38 f1dm
 |-  ( B : D -1-1-> S -> dom B = D )
39 38 eleq2d
 |-  ( B : D -1-1-> S -> ( u e. dom B <-> u e. D ) )
40 37 39 bitr3id
 |-  ( B : D -1-1-> S -> ( E. v <. u , v >. e. B <-> u e. D ) )
41 40 adantr
 |-  ( ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> ( E. v <. u , v >. e. B <-> u e. D ) )
42 41 ralrexbid
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> ( E. x e. A E. v <. u , v >. e. B <-> E. x e. A u e. D ) )
43 eliun
 |-  ( <. u , v >. e. U_ x e. A B <-> E. x e. A <. u , v >. e. B )
44 43 exbii
 |-  ( E. v <. u , v >. e. U_ x e. A B <-> E. v E. x e. A <. u , v >. e. B )
45 3 eldm2
 |-  ( u e. dom U_ x e. A B <-> E. v <. u , v >. e. U_ x e. A B )
46 rexcom4
 |-  ( E. x e. A E. v <. u , v >. e. B <-> E. v E. x e. A <. u , v >. e. B )
47 44 45 46 3bitr4i
 |-  ( u e. dom U_ x e. A B <-> E. x e. A E. v <. u , v >. e. B )
48 eliun
 |-  ( u e. U_ x e. A D <-> E. x e. A u e. D )
49 42 47 48 3bitr4g
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> ( u e. dom U_ x e. A B <-> u e. U_ x e. A D ) )
50 49 eqrdv
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> dom U_ x e. A B = U_ x e. A D )
51 df-fn
 |-  ( U_ x e. A B Fn U_ x e. A D <-> ( Fun U_ x e. A B /\ dom U_ x e. A B = U_ x e. A D ) )
52 36 50 51 sylanbrc
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> U_ x e. A B Fn U_ x e. A D )
53 rniun
 |-  ran U_ x e. A B = U_ x e. A ran B
54 22 frnd
 |-  ( B : D -1-1-> S -> ran B C_ S )
55 54 adantr
 |-  ( ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> ran B C_ S )
56 55 ralimi
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> A. x e. A ran B C_ S )
57 iunss
 |-  ( U_ x e. A ran B C_ S <-> A. x e. A ran B C_ S )
58 56 57 sylibr
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> U_ x e. A ran B C_ S )
59 53 58 eqsstrid
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> ran U_ x e. A B C_ S )
60 df-f
 |-  ( U_ x e. A B : U_ x e. A D --> S <-> ( U_ x e. A B Fn U_ x e. A D /\ ran U_ x e. A B C_ S ) )
61 52 59 60 sylanbrc
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> U_ x e. A B : U_ x e. A D --> S )
62 32 simprd
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> Fun `' U. { z | E. x e. A z = B } )
63 34 cnveqi
 |-  `' U_ x e. A B = `' U. { z | E. x e. A z = B }
64 63 funeqi
 |-  ( Fun `' U_ x e. A B <-> Fun `' U. { z | E. x e. A z = B } )
65 62 64 sylibr
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> Fun `' U_ x e. A B )
66 df-f1
 |-  ( U_ x e. A B : U_ x e. A D -1-1-> S <-> ( U_ x e. A B : U_ x e. A D --> S /\ Fun `' U_ x e. A B ) )
67 61 65 66 sylanbrc
 |-  ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> U_ x e. A B : U_ x e. A D -1-1-> S )