Metamath Proof Explorer

Theorem founiiun0

Description: Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion founiiun0 
|- ( F : A -onto-> ( B u. { (/) } ) -> U. B = U_ x e. A ( F ` x ) )

Proof

Step Hyp Ref Expression
1 uniiun 
 |-  U. B = U_ y e. B y
2 elun1 
 |-  ( y e. B -> y e. ( B u. { (/) } ) )
3 foelrni 
 |-  ( ( F : A -onto-> ( B u. { (/) } ) /\ y e. ( B u. { (/) } ) ) -> E. x e. A ( F ` x ) = y )
4 2 3 sylan2 
 |-  ( ( F : A -onto-> ( B u. { (/) } ) /\ y e. B ) -> E. x e. A ( F ` x ) = y )
5 eqimss2 
 |-  ( ( F ` x ) = y -> y C_ ( F ` x ) )
6 5 reximi 
 |-  ( E. x e. A ( F ` x ) = y -> E. x e. A y C_ ( F ` x ) )
7 4 6 syl 
 |-  ( ( F : A -onto-> ( B u. { (/) } ) /\ y e. B ) -> E. x e. A y C_ ( F ` x ) )
8 7 ralrimiva 
 |-  ( F : A -onto-> ( B u. { (/) } ) -> A. y e. B E. x e. A y C_ ( F ` x ) )
9 iunss2 
 |-  ( A. y e. B E. x e. A y C_ ( F ` x ) -> U_ y e. B y C_ U_ x e. A ( F ` x ) )
10 8 9 syl 
 |-  ( F : A -onto-> ( B u. { (/) } ) -> U_ y e. B y C_ U_ x e. A ( F ` x ) )
11 simpl 
 |-  ( ( F : A -onto-> ( B u. { (/) } ) /\ B = (/) ) -> F : A -onto-> ( B u. { (/) } ) )
12 uneq1 
 |-  ( B = (/) -> ( B u. { (/) } ) = ( (/) u. { (/) } ) )
13 0un 
 |-  ( (/) u. { (/) } ) = { (/) }
14 12 13 eqtrdi 
 |-  ( B = (/) -> ( B u. { (/) } ) = { (/) } )
15 14 adantl 
 |-  ( ( F : A -onto-> ( B u. { (/) } ) /\ B = (/) ) -> ( B u. { (/) } ) = { (/) } )
16 foeq3 
 |-  ( ( B u. { (/) } ) = { (/) } -> ( F : A -onto-> ( B u. { (/) } ) <-> F : A -onto-> { (/) } ) )
17 15 16 syl 
 |-  ( ( F : A -onto-> ( B u. { (/) } ) /\ B = (/) ) -> ( F : A -onto-> ( B u. { (/) } ) <-> F : A -onto-> { (/) } ) )
18 11 17 mpbid 
 |-  ( ( F : A -onto-> ( B u. { (/) } ) /\ B = (/) ) -> F : A -onto-> { (/) } )
19 founiiun 
 |-  ( F : A -onto-> { (/) } -> U. { (/) } = U_ x e. A ( F ` x ) )
20 unisn0 
 |-  U. { (/) } = (/)
21 19 20 eqtr3di 
 |-  ( F : A -onto-> { (/) } -> U_ x e. A ( F ` x ) = (/) )
22 0ss 
 |-  (/) C_ U_ y e. B y
23 21 22 eqsstrdi 
 |-  ( F : A -onto-> { (/) } -> U_ x e. A ( F ` x ) C_ U_ y e. B y )
24 18 23 syl 
 |-  ( ( F : A -onto-> ( B u. { (/) } ) /\ B = (/) ) -> U_ x e. A ( F ` x ) C_ U_ y e. B y )
25 ssid 
 |-  ( F ` x ) C_ ( F ` x )
26 sseq2 
 |-  ( y = ( F ` x ) -> ( ( F ` x ) C_ y <-> ( F ` x ) C_ ( F ` x ) ) )
27 26 rspcev 
 |-  ( ( ( F ` x ) e. B /\ ( F ` x ) C_ ( F ` x ) ) -> E. y e. B ( F ` x ) C_ y )
28 25 27 mpan2 
 |-  ( ( F ` x ) e. B -> E. y e. B ( F ` x ) C_ y )
29 28 adantl 
 |-  ( ( ( ( F : A -onto-> ( B u. { (/) } ) /\ -. B = (/) ) /\ x e. A ) /\ ( F ` x ) e. B ) -> E. y e. B ( F ` x ) C_ y )
30 fof 
 |-  ( F : A -onto-> ( B u. { (/) } ) -> F : A --> ( B u. { (/) } ) )
31 30 ffvelrnda 
 |-  ( ( F : A -onto-> ( B u. { (/) } ) /\ x e. A ) -> ( F ` x ) e. ( B u. { (/) } ) )
32 elunnel1 
 |-  ( ( ( F ` x ) e. ( B u. { (/) } ) /\ -. ( F ` x ) e. B ) -> ( F ` x ) e. { (/) } )
33 31 32 sylan 
 |-  ( ( ( F : A -onto-> ( B u. { (/) } ) /\ x e. A ) /\ -. ( F ` x ) e. B ) -> ( F ` x ) e. { (/) } )
34 elsni 
 |-  ( ( F ` x ) e. { (/) } -> ( F ` x ) = (/) )
35 33 34 syl 
 |-  ( ( ( F : A -onto-> ( B u. { (/) } ) /\ x e. A ) /\ -. ( F ` x ) e. B ) -> ( F ` x ) = (/) )
36 35 adantllr 
 |-  ( ( ( ( F : A -onto-> ( B u. { (/) } ) /\ -. B = (/) ) /\ x e. A ) /\ -. ( F ` x ) e. B ) -> ( F ` x ) = (/) )
37 neq0 
 |-  ( -. B = (/) <-> E. y y e. B )
38 37 biimpi 
 |-  ( -. B = (/) -> E. y y e. B )
39 38 adantr 
 |-  ( ( -. B = (/) /\ ( F ` x ) = (/) ) -> E. y y e. B )
40 id 
 |-  ( ( F ` x ) = (/) -> ( F ` x ) = (/) )
41 0ss 
 |-  (/) C_ y
42 40 41 eqsstrdi 
 |-  ( ( F ` x ) = (/) -> ( F ` x ) C_ y )
43 42 anim1ci 
 |-  ( ( ( F ` x ) = (/) /\ y e. B ) -> ( y e. B /\ ( F ` x ) C_ y ) )
44 43 ex 
 |-  ( ( F ` x ) = (/) -> ( y e. B -> ( y e. B /\ ( F ` x ) C_ y ) ) )
45 44 adantl 
 |-  ( ( -. B = (/) /\ ( F ` x ) = (/) ) -> ( y e. B -> ( y e. B /\ ( F ` x ) C_ y ) ) )
46 45 eximdv 
 |-  ( ( -. B = (/) /\ ( F ` x ) = (/) ) -> ( E. y y e. B -> E. y ( y e. B /\ ( F ` x ) C_ y ) ) )
47 39 46 mpd 
 |-  ( ( -. B = (/) /\ ( F ` x ) = (/) ) -> E. y ( y e. B /\ ( F ` x ) C_ y ) )
48 df-rex 
 |-  ( E. y e. B ( F ` x ) C_ y <-> E. y ( y e. B /\ ( F ` x ) C_ y ) )
49 47 48 sylibr 
 |-  ( ( -. B = (/) /\ ( F ` x ) = (/) ) -> E. y e. B ( F ` x ) C_ y )
50 49 ad4ant24 
 |-  ( ( ( ( F : A -onto-> ( B u. { (/) } ) /\ -. B = (/) ) /\ x e. A ) /\ ( F ` x ) = (/) ) -> E. y e. B ( F ` x ) C_ y )
51 36 50 syldan 
 |-  ( ( ( ( F : A -onto-> ( B u. { (/) } ) /\ -. B = (/) ) /\ x e. A ) /\ -. ( F ` x ) e. B ) -> E. y e. B ( F ` x ) C_ y )
52 29 51 pm2.61dan 
 |-  ( ( ( F : A -onto-> ( B u. { (/) } ) /\ -. B = (/) ) /\ x e. A ) -> E. y e. B ( F ` x ) C_ y )
53 52 ralrimiva 
 |-  ( ( F : A -onto-> ( B u. { (/) } ) /\ -. B = (/) ) -> A. x e. A E. y e. B ( F ` x ) C_ y )
54 iunss2 
 |-  ( A. x e. A E. y e. B ( F ` x ) C_ y -> U_ x e. A ( F ` x ) C_ U_ y e. B y )
55 53 54 syl 
 |-  ( ( F : A -onto-> ( B u. { (/) } ) /\ -. B = (/) ) -> U_ x e. A ( F ` x ) C_ U_ y e. B y )
56 24 55 pm2.61dan 
 |-  ( F : A -onto-> ( B u. { (/) } ) -> U_ x e. A ( F ` x ) C_ U_ y e. B y )
57 10 56 eqssd 
 |-  ( F : A -onto-> ( B u. { (/) } ) -> U_ y e. B y = U_ x e. A ( F ` x ) )
58 1 57 syl5eq 
 |-  ( F : A -onto-> ( B u. { (/) } ) -> U. B = U_ x e. A ( F ` x ) )