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 )