This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 uneq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ∪ 𝑥 ) = ( 𝐴 ∪ ∅ ) )
2 1 eleq1d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ∪ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∪ ∅ ) ∈ Fin ) )
3 2 imbi2d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ∈ Fin → ( 𝐴 ∪ 𝑥 ) ∈ Fin ) ↔ ( 𝐴 ∈ Fin → ( 𝐴 ∪ ∅ ) ∈ Fin ) ) )
4 uneq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∪ 𝑥 ) = ( 𝐴 ∪ 𝑦 ) )
5 4 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∪ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∪ 𝑦 ) ∈ Fin ) )
6 5 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ Fin → ( 𝐴 ∪ 𝑥 ) ∈ Fin ) ↔ ( 𝐴 ∈ Fin → ( 𝐴 ∪ 𝑦 ) ∈ Fin ) ) )
7 uneq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐴 ∪ 𝑥 ) = ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) )
8 7 eleq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐴 ∪ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
9 8 imbi2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐴 ∈ Fin → ( 𝐴 ∪ 𝑥 ) ∈ Fin ) ↔ ( 𝐴 ∈ Fin → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) ) )
10 uneq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ∪ 𝑥 ) = ( 𝐴 ∪ 𝐵 ) )
11 10 eleq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∪ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∪ 𝐵 ) ∈ Fin ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ Fin → ( 𝐴 ∪ 𝑥 ) ∈ Fin ) ↔ ( 𝐴 ∈ Fin → ( 𝐴 ∪ 𝐵 ) ∈ Fin ) ) )
13 un0 ⊢ ( 𝐴 ∪ ∅ ) = 𝐴
14 13 eleq1i ⊢ ( ( 𝐴 ∪ ∅ ) ∈ Fin ↔ 𝐴 ∈ Fin )
15 14 biimpri ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∪ ∅ ) ∈ Fin )
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 ⊢ ( 𝑧 ∈ 𝐴 → ( ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ↔ ( 𝐴 ∪ 𝑦 ) ∈ Fin ) )
25 24 biimprd ⊢ ( 𝑧 ∈ 𝐴 → ( ( 𝐴 ∪ 𝑦 ) ∈ Fin → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
26 25 adantld ⊢ ( 𝑧 ∈ 𝐴 → ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝐴 ∪ 𝑦 ) ∈ Fin ) → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
27 isfi ⊢ ( ( 𝐴 ∪ 𝑦 ) ∈ Fin ↔ ∃ 𝑤 ∈ ω ( 𝐴 ∪ 𝑦 ) ≈ 𝑤 )
28 27 biimpi ⊢ ( ( 𝐴 ∪ 𝑦 ) ∈ Fin → ∃ 𝑤 ∈ ω ( 𝐴 ∪ 𝑦 ) ≈ 𝑤 )
29 r19.41v ⊢ ( ∃ 𝑤 ∈ ω ( ( 𝐴 ∪ 𝑦 ) ≈ 𝑤 ∧ ( ¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦 ) ) ↔ ( ∃ 𝑤 ∈ ω ( 𝐴 ∪ 𝑦 ) ≈ 𝑤 ∧ ( ¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦 ) ) )
30 disjsn ⊢ ( ( ( 𝐴 ∪ 𝑦 ) ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ ( 𝐴 ∪ 𝑦 ) )
31 elun ⊢ ( 𝑧 ∈ ( 𝐴 ∪ 𝑦 ) ↔ ( 𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦 ) )
32 31 notbii ⊢ ( ¬ 𝑧 ∈ ( 𝐴 ∪ 𝑦 ) ↔ ¬ ( 𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦 ) )
33 pm4.56 ⊢ ( ( ¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦 ) ↔ ¬ ( 𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦 ) )
34 32 33 bitr4i ⊢ ( ¬ 𝑧 ∈ ( 𝐴 ∪ 𝑦 ) ↔ ( ¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦 ) )
35 30 34 sylbbr ⊢ ( ( ¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝐴 ∪ 𝑦 ) ∩ { 𝑧 } ) = ∅ )
36 nnord ⊢ ( 𝑤 ∈ ω → Ord 𝑤 )
37 orddisj ⊢ ( Ord 𝑤 → ( 𝑤 ∩ { 𝑤 } ) = ∅ )
38 36 37 syl ⊢ ( 𝑤 ∈ ω → ( 𝑤 ∩ { 𝑤 } ) = ∅ )
39 en2sn ⊢ ( ( 𝑧 ∈ V ∧ 𝑤 ∈ V ) → { 𝑧 } ≈ { 𝑤 } )
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 ⊢ suc 𝑤 = ( 𝑤 ∪ { 𝑤 } )
50 peano2 ⊢ ( 𝑤 ∈ ω → suc 𝑤 ∈ ω )
51 49 50 eqeltrrid ⊢ ( 𝑤 ∈ ω → ( 𝑤 ∪ { 𝑤 } ) ∈ ω )
52 breq2 ⊢ ( 𝑣 = ( 𝑤 ∪ { 𝑤 } ) → ( ( ( 𝐴 ∪ 𝑦 ) ∪ { 𝑧 } ) ≈ 𝑣 ↔ ( ( 𝐴 ∪ 𝑦 ) ∪ { 𝑧 } ) ≈ ( 𝑤 ∪ { 𝑤 } ) ) )
53 52 rspcev ⊢ ( ( ( 𝑤 ∪ { 𝑤 } ) ∈ ω ∧ ( ( 𝐴 ∪ 𝑦 ) ∪ { 𝑧 } ) ≈ ( 𝑤 ∪ { 𝑤 } ) ) → ∃ 𝑣 ∈ ω ( ( 𝐴 ∪ 𝑦 ) ∪ { 𝑧 } ) ≈ 𝑣 )
54 51 53 sylan ⊢ ( ( 𝑤 ∈ ω ∧ ( ( 𝐴 ∪ 𝑦 ) ∪ { 𝑧 } ) ≈ ( 𝑤 ∪ { 𝑤 } ) ) → ∃ 𝑣 ∈ ω ( ( 𝐴 ∪ 𝑦 ) ∪ { 𝑧 } ) ≈ 𝑣 )
55 isfi ⊢ ( ( ( 𝐴 ∪ 𝑦 ) ∪ { 𝑧 } ) ∈ Fin ↔ ∃ 𝑣 ∈ ω ( ( 𝐴 ∪ 𝑦 ) ∪ { 𝑧 } ) ≈ 𝑣 )
56 54 55 sylibr ⊢ ( ( 𝑤 ∈ ω ∧ ( ( 𝐴 ∪ 𝑦 ) ∪ { 𝑧 } ) ≈ ( 𝑤 ∪ { 𝑤 } ) ) → ( ( 𝐴 ∪ 𝑦 ) ∪ { 𝑧 } ) ∈ Fin )
57 48 56 eqeltrrid ⊢ ( ( 𝑤 ∈ ω ∧ ( ( 𝐴 ∪ 𝑦 ) ∪ { 𝑧 } ) ≈ ( 𝑤 ∪ { 𝑤 } ) ) → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
58 47 57 syldan ⊢ ( ( 𝑤 ∈ ω ∧ ( ( 𝐴 ∪ 𝑦 ) ≈ 𝑤 ∧ ( ¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦 ) ) ) → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
59 58 rexlimiva ⊢ ( ∃ 𝑤 ∈ ω ( ( 𝐴 ∪ 𝑦 ) ≈ 𝑤 ∧ ( ¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
60 29 59 sylbir ⊢ ( ( ∃ 𝑤 ∈ ω ( 𝐴 ∪ 𝑦 ) ≈ 𝑤 ∧ ( ¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
61 28 60 sylan ⊢ ( ( ( 𝐴 ∪ 𝑦 ) ∈ Fin ∧ ( ¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
62 61 ancoms ⊢ ( ( ( ¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐴 ∪ 𝑦 ) ∈ Fin ) → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
63 62 expl ⊢ ( ¬ 𝑧 ∈ 𝐴 → ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝐴 ∪ 𝑦 ) ∈ Fin ) → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
64 26 63 pm2.61i ⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝐴 ∪ 𝑦 ) ∈ Fin ) → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
65 64 ex ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( 𝐴 ∪ 𝑦 ) ∈ Fin → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
66 65 imim2d ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( 𝐴 ∈ Fin → ( 𝐴 ∪ 𝑦 ) ∈ Fin ) → ( 𝐴 ∈ Fin → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) ) )
67 66 adantl ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝐴 ∈ Fin → ( 𝐴 ∪ 𝑦 ) ∈ Fin ) → ( 𝐴 ∈ Fin → ( 𝐴 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) ) )
68 3 6 9 12 15 67 findcard2s ⊢ ( 𝐵 ∈ Fin → ( 𝐴 ∈ Fin → ( 𝐴 ∪ 𝐵 ) ∈ Fin ) )
69 68 impcom ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )