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

Metamath Proof Explorer

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 𝐵 ) ∖ 𝐴 ) )