Theorem unfilem3

Description: Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 16-Nov-2002) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	unfilem3	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝐵 ≈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝐴 = if ( 𝐴 ∈ ω , 𝐴 , ∅ ) → ( 𝐴 +o 𝐵 ) = ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) )
2		id	⊢ ( 𝐴 = if ( 𝐴 ∈ ω , 𝐴 , ∅ ) → 𝐴 = if ( 𝐴 ∈ ω , 𝐴 , ∅ ) )
3	1 2	difeq12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ω , 𝐴 , ∅ ) → ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) = ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ∖ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) ) )
4	3	breq2d	⊢ ( 𝐴 = if ( 𝐴 ∈ ω , 𝐴 , ∅ ) → ( 𝐵 ≈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ↔ 𝐵 ≈ ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ∖ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) ) ) )
5		id	⊢ ( 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) → 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) )
6		oveq2	⊢ ( 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) → ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) = ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) )
7	6	difeq1d	⊢ ( 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) → ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ∖ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) ) = ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ∖ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) ) )
8	5 7	breq12d	⊢ ( 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) → ( 𝐵 ≈ ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ∖ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) ) ↔ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ≈ ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ∖ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) ) ) )
9		peano1	⊢ ∅ ∈ ω
10	9	elimel	⊢ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ∈ ω
11		ovex	⊢ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ∈ V
12	11	difexi	⊢ ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ∖ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) ) ∈ V
13	9	elimel	⊢ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) ∈ ω
14		eqid	⊢ ( 𝑥 ∈ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ↦ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝑥 ) ) = ( 𝑥 ∈ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ↦ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝑥 ) )
15	13 10 14	unfilem2	⊢ ( 𝑥 ∈ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ↦ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝑥 ) ) : if ( 𝐵 ∈ ω , 𝐵 , ∅ ) –1-1-onto→ ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ∖ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) )
16		f1oen2g	⊢ ( ( if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ∈ ω ∧ ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ∖ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) ) ∈ V ∧ ( 𝑥 ∈ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ↦ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝑥 ) ) : if ( 𝐵 ∈ ω , 𝐵 , ∅ ) –1-1-onto→ ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ∖ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) ) ) → if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ≈ ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ∖ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) ) )
17	10 12 15 16	mp3an	⊢ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ≈ ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ∖ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) )
18	4 8 17	dedth2h	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝐵 ≈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) )