Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fissuni Structured version   Unicode version

Theorem fissuni 7411
 Description: A finite subset of a union is covered by finitely many elements. (Contributed by Stefan O'Rear, 2-Apr-2015.)
Assertion
Ref Expression
fissuni
Distinct variable groups:   ,   ,

Proof of Theorem fissuni
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 448 . . 3
2 dfss3 3338 . . . . . 6
3 eluni2 4019 . . . . . . 7
43ralbii 2729 . . . . . 6
52, 4bitri 241 . . . . 5
65biimpi 187 . . . 4
8 eleq2 2497 . . . 4
98ac6sfi 7351 . . 3
101, 7, 9syl2anc 643 . 2
11 imassrn 5216 . . . . . . 7
12 frn 5597 . . . . . . 7
1311, 12syl5ss 3359 . . . . . 6
14 vex 2959 . . . . . . . 8
15 imaexg 5217 . . . . . . . 8
1614, 15ax-mp 8 . . . . . . 7
1716elpw 3805 . . . . . 6
1813, 17sylibr 204 . . . . 5
1918ad2antrl 709 . . . 4
20 ffun 5593 . . . . . 6
2120ad2antrl 709 . . . . 5
22 simplr 732 . . . . 5
23 imafi 7399 . . . . 5
2421, 22, 23syl2anc 643 . . . 4
25 elin 3530 . . . 4
2619, 24, 25sylanbrc 646 . . 3
27 ffn 5591 . . . . . . . . . . 11
2827adantr 452 . . . . . . . . . 10
29 ssid 3367 . . . . . . . . . . 11
3029a1i 11 . . . . . . . . . 10
31 simpr 448 . . . . . . . . . 10
32 fnfvima 5976 . . . . . . . . . 10
3328, 30, 31, 32syl3anc 1184 . . . . . . . . 9
34 elssuni 4043 . . . . . . . . 9
3533, 34syl 16 . . . . . . . 8
3635sseld 3347 . . . . . . 7
3736ralimdva 2784 . . . . . 6
3837imp 419 . . . . 5
39 dfss3 3338 . . . . 5
4038, 39sylibr 204 . . . 4