Metamath Proof Explorer

Theorem unfilem1

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 unfilem1 ran 𝐹 = ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 )

Proof

Step Hyp Ref Expression
1 unfilem1.1 ⊢ 𝐴 ∈ ω
2 unfilem1.2 ⊢ 𝐵 ∈ ω
3 unfilem1.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) )
4 elnn ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐵 ∈ ω ) → 𝑥 ∈ ω )
5 2 4 mpan2 ⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ω )
6 nnaord ⊢ ( ( 𝑥 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) → ( 𝑥 ∈ 𝐵 ↔ ( 𝐴 +o 𝑥 ) ∈ ( 𝐴 +o 𝐵 ) ) )
7 2 1 6 mp3an23 ⊢ ( 𝑥 ∈ ω → ( 𝑥 ∈ 𝐵 ↔ ( 𝐴 +o 𝑥 ) ∈ ( 𝐴 +o 𝐵 ) ) )
8 5 7 syl ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐵 ↔ ( 𝐴 +o 𝑥 ) ∈ ( 𝐴 +o 𝐵 ) ) )
9 8 ibi ⊢ ( 𝑥 ∈ 𝐵 → ( 𝐴 +o 𝑥 ) ∈ ( 𝐴 +o 𝐵 ) )
10 nnaword1 ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → 𝐴 ⊆ ( 𝐴 +o 𝑥 ) )
11 nnord ⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
12 nnacl ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ( 𝐴 +o 𝑥 ) ∈ ω )
13 nnord ⊢ ( ( 𝐴 +o 𝑥 ) ∈ ω → Ord ( 𝐴 +o 𝑥 ) )
14 12 13 syl ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → Ord ( 𝐴 +o 𝑥 ) )
15 ordtri1 ⊢ ( ( Ord 𝐴 ∧ Ord ( 𝐴 +o 𝑥 ) ) → ( 𝐴 ⊆ ( 𝐴 +o 𝑥 ) ↔ ¬ ( 𝐴 +o 𝑥 ) ∈ 𝐴 ) )
16 11 14 15 syl2an2r ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ( 𝐴 ⊆ ( 𝐴 +o 𝑥 ) ↔ ¬ ( 𝐴 +o 𝑥 ) ∈ 𝐴 ) )
17 10 16 mpbid ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ¬ ( 𝐴 +o 𝑥 ) ∈ 𝐴 )
18 1 5 17 sylancr ⊢ ( 𝑥 ∈ 𝐵 → ¬ ( 𝐴 +o 𝑥 ) ∈ 𝐴 )
19 9 18 jca ⊢ ( 𝑥 ∈ 𝐵 → ( ( 𝐴 +o 𝑥 ) ∈ ( 𝐴 +o 𝐵 ) ∧ ¬ ( 𝐴 +o 𝑥 ) ∈ 𝐴 ) )
20 eleq1 ⊢ ( 𝑦 = ( 𝐴 +o 𝑥 ) → ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) ↔ ( 𝐴 +o 𝑥 ) ∈ ( 𝐴 +o 𝐵 ) ) )
21 eleq1 ⊢ ( 𝑦 = ( 𝐴 +o 𝑥 ) → ( 𝑦 ∈ 𝐴 ↔ ( 𝐴 +o 𝑥 ) ∈ 𝐴 ) )
22 21 notbid ⊢ ( 𝑦 = ( 𝐴 +o 𝑥 ) → ( ¬ 𝑦 ∈ 𝐴 ↔ ¬ ( 𝐴 +o 𝑥 ) ∈ 𝐴 ) )
23 20 22 anbi12d ⊢ ( 𝑦 = ( 𝐴 +o 𝑥 ) → ( ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) ∧ ¬ 𝑦 ∈ 𝐴 ) ↔ ( ( 𝐴 +o 𝑥 ) ∈ ( 𝐴 +o 𝐵 ) ∧ ¬ ( 𝐴 +o 𝑥 ) ∈ 𝐴 ) ) )
24 23 biimparc ⊢ ( ( ( ( 𝐴 +o 𝑥 ) ∈ ( 𝐴 +o 𝐵 ) ∧ ¬ ( 𝐴 +o 𝑥 ) ∈ 𝐴 ) ∧ 𝑦 = ( 𝐴 +o 𝑥 ) ) → ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) ∧ ¬ 𝑦 ∈ 𝐴 ) )
25 19 24 sylan ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 = ( 𝐴 +o 𝑥 ) ) → ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) ∧ ¬ 𝑦 ∈ 𝐴 ) )
26 25 rexlimiva ⊢ ( ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑥 ) → ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) ∧ ¬ 𝑦 ∈ 𝐴 ) )
27 1 2 nnacli ⊢ ( 𝐴 +o 𝐵 ) ∈ ω
28 elnn ⊢ ( ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) ∧ ( 𝐴 +o 𝐵 ) ∈ ω ) → 𝑦 ∈ ω )
29 27 28 mpan2 ⊢ ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) → 𝑦 ∈ ω )
30 nnord ⊢ ( 𝑦 ∈ ω → Ord 𝑦 )
31 ordtri1 ⊢ ( ( Ord 𝐴 ∧ Ord 𝑦 ) → ( 𝐴 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝐴 ) )
32 11 30 31 syl2an ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝐴 ) )
33 nnawordex ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ⊆ 𝑦 ↔ ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝑦 ) )
34 32 33 bitr3d ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ¬ 𝑦 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝑦 ) )
35 1 29 34 sylancr ⊢ ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) → ( ¬ 𝑦 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝑦 ) )
36 eleq1 ⊢ ( ( 𝐴 +o 𝑥 ) = 𝑦 → ( ( 𝐴 +o 𝑥 ) ∈ ( 𝐴 +o 𝐵 ) ↔ 𝑦 ∈ ( 𝐴 +o 𝐵 ) ) )
37 7 36 sylan9bb ⊢ ( ( 𝑥 ∈ ω ∧ ( 𝐴 +o 𝑥 ) = 𝑦 ) → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ ( 𝐴 +o 𝐵 ) ) )
38 37 biimprcd ⊢ ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) → ( ( 𝑥 ∈ ω ∧ ( 𝐴 +o 𝑥 ) = 𝑦 ) → 𝑥 ∈ 𝐵 ) )
39 eqcom ⊢ ( ( 𝐴 +o 𝑥 ) = 𝑦 ↔ 𝑦 = ( 𝐴 +o 𝑥 ) )
40 39 bilani ⊢ ( ( 𝑥 ∈ ω ∧ ( 𝐴 +o 𝑥 ) = 𝑦 ) → 𝑦 = ( 𝐴 +o 𝑥 ) )
41 38 40 jca2 ⊢ ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) → ( ( 𝑥 ∈ ω ∧ ( 𝐴 +o 𝑥 ) = 𝑦 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 = ( 𝐴 +o 𝑥 ) ) ) )
42 41 reximdv2 ⊢ ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) → ( ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑥 ) ) )
43 35 42 sylbid ⊢ ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) → ( ¬ 𝑦 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑥 ) ) )
44 43 imp ⊢ ( ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) ∧ ¬ 𝑦 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑥 ) )
45 26 44 impbii ⊢ ( ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑥 ) ↔ ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) ∧ ¬ 𝑦 ∈ 𝐴 ) )
46 ovex ⊢ ( 𝐴 +o 𝑥 ) ∈ V
47 3 46 elrnmpti ⊢ ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑥 ) )
48 eldif ⊢ ( 𝑦 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ↔ ( 𝑦 ∈ ( 𝐴 +o 𝐵 ) ∧ ¬ 𝑦 ∈ 𝐴 ) )
49 45 47 48 3bitr4i ⊢ ( 𝑦 ∈ ran 𝐹 ↔ 𝑦 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) )
50 49 eqriv ⊢ ran 𝐹 = ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 )