Theorem domalom

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

	Ref	Expression
Assertion	domalom	⊢ ( ∀ 𝑛 ∈ ω 𝑛 ≼ 𝐴 → ¬ 𝐴 ∈ Fin )

Proof

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