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 
|- ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )

Proof

Step Hyp Ref Expression
1 uneq2 
 |-  ( x = (/) -> ( A u. x ) = ( A u. (/) ) )
2 1 eleq1d 
 |-  ( x = (/) -> ( ( A u. x ) e. Fin <-> ( A u. (/) ) e. Fin ) )
3 2 imbi2d 
 |-  ( x = (/) -> ( ( A e. Fin -> ( A u. x ) e. Fin ) <-> ( A e. Fin -> ( A u. (/) ) e. Fin ) ) )
4 uneq2 
 |-  ( x = y -> ( A u. x ) = ( A u. y ) )
5 4 eleq1d 
 |-  ( x = y -> ( ( A u. x ) e. Fin <-> ( A u. y ) e. Fin ) )
6 5 imbi2d 
 |-  ( x = y -> ( ( A e. Fin -> ( A u. x ) e. Fin ) <-> ( A e. Fin -> ( A u. y ) e. Fin ) ) )
7 uneq2 
 |-  ( x = ( y u. { z } ) -> ( A u. x ) = ( A u. ( y u. { z } ) ) )
8 7 eleq1d 
 |-  ( x = ( y u. { z } ) -> ( ( A u. x ) e. Fin <-> ( A u. ( y u. { z } ) ) e. Fin ) )
9 8 imbi2d 
 |-  ( x = ( y u. { z } ) -> ( ( A e. Fin -> ( A u. x ) e. Fin ) <-> ( A e. Fin -> ( A u. ( y u. { z } ) ) e. Fin ) ) )
10 uneq2 
 |-  ( x = B -> ( A u. x ) = ( A u. B ) )
11 10 eleq1d 
 |-  ( x = B -> ( ( A u. x ) e. Fin <-> ( A u. B ) e. Fin ) )
12 11 imbi2d 
 |-  ( x = B -> ( ( A e. Fin -> ( A u. x ) e. Fin ) <-> ( A e. Fin -> ( A u. B ) e. Fin ) ) )
13 un0 
 |-  ( A u. (/) ) = A
14 13 eleq1i 
 |-  ( ( A u. (/) ) e. Fin <-> A e. Fin )
15 14 biimpri 
 |-  ( A e. Fin -> ( A u. (/) ) e. Fin )
16 snssi 
 |-  ( z e. A -> { z } C_ A )
17 ssequn2 
 |-  ( { z } C_ A <-> ( A u. { z } ) = A )
18 17 biimpi 
 |-  ( { z } C_ A -> ( A u. { z } ) = A )
19 18 uneq2d 
 |-  ( { z } C_ A -> ( y u. ( A u. { z } ) ) = ( y u. A ) )
20 un12 
 |-  ( A u. ( y u. { z } ) ) = ( y u. ( A u. { z } ) )
21 uncom 
 |-  ( A u. y ) = ( y u. A )
22 19 20 21 3eqtr4g 
 |-  ( { z } C_ A -> ( A u. ( y u. { z } ) ) = ( A u. y ) )
23 16 22 syl 
 |-  ( z e. A -> ( A u. ( y u. { z } ) ) = ( A u. y ) )
24 23 eleq1d 
 |-  ( z e. A -> ( ( A u. ( y u. { z } ) ) e. Fin <-> ( A u. y ) e. Fin ) )
25 24 biimprd 
 |-  ( z e. A -> ( ( A u. y ) e. Fin -> ( A u. ( y u. { z } ) ) e. Fin ) )
26 25 adantld 
 |-  ( z e. A -> ( ( -. z e. y /\ ( A u. y ) e. Fin ) -> ( A u. ( y u. { z } ) ) e. Fin ) )
27 isfi 
 |-  ( ( A u. y ) e. Fin <-> E. w e. _om ( A u. y ) ~~ w )
28 27 biimpi 
 |-  ( ( A u. y ) e. Fin -> E. w e. _om ( A u. y ) ~~ w )
29 r19.41v 
 |-  ( E. w e. _om ( ( A u. y ) ~~ w /\ ( -. z e. A /\ -. z e. y ) ) <-> ( E. w e. _om ( A u. y ) ~~ w /\ ( -. z e. A /\ -. z e. y ) ) )
30 disjsn 
 |-  ( ( ( A u. y ) i^i { z } ) = (/) <-> -. z e. ( A u. y ) )
31 elun 
 |-  ( z e. ( A u. y ) <-> ( z e. A \/ z e. y ) )
32 31 notbii 
 |-  ( -. z e. ( A u. y ) <-> -. ( z e. A \/ z e. y ) )
33 pm4.56 
 |-  ( ( -. z e. A /\ -. z e. y ) <-> -. ( z e. A \/ z e. y ) )
34 32 33 bitr4i 
 |-  ( -. z e. ( A u. y ) <-> ( -. z e. A /\ -. z e. y ) )
35 30 34 sylbbr 
 |-  ( ( -. z e. A /\ -. z e. y ) -> ( ( A u. y ) i^i { z } ) = (/) )
36 nnord 
 |-  ( w e. _om -> Ord w )
37 orddisj 
 |-  ( Ord w -> ( w i^i { w } ) = (/) )
38 36 37 syl 
 |-  ( w e. _om -> ( w i^i { w } ) = (/) )
39 en2sn 
 |-  ( ( z e. _V /\ w e. _V ) -> { z } ~~ { w } )
40 39 el2v 
 |-  { z } ~~ { w }
41 unen 
 |-  ( ( ( ( A u. y ) ~~ w /\ { z } ~~ { w } ) /\ ( ( ( A u. y ) i^i { z } ) = (/) /\ ( w i^i { w } ) = (/) ) ) -> ( ( A u. y ) u. { z } ) ~~ ( w u. { w } ) )
42 40 41 mpanl2 
 |-  ( ( ( A u. y ) ~~ w /\ ( ( ( A u. y ) i^i { z } ) = (/) /\ ( w i^i { w } ) = (/) ) ) -> ( ( A u. y ) u. { z } ) ~~ ( w u. { w } ) )
43 38 42 sylanr2 
 |-  ( ( ( A u. y ) ~~ w /\ ( ( ( A u. y ) i^i { z } ) = (/) /\ w e. _om ) ) -> ( ( A u. y ) u. { z } ) ~~ ( w u. { w } ) )
44 35 43 sylanr1 
 |-  ( ( ( A u. y ) ~~ w /\ ( ( -. z e. A /\ -. z e. y ) /\ w e. _om ) ) -> ( ( A u. y ) u. { z } ) ~~ ( w u. { w } ) )
45 44 3impb 
 |-  ( ( ( A u. y ) ~~ w /\ ( -. z e. A /\ -. z e. y ) /\ w e. _om ) -> ( ( A u. y ) u. { z } ) ~~ ( w u. { w } ) )
46 45 3comr 
 |-  ( ( w e. _om /\ ( A u. y ) ~~ w /\ ( -. z e. A /\ -. z e. y ) ) -> ( ( A u. y ) u. { z } ) ~~ ( w u. { w } ) )
47 46 3expb 
 |-  ( ( w e. _om /\ ( ( A u. y ) ~~ w /\ ( -. z e. A /\ -. z e. y ) ) ) -> ( ( A u. y ) u. { z } ) ~~ ( w u. { w } ) )
48 unass 
 |-  ( ( A u. y ) u. { z } ) = ( A u. ( y u. { z } ) )
49 df-suc 
 |-  suc w = ( w u. { w } )
50 peano2 
 |-  ( w e. _om -> suc w e. _om )
51 49 50 eqeltrrid 
 |-  ( w e. _om -> ( w u. { w } ) e. _om )
52 breq2 
 |-  ( v = ( w u. { w } ) -> ( ( ( A u. y ) u. { z } ) ~~ v <-> ( ( A u. y ) u. { z } ) ~~ ( w u. { w } ) ) )
53 52 rspcev 
 |-  ( ( ( w u. { w } ) e. _om /\ ( ( A u. y ) u. { z } ) ~~ ( w u. { w } ) ) -> E. v e. _om ( ( A u. y ) u. { z } ) ~~ v )
54 51 53 sylan 
 |-  ( ( w e. _om /\ ( ( A u. y ) u. { z } ) ~~ ( w u. { w } ) ) -> E. v e. _om ( ( A u. y ) u. { z } ) ~~ v )
55 isfi 
 |-  ( ( ( A u. y ) u. { z } ) e. Fin <-> E. v e. _om ( ( A u. y ) u. { z } ) ~~ v )
56 54 55 sylibr 
 |-  ( ( w e. _om /\ ( ( A u. y ) u. { z } ) ~~ ( w u. { w } ) ) -> ( ( A u. y ) u. { z } ) e. Fin )
57 48 56 eqeltrrid 
 |-  ( ( w e. _om /\ ( ( A u. y ) u. { z } ) ~~ ( w u. { w } ) ) -> ( A u. ( y u. { z } ) ) e. Fin )
58 47 57 syldan 
 |-  ( ( w e. _om /\ ( ( A u. y ) ~~ w /\ ( -. z e. A /\ -. z e. y ) ) ) -> ( A u. ( y u. { z } ) ) e. Fin )
59 58 rexlimiva 
 |-  ( E. w e. _om ( ( A u. y ) ~~ w /\ ( -. z e. A /\ -. z e. y ) ) -> ( A u. ( y u. { z } ) ) e. Fin )
60 29 59 sylbir 
 |-  ( ( E. w e. _om ( A u. y ) ~~ w /\ ( -. z e. A /\ -. z e. y ) ) -> ( A u. ( y u. { z } ) ) e. Fin )
61 28 60 sylan 
 |-  ( ( ( A u. y ) e. Fin /\ ( -. z e. A /\ -. z e. y ) ) -> ( A u. ( y u. { z } ) ) e. Fin )
62 61 ancoms 
 |-  ( ( ( -. z e. A /\ -. z e. y ) /\ ( A u. y ) e. Fin ) -> ( A u. ( y u. { z } ) ) e. Fin )
63 62 expl 
 |-  ( -. z e. A -> ( ( -. z e. y /\ ( A u. y ) e. Fin ) -> ( A u. ( y u. { z } ) ) e. Fin ) )
64 26 63 pm2.61i 
 |-  ( ( -. z e. y /\ ( A u. y ) e. Fin ) -> ( A u. ( y u. { z } ) ) e. Fin )
65 64 ex 
 |-  ( -. z e. y -> ( ( A u. y ) e. Fin -> ( A u. ( y u. { z } ) ) e. Fin ) )
66 65 imim2d 
 |-  ( -. z e. y -> ( ( A e. Fin -> ( A u. y ) e. Fin ) -> ( A e. Fin -> ( A u. ( y u. { z } ) ) e. Fin ) ) )
67 66 adantl 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( A e. Fin -> ( A u. y ) e. Fin ) -> ( A e. Fin -> ( A u. ( y u. { z } ) ) e. Fin ) ) )
68 3 6 9 12 15 67 findcard2s 
 |-  ( B e. Fin -> ( A e. Fin -> ( A u. B ) e. Fin ) )
69 68 impcom 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )