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)

	Ref	Expression
Assertion	unfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		diffi	⊢ ( 𝐵 ∈ Fin → ( 𝐵 ∖ 𝐴 ) ∈ Fin )
2		reeanv	⊢ ( ∃ 𝑥 ∈ ω ∃ 𝑦 ∈ ω ( 𝐴 ≈ 𝑥 ∧ ( 𝐵 ∖ 𝐴 ) ≈ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃ 𝑦 ∈ ω ( 𝐵 ∖ 𝐴 ) ≈ 𝑦 ) )
3		isfi	⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
4		isfi	⊢ ( ( 𝐵 ∖ 𝐴 ) ∈ Fin ↔ ∃ 𝑦 ∈ ω ( 𝐵 ∖ 𝐴 ) ≈ 𝑦 )
5	3 4	anbi12i	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐵 ∖ 𝐴 ) ∈ Fin ) ↔ ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃ 𝑦 ∈ ω ( 𝐵 ∖ 𝐴 ) ≈ 𝑦 ) )
6	2 5	bitr4i	⊢ ( ∃ 𝑥 ∈ ω ∃ 𝑦 ∈ ω ( 𝐴 ≈ 𝑥 ∧ ( 𝐵 ∖ 𝐴 ) ≈ 𝑦 ) ↔ ( 𝐴 ∈ Fin ∧ ( 𝐵 ∖ 𝐴 ) ∈ Fin ) )
7		nnacl	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑥 +o 𝑦 ) ∈ ω )
8		unfilem3	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → 𝑦 ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) )
9		entr	⊢ ( ( ( 𝐵 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) → ( 𝐵 ∖ 𝐴 ) ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) )
10	9	expcom	⊢ ( 𝑦 ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) → ( ( 𝐵 ∖ 𝐴 ) ≈ 𝑦 → ( 𝐵 ∖ 𝐴 ) ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) )
11	8 10	syl	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐵 ∖ 𝐴 ) ≈ 𝑦 → ( 𝐵 ∖ 𝐴 ) ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) )
12		disjdif	⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
13		disjdif	⊢ ( 𝑥 ∩ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) = ∅
14		unen	⊢ ( ( ( 𝐴 ≈ 𝑥 ∧ ( 𝐵 ∖ 𝐴 ) ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) ∧ ( ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅ ∧ ( 𝑥 ∩ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) = ∅ ) ) → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ≈ ( 𝑥 ∪ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) )
15	12 13 14	mpanr12	⊢ ( ( 𝐴 ≈ 𝑥 ∧ ( 𝐵 ∖ 𝐴 ) ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ≈ ( 𝑥 ∪ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) )
16		undif2	⊢ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = ( 𝐴 ∪ 𝐵 )
17	16	a1i	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = ( 𝐴 ∪ 𝐵 ) )
18		nnaword1	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → 𝑥 ⊆ ( 𝑥 +o 𝑦 ) )
19		undif	⊢ ( 𝑥 ⊆ ( 𝑥 +o 𝑦 ) ↔ ( 𝑥 ∪ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) = ( 𝑥 +o 𝑦 ) )
20	18 19	sylib	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑥 ∪ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) = ( 𝑥 +o 𝑦 ) )
21	17 20	breq12d	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ≈ ( 𝑥 ∪ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) ↔ ( 𝐴 ∪ 𝐵 ) ≈ ( 𝑥 +o 𝑦 ) ) )
22	15 21	syl5ib	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ≈ 𝑥 ∧ ( 𝐵 ∖ 𝐴 ) ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) → ( 𝐴 ∪ 𝐵 ) ≈ ( 𝑥 +o 𝑦 ) ) )
23	11 22	sylan2d	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ≈ 𝑥 ∧ ( 𝐵 ∖ 𝐴 ) ≈ 𝑦 ) → ( 𝐴 ∪ 𝐵 ) ≈ ( 𝑥 +o 𝑦 ) ) )
24		breq2	⊢ ( 𝑧 = ( 𝑥 +o 𝑦 ) → ( ( 𝐴 ∪ 𝐵 ) ≈ 𝑧 ↔ ( 𝐴 ∪ 𝐵 ) ≈ ( 𝑥 +o 𝑦 ) ) )
25	24	rspcev	⊢ ( ( ( 𝑥 +o 𝑦 ) ∈ ω ∧ ( 𝐴 ∪ 𝐵 ) ≈ ( 𝑥 +o 𝑦 ) ) → ∃ 𝑧 ∈ ω ( 𝐴 ∪ 𝐵 ) ≈ 𝑧 )
26		isfi	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin ↔ ∃ 𝑧 ∈ ω ( 𝐴 ∪ 𝐵 ) ≈ 𝑧 )
27	25 26	sylibr	⊢ ( ( ( 𝑥 +o 𝑦 ) ∈ ω ∧ ( 𝐴 ∪ 𝐵 ) ≈ ( 𝑥 +o 𝑦 ) ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )
28	7 23 27	syl6an	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ≈ 𝑥 ∧ ( 𝐵 ∖ 𝐴 ) ≈ 𝑦 ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin ) )
29	28	rexlimivv	⊢ ( ∃ 𝑥 ∈ ω ∃ 𝑦 ∈ ω ( 𝐴 ≈ 𝑥 ∧ ( 𝐵 ∖ 𝐴 ) ≈ 𝑦 ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )
30	6 29	sylbir	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐵 ∖ 𝐴 ) ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )
31	1 30	sylan2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )