Description: The union of two finite sets is finite. Part of Corollary 6K of Enderton p. 144. (Contributed by NM, 16-Nov-2002) Avoid ax-pow . (Revised by BTernaryTau, 7-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | unfi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uneq2 | |
|
2 | 1 | eleq1d | |
3 | 2 | imbi2d | |
4 | uneq2 | |
|
5 | 4 | eleq1d | |
6 | 5 | imbi2d | |
7 | uneq2 | |
|
8 | 7 | eleq1d | |
9 | 8 | imbi2d | |
10 | uneq2 | |
|
11 | 10 | eleq1d | |
12 | 11 | imbi2d | |
13 | un0 | |
|
14 | 13 | eleq1i | |
15 | 14 | biimpri | |
16 | snssi | |
|
17 | ssequn2 | |
|
18 | 17 | biimpi | |
19 | 18 | uneq2d | |
20 | un12 | |
|
21 | uncom | |
|
22 | 19 20 21 | 3eqtr4g | |
23 | 16 22 | syl | |
24 | 23 | eleq1d | |
25 | 24 | biimprd | |
26 | 25 | adantld | |
27 | isfi | |
|
28 | 27 | biimpi | |
29 | r19.41v | |
|
30 | disjsn | |
|
31 | elun | |
|
32 | 31 | notbii | |
33 | pm4.56 | |
|
34 | 32 33 | bitr4i | |
35 | 30 34 | sylbbr | |
36 | nnord | |
|
37 | orddisj | |
|
38 | 36 37 | syl | |
39 | en2sn | |
|
40 | 39 | el2v | |
41 | unen | |
|
42 | 40 41 | mpanl2 | |
43 | 38 42 | sylanr2 | |
44 | 35 43 | sylanr1 | |
45 | 44 | 3impb | |
46 | 45 | 3comr | |
47 | 46 | 3expb | |
48 | unass | |
|
49 | df-suc | |
|
50 | peano2 | |
|
51 | 49 50 | eqeltrrid | |
52 | breq2 | |
|
53 | 52 | rspcev | |
54 | 51 53 | sylan | |
55 | isfi | |
|
56 | 54 55 | sylibr | |
57 | 48 56 | eqeltrrid | |
58 | 47 57 | syldan | |
59 | 58 | rexlimiva | |
60 | 29 59 | sylbir | |
61 | 28 60 | sylan | |
62 | 61 | ancoms | |
63 | 62 | expl | |
64 | 26 63 | pm2.61i | |
65 | 64 | ex | |
66 | 65 | imim2d | |
67 | 66 | adantl | |
68 | 3 6 9 12 15 67 | findcard2s | |
69 | 68 | impcom | |