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=ifA∈ωA∅→A+𝑜B=ifA∈ωA∅+𝑜B
2 id ⊢A=ifA∈ωA∅→A=ifA∈ωA∅
3 1 2 difeq12d ⊢A=ifA∈ωA∅→A+𝑜B∖A=ifA∈ωA∅+𝑜B∖ifA∈ωA∅
4 3 breq2d ⊢A=ifA∈ωA∅→B≈A+𝑜B∖A↔B≈ifA∈ωA∅+𝑜B∖ifA∈ωA∅
5 id ⊢B=ifB∈ωB∅→B=ifB∈ωB∅
6 oveq2 ⊢B=ifB∈ωB∅→ifA∈ωA∅+𝑜B=ifA∈ωA∅+𝑜ifB∈ωB∅
7 6 difeq1d ⊢B=ifB∈ωB∅→ifA∈ωA∅+𝑜B∖ifA∈ωA∅=ifA∈ωA∅+𝑜ifB∈ωB∅∖ifA∈ωA∅
8 5 7 breq12d ⊢B=ifB∈ωB∅→B≈ifA∈ωA∅+𝑜B∖ifA∈ωA∅↔ifB∈ωB∅≈ifA∈ωA∅+𝑜ifB∈ωB∅∖ifA∈ωA∅
9 peano1 ⊢∅∈ω
10 9 elimel ⊢ifB∈ωB∅∈ω
11 ovex ⊢ifA∈ωA∅+𝑜ifB∈ωB∅∈V
12 11 difexi ⊢ifA∈ωA∅+𝑜ifB∈ωB∅∖ifA∈ωA∅∈V
13 9 elimel ⊢ifA∈ωA∅∈ω
14 eqid ⊢x∈ifB∈ωB∅⟼ifA∈ωA∅+𝑜x=x∈ifB∈ωB∅⟼ifA∈ωA∅+𝑜x
15 13 10 14 unfilem2 ⊢x∈ifB∈ωB∅⟼ifA∈ωA∅+𝑜x:ifB∈ωB∅⟶1-1 ontoifA∈ωA∅+𝑜ifB∈ωB∅∖ifA∈ωA∅
16 f1oen2g ⊢ifB∈ωB∅∈ω∧ifA∈ωA∅+𝑜ifB∈ωB∅∖ifA∈ωA∅∈V∧x∈ifB∈ωB∅⟼ifA∈ωA∅+𝑜x:ifB∈ωB∅⟶1-1 ontoifA∈ωA∅+𝑜ifB∈ωB∅∖ifA∈ωA∅→ifB∈ωB∅≈ifA∈ωA∅+𝑜ifB∈ωB∅∖ifA∈ωA∅
17 10 12 15 16 mp3an ⊢ifB∈ωB∅≈ifA∈ωA∅+𝑜ifB∈ωB∅∖ifA∈ωA∅
18 4 8 17 dedth2h ⊢A∈ω∧B∈ω→B≈A+𝑜B∖A