Metamath Proof Explorer

Theorem domalom

Description: A class which dominates every natural number is not finite. (Contributed by ML, 14-Dec-2020)

Ref Expression
Assertion domalom ⊢ ∀ n ∈ ω n ≼ A → ¬ A ∈ Fin

Proof

Step Hyp Ref Expression
1 nfra1 ⊢ Ⅎ n ∀ n ∈ ω n ≼ A
2 breq1 ⊢ y = n → y ≺ A ↔ n ≺ A
3 2 imbi2d ⊢ y = n → ∀ n ∈ ω n ≼ A → y ≺ A ↔ ∀ n ∈ ω n ≼ A → n ≺ A
4 breq1 ⊢ y = ∅ → y ≺ A ↔ ∅ ≺ A
5 breq1 ⊢ y = z → y ≺ A ↔ z ≺ A
6 breq1 ⊢ y = suc ⁡ z → y ≺ A ↔ suc ⁡ z ≺ A
7 1n0 ⊢ 1 𝑜 ≠ ∅
8 1onn ⊢ 1 𝑜 ∈ ω
9 0sdomg ⊢ 1 𝑜 ∈ ω → ∅ ≺ 1 𝑜 ↔ 1 𝑜 ≠ ∅
10 8 9 ax-mp ⊢ ∅ ≺ 1 𝑜 ↔ 1 𝑜 ≠ ∅
11 7 10 mpbir ⊢ ∅ ≺ 1 𝑜
12 breq1 ⊢ n = 1 𝑜 → n ≼ A ↔ 1 𝑜 ≼ A
13 12 rspccv ⊢ ∀ n ∈ ω n ≼ A → 1 𝑜 ∈ ω → 1 𝑜 ≼ A
14 8 13 mpi ⊢ ∀ n ∈ ω n ≼ A → 1 𝑜 ≼ A
15 sdomdomtr ⊢ ∅ ≺ 1 𝑜 ∧ 1 𝑜 ≼ A → ∅ ≺ A
16 11 14 15 sylancr ⊢ ∀ n ∈ ω n ≼ A → ∅ ≺ A
17 peano2 ⊢ z ∈ ω → suc ⁡ z ∈ ω
18 php4 ⊢ suc ⁡ z ∈ ω → suc ⁡ z ≺ suc ⁡ suc ⁡ z
19 17 18 syl ⊢ z ∈ ω → suc ⁡ z ≺ suc ⁡ suc ⁡ z
20 breq1 ⊢ n = suc ⁡ suc ⁡ z → n ≼ A ↔ suc ⁡ suc ⁡ z ≼ A
21 20 rspccv ⊢ ∀ n ∈ ω n ≼ A → suc ⁡ suc ⁡ z ∈ ω → suc ⁡ suc ⁡ z ≼ A
22 peano2 ⊢ suc ⁡ z ∈ ω → suc ⁡ suc ⁡ z ∈ ω
23 17 22 syl ⊢ z ∈ ω → suc ⁡ suc ⁡ z ∈ ω
24 21 23 impel ⊢ ∀ n ∈ ω n ≼ A ∧ z ∈ ω → suc ⁡ suc ⁡ z ≼ A
25 sdomdomtr ⊢ suc ⁡ z ≺ suc ⁡ suc ⁡ z ∧ suc ⁡ suc ⁡ z ≼ A → suc ⁡ z ≺ A
26 19 24 25 syl2an2 ⊢ ∀ n ∈ ω n ≼ A ∧ z ∈ ω → suc ⁡ z ≺ A
27 26 a1d ⊢ ∀ n ∈ ω n ≼ A ∧ z ∈ ω → z ≺ A → suc ⁡ z ≺ A
28 27 expcom ⊢ z ∈ ω → ∀ n ∈ ω n ≼ A → z ≺ A → suc ⁡ z ≺ A
29 4 5 6 16 28 finds2 ⊢ y ∈ ω → ∀ n ∈ ω n ≼ A → y ≺ A
30 3 29 vtoclga ⊢ n ∈ ω → ∀ n ∈ ω n ≼ A → n ≺ A
31 30 com12 ⊢ ∀ n ∈ ω n ≼ A → n ∈ ω → n ≺ A
32 1 31 ralrimi ⊢ ∀ n ∈ ω n ≼ A → ∀ n ∈ ω n ≺ A
33 sdomnen ⊢ n ≺ A → ¬ n ≈ A
34 ensym ⊢ A ≈ n → n ≈ A
35 33 34 nsyl ⊢ n ≺ A → ¬ A ≈ n
36 35 ralimi ⊢ ∀ n ∈ ω n ≺ A → ∀ n ∈ ω ¬ A ≈ n
37 32 36 syl ⊢ ∀ n ∈ ω n ≼ A → ∀ n ∈ ω ¬ A ≈ n
38 isfi ⊢ A ∈ Fin ↔ ∃ n ∈ ω A ≈ n
39 38 notbii ⊢ ¬ A ∈ Fin ↔ ¬ ∃ n ∈ ω A ≈ n
40 ralnex ⊢ ∀ n ∈ ω ¬ A ≈ n ↔ ¬ ∃ n ∈ ω A ≈ n
41 39 40 bitr4i ⊢ ¬ A ∈ Fin ↔ ∀ n ∈ ω ¬ A ≈ n
42 37 41 sylibr ⊢ ∀ n ∈ ω n ≼ A → ¬ A ∈ Fin