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 ⊢ A ∈ ω ∧ B ∈ ω → B ≈ A + 𝑜 B ∖ A

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = if A ∈ ω A ∅ → A + 𝑜 B = if A ∈ ω A ∅ + 𝑜 B
2 id ⊢ A = if A ∈ ω A ∅ → A = if A ∈ ω A ∅
3 1 2 difeq12d ⊢ A = if A ∈ ω A ∅ → A + 𝑜 B ∖ A = if A ∈ ω A ∅ + 𝑜 B ∖ if A ∈ ω A ∅
4 3 breq2d ⊢ A = if A ∈ ω A ∅ → B ≈ A + 𝑜 B ∖ A ↔ B ≈ if A ∈ ω A ∅ + 𝑜 B ∖ if A ∈ ω A ∅
5 id ⊢ B = if B ∈ ω B ∅ → B = if B ∈ ω B ∅
6 oveq2 ⊢ B = if B ∈ ω B ∅ → if A ∈ ω A ∅ + 𝑜 B = if A ∈ ω A ∅ + 𝑜 if B ∈ ω B ∅
7 6 difeq1d ⊢ B = if B ∈ ω B ∅ → if A ∈ ω A ∅ + 𝑜 B ∖ if A ∈ ω A ∅ = if A ∈ ω A ∅ + 𝑜 if B ∈ ω B ∅ ∖ if A ∈ ω A ∅
8 5 7 breq12d ⊢ B = if B ∈ ω B ∅ → B ≈ if A ∈ ω A ∅ + 𝑜 B ∖ if A ∈ ω A ∅ ↔ if B ∈ ω B ∅ ≈ if A ∈ ω A ∅ + 𝑜 if B ∈ ω B ∅ ∖ if A ∈ ω A ∅
9 peano1 ⊢ ∅ ∈ ω
10 9 elimel ⊢ if B ∈ ω B ∅ ∈ ω
11 ovex ⊢ if A ∈ ω A ∅ + 𝑜 if B ∈ ω B ∅ ∈ V
12 11 difexi ⊢ if A ∈ ω A ∅ + 𝑜 if B ∈ ω B ∅ ∖ if A ∈ ω A ∅ ∈ V
13 9 elimel ⊢ if A ∈ ω A ∅ ∈ ω
14 eqid ⊢ x ∈ if B ∈ ω B ∅ ⟼ if A ∈ ω A ∅ + 𝑜 x = x ∈ if B ∈ ω B ∅ ⟼ if A ∈ ω A ∅ + 𝑜 x
15 13 10 14 unfilem2 ⊢ x ∈ if B ∈ ω B ∅ ⟼ if A ∈ ω A ∅ + 𝑜 x : if B ∈ ω B ∅ ⟶ 1-1 onto if A ∈ ω A ∅ + 𝑜 if B ∈ ω B ∅ ∖ if A ∈ ω A ∅
16 f1oen2g ⊢ if B ∈ ω B ∅ ∈ ω ∧ if A ∈ ω A ∅ + 𝑜 if B ∈ ω B ∅ ∖ if A ∈ ω A ∅ ∈ V ∧ x ∈ if B ∈ ω B ∅ ⟼ if A ∈ ω A ∅ + 𝑜 x : if B ∈ ω B ∅ ⟶ 1-1 onto if A ∈ ω A ∅ + 𝑜 if B ∈ ω B ∅ ∖ if A ∈ ω A ∅ → if B ∈ ω B ∅ ≈ if A ∈ ω A ∅ + 𝑜 if B ∈ ω B ∅ ∖ if A ∈ ω A ∅
17 10 12 15 16 mp3an ⊢ if B ∈ ω B ∅ ≈ if A ∈ ω A ∅ + 𝑜 if B ∈ ω B ∅ ∖ if A ∈ ω A ∅
18 4 8 17 dedth2h ⊢ A ∈ ω ∧ B ∈ ω → B ≈ A + 𝑜 B ∖ A