Metamath Proof Explorer


Theorem unfi

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 AFinBFinABFin

Proof

Step Hyp Ref Expression
1 uneq2 x=Ax=A
2 1 eleq1d x=AxFinAFin
3 2 imbi2d x=AFinAxFinAFinAFin
4 uneq2 x=yAx=Ay
5 4 eleq1d x=yAxFinAyFin
6 5 imbi2d x=yAFinAxFinAFinAyFin
7 uneq2 x=yzAx=Ayz
8 7 eleq1d x=yzAxFinAyzFin
9 8 imbi2d x=yzAFinAxFinAFinAyzFin
10 uneq2 x=BAx=AB
11 10 eleq1d x=BAxFinABFin
12 11 imbi2d x=BAFinAxFinAFinABFin
13 un0 A=A
14 13 eleq1i AFinAFin
15 14 biimpri AFinAFin
16 snssi zAzA
17 ssequn2 zAAz=A
18 17 biimpi zAAz=A
19 18 uneq2d zAyAz=yA
20 un12 Ayz=yAz
21 uncom Ay=yA
22 19 20 21 3eqtr4g zAAyz=Ay
23 16 22 syl zAAyz=Ay
24 23 eleq1d zAAyzFinAyFin
25 24 biimprd zAAyFinAyzFin
26 25 adantld zA¬zyAyFinAyzFin
27 isfi AyFinwωAyw
28 27 biimpi AyFinwωAyw
29 r19.41v wωAyw¬zA¬zywωAyw¬zA¬zy
30 disjsn Ayz=¬zAy
31 elun zAyzAzy
32 31 notbii ¬zAy¬zAzy
33 pm4.56 ¬zA¬zy¬zAzy
34 32 33 bitr4i ¬zAy¬zA¬zy
35 30 34 sylbbr ¬zA¬zyAyz=
36 nnord wωOrdw
37 orddisj Ordwww=
38 36 37 syl wωww=
39 en2sn zVwVzw
40 39 el2v zw
41 unen AywzwAyz=ww=Ayzww
42 40 41 mpanl2 AywAyz=ww=Ayzww
43 38 42 sylanr2 AywAyz=wωAyzww
44 35 43 sylanr1 Ayw¬zA¬zywωAyzww
45 44 3impb Ayw¬zA¬zywωAyzww
46 45 3comr wωAyw¬zA¬zyAyzww
47 46 3expb wωAyw¬zA¬zyAyzww
48 unass Ayz=Ayz
49 df-suc sucw=ww
50 peano2 wωsucwω
51 49 50 eqeltrrid wωwwω
52 breq2 v=wwAyzvAyzww
53 52 rspcev wwωAyzwwvωAyzv
54 51 53 sylan wωAyzwwvωAyzv
55 isfi AyzFinvωAyzv
56 54 55 sylibr wωAyzwwAyzFin
57 48 56 eqeltrrid wωAyzwwAyzFin
58 47 57 syldan wωAyw¬zA¬zyAyzFin
59 58 rexlimiva wωAyw¬zA¬zyAyzFin
60 29 59 sylbir wωAyw¬zA¬zyAyzFin
61 28 60 sylan AyFin¬zA¬zyAyzFin
62 61 ancoms ¬zA¬zyAyFinAyzFin
63 62 expl ¬zA¬zyAyFinAyzFin
64 26 63 pm2.61i ¬zyAyFinAyzFin
65 64 ex ¬zyAyFinAyzFin
66 65 imim2d ¬zyAFinAyFinAFinAyzFin
67 66 adantl yFin¬zyAFinAyFinAFinAyzFin
68 3 6 9 12 15 67 findcard2s BFinAFinABFin
69 68 impcom AFinBFinABFin