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

Metamath Proof Explorer

Theorem unfilem2

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

Ref Expression
Hypotheses unfilem1.1 ⊢ 𝐴 ∈ ω
unfilem1.2 ⊢ 𝐵 ∈ ω
unfilem1.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) )
Assertion unfilem2 𝐹 : 𝐵 –1-1-onto→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 )

Proof

Step Hyp Ref Expression
1 unfilem1.1 ⊢ 𝐴 ∈ ω
2 unfilem1.2 ⊢ 𝐵 ∈ ω
3 unfilem1.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) )
4 ovex ⊢ ( 𝐴 +o 𝑥 ) ∈ V
5 4 3 fnmpti ⊢ 𝐹 Fn 𝐵
6 1 2 3 unfilem1 ⊢ ran 𝐹 = ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 )
7 df-fo ⊢ ( 𝐹 : 𝐵 –onto→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ↔ ( 𝐹 Fn 𝐵 ∧ ran 𝐹 = ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) )
8 5 6 7 mpbir2an ⊢ 𝐹 : 𝐵 –onto→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 )
9 fof ⊢ ( 𝐹 : 𝐵 –onto→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) → 𝐹 : 𝐵 ⟶ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) )
10 8 9 ax-mp ⊢ 𝐹 : 𝐵 ⟶ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 )
11 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑧 ) )
12 ovex ⊢ ( 𝐴 +o 𝑧 ) ∈ V
13 11 3 12 fvmpt ⊢ ( 𝑧 ∈ 𝐵 → ( 𝐹 ‘ 𝑧 ) = ( 𝐴 +o 𝑧 ) )
14 oveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑤 ) )
15 ovex ⊢ ( 𝐴 +o 𝑤 ) ∈ V
16 14 3 15 fvmpt ⊢ ( 𝑤 ∈ 𝐵 → ( 𝐹 ‘ 𝑤 ) = ( 𝐴 +o 𝑤 ) )
17 13 16 eqeqan12d ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐴 +o 𝑧 ) = ( 𝐴 +o 𝑤 ) ) )
18 elnn ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝐵 ∈ ω ) → 𝑧 ∈ ω )
19 2 18 mpan2 ⊢ ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ω )
20 elnn ⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝐵 ∈ ω ) → 𝑤 ∈ ω )
21 2 20 mpan2 ⊢ ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ω )
22 nnacan ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) → ( ( 𝐴 +o 𝑧 ) = ( 𝐴 +o 𝑤 ) ↔ 𝑧 = 𝑤 ) )
23 1 19 21 22 mp3an3an ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝐴 +o 𝑧 ) = ( 𝐴 +o 𝑤 ) ↔ 𝑧 = 𝑤 ) )
24 17 23 bitrd ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ 𝑧 = 𝑤 ) )
25 24 biimpd ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
26 25 rgen2 ⊢ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 )
27 dff13 ⊢ ( 𝐹 : 𝐵 –1-1→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ↔ ( 𝐹 : 𝐵 ⟶ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
28 10 26 27 mpbir2an ⊢ 𝐹 : 𝐵 –1-1→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 )
29 df-f1o ⊢ ( 𝐹 : 𝐵 –1-1-onto→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ↔ ( 𝐹 : 𝐵 –1-1→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ∧ 𝐹 : 𝐵 –onto→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) )
30 28 8 29 mpbir2an ⊢ 𝐹 : 𝐵 –1-1-onto→ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 )