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

Theorem fissuni 7837
 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 461 . . 3
2 dfss3 3499 . . . . 5
3 eluni2 4255 . . . . . 6
43ralbii 2898 . . . . 5
52, 4sylbb 197 . . . 4
7 eleq2 2540 . . . 4
87ac6sfi 7776 . . 3
91, 6, 8syl2anc 661 . 2
10 imassrn 5354 . . . . . . 7
11 frn 5743 . . . . . . 7
1210, 11syl5ss 3520 . . . . . 6
13 vex 3121 . . . . . . . 8
14 imaexg 6732 . . . . . . . 8
1513, 14ax-mp 5 . . . . . . 7
1615elpw 4022 . . . . . 6
1712, 16sylibr 212 . . . . 5
1817ad2antrl 727 . . . 4
19 ffun 5739 . . . . . 6
2019ad2antrl 727 . . . . 5
21 simplr 754 . . . . 5
22 imafi 7825 . . . . 5
2320, 21, 22syl2anc 661 . . . 4
2418, 23elind 3693 . . 3
25 ffn 5737 . . . . . . . . . . 11
2625adantr 465 . . . . . . . . . 10
27 ssid 3528 . . . . . . . . . . 11
2827a1i 11 . . . . . . . . . 10
29 simpr 461 . . . . . . . . . 10
30 fnfvima 6149 . . . . . . . . . 10
3126, 28, 29, 30syl3anc 1228 . . . . . . . . 9
32 elssuni 4281 . . . . . . . . 9
3331, 32syl 16 . . . . . . . 8
3433sseld 3508 . . . . . . 7
3534ralimdva 2875 . . . . . 6
3635imp 429 . . . . 5
37 dfss3 3499 . . . . 5
3836, 37sylibr 212 . . . 4