Theorem isfinite2

Description: Any set strictly dominated by the class of natural numbers is finite. Sufficiency part of Theorem 42 of Suppes p. 151. This theorem does not require the Axiom of Infinity. (Contributed by NM, 24-Apr-2004)

	Ref	Expression
Assertion	isfinite2	⊢ ( 𝐴 ≺ ω → 𝐴 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		relsdom	⊢ Rel ≺
2	1	brrelex2i	⊢ ( 𝐴 ≺ ω → ω ∈ V )
3		sdomdom	⊢ ( 𝐴 ≺ ω → 𝐴 ≼ ω )
4		domeng	⊢ ( ω ∈ V → ( 𝐴 ≼ ω ↔ ∃ 𝑦 ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) ) )
5	3 4	imbitrid	⊢ ( ω ∈ V → ( 𝐴 ≺ ω → ∃ 𝑦 ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) ) )
6		ensym	⊢ ( 𝐴 ≈ 𝑦 → 𝑦 ≈ 𝐴 )
7	6	ad2antrl	⊢ ( ( 𝐴 ≺ ω ∧ ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) ) → 𝑦 ≈ 𝐴 )
8		simpl	⊢ ( ( 𝐴 ≺ ω ∧ ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) ) → 𝐴 ≺ ω )
9		ensdomtr	⊢ ( ( 𝑦 ≈ 𝐴 ∧ 𝐴 ≺ ω ) → 𝑦 ≺ ω )
10	7 8 9	syl2anc	⊢ ( ( 𝐴 ≺ ω ∧ ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) ) → 𝑦 ≺ ω )
11		sdomnen	⊢ ( 𝑦 ≺ ω → ¬ 𝑦 ≈ ω )
12	10 11	syl	⊢ ( ( 𝐴 ≺ ω ∧ ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) ) → ¬ 𝑦 ≈ ω )
13		simpr	⊢ ( ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) → 𝑦 ⊆ ω )
14		unbnn	⊢ ( ( ω ∈ V ∧ 𝑦 ⊆ ω ∧ ∀ 𝑧 ∈ ω ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 ) → 𝑦 ≈ ω )
15	14	3expia	⊢ ( ( ω ∈ V ∧ 𝑦 ⊆ ω ) → ( ∀ 𝑧 ∈ ω ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ≈ ω ) )
16	2 13 15	syl2an	⊢ ( ( 𝐴 ≺ ω ∧ ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) ) → ( ∀ 𝑧 ∈ ω ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ≈ ω ) )
17	12 16	mtod	⊢ ( ( 𝐴 ≺ ω ∧ ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) ) → ¬ ∀ 𝑧 ∈ ω ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 )
18		rexnal	⊢ ( ∃ 𝑧 ∈ ω ¬ ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 ↔ ¬ ∀ 𝑧 ∈ ω ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 )
19		omsson	⊢ ω ⊆ On
20		sstr	⊢ ( ( 𝑦 ⊆ ω ∧ ω ⊆ On ) → 𝑦 ⊆ On )
21	19 20	mpan2	⊢ ( 𝑦 ⊆ ω → 𝑦 ⊆ On )
22		nnord	⊢ ( 𝑧 ∈ ω → Ord 𝑧 )
23		ssel2	⊢ ( ( 𝑦 ⊆ On ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ∈ On )
24		vex	⊢ 𝑤 ∈ V
25	24	elon	⊢ ( 𝑤 ∈ On ↔ Ord 𝑤 )
26	23 25	sylib	⊢ ( ( 𝑦 ⊆ On ∧ 𝑤 ∈ 𝑦 ) → Ord 𝑤 )
27		ordtri1	⊢ ( ( Ord 𝑤 ∧ Ord 𝑧 ) → ( 𝑤 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑤 ) )
28	26 27	sylan	⊢ ( ( ( 𝑦 ⊆ On ∧ 𝑤 ∈ 𝑦 ) ∧ Ord 𝑧 ) → ( 𝑤 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑤 ) )
29	28	an32s	⊢ ( ( ( 𝑦 ⊆ On ∧ Ord 𝑧 ) ∧ 𝑤 ∈ 𝑦 ) → ( 𝑤 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑤 ) )
30	29	ralbidva	⊢ ( ( 𝑦 ⊆ On ∧ Ord 𝑧 ) → ( ∀ 𝑤 ∈ 𝑦 𝑤 ⊆ 𝑧 ↔ ∀ 𝑤 ∈ 𝑦 ¬ 𝑧 ∈ 𝑤 ) )
31		unissb	⊢ ( ∪ 𝑦 ⊆ 𝑧 ↔ ∀ 𝑤 ∈ 𝑦 𝑤 ⊆ 𝑧 )
32		ralnex	⊢ ( ∀ 𝑤 ∈ 𝑦 ¬ 𝑧 ∈ 𝑤 ↔ ¬ ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 )
33	32	bicomi	⊢ ( ¬ ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 ↔ ∀ 𝑤 ∈ 𝑦 ¬ 𝑧 ∈ 𝑤 )
34	30 31 33	3bitr4g	⊢ ( ( 𝑦 ⊆ On ∧ Ord 𝑧 ) → ( ∪ 𝑦 ⊆ 𝑧 ↔ ¬ ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 ) )
35		ordunisssuc	⊢ ( ( 𝑦 ⊆ On ∧ Ord 𝑧 ) → ( ∪ 𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ suc 𝑧 ) )
36	34 35	bitr3d	⊢ ( ( 𝑦 ⊆ On ∧ Ord 𝑧 ) → ( ¬ ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 ↔ 𝑦 ⊆ suc 𝑧 ) )
37	21 22 36	syl2an	⊢ ( ( 𝑦 ⊆ ω ∧ 𝑧 ∈ ω ) → ( ¬ ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 ↔ 𝑦 ⊆ suc 𝑧 ) )
38		peano2b	⊢ ( 𝑧 ∈ ω ↔ suc 𝑧 ∈ ω )
39		ssnnfi	⊢ ( ( suc 𝑧 ∈ ω ∧ 𝑦 ⊆ suc 𝑧 ) → 𝑦 ∈ Fin )
40	38 39	sylanb	⊢ ( ( 𝑧 ∈ ω ∧ 𝑦 ⊆ suc 𝑧 ) → 𝑦 ∈ Fin )
41	40	ex	⊢ ( 𝑧 ∈ ω → ( 𝑦 ⊆ suc 𝑧 → 𝑦 ∈ Fin ) )
42	41	adantl	⊢ ( ( 𝑦 ⊆ ω ∧ 𝑧 ∈ ω ) → ( 𝑦 ⊆ suc 𝑧 → 𝑦 ∈ Fin ) )
43	37 42	sylbid	⊢ ( ( 𝑦 ⊆ ω ∧ 𝑧 ∈ ω ) → ( ¬ ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ∈ Fin ) )
44	43	rexlimdva	⊢ ( 𝑦 ⊆ ω → ( ∃ 𝑧 ∈ ω ¬ ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ∈ Fin ) )
45	18 44	biimtrrid	⊢ ( 𝑦 ⊆ ω → ( ¬ ∀ 𝑧 ∈ ω ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ∈ Fin ) )
46	45	ad2antll	⊢ ( ( 𝐴 ≺ ω ∧ ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) ) → ( ¬ ∀ 𝑧 ∈ ω ∃ 𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ∈ Fin ) )
47	17 46	mpd	⊢ ( ( 𝐴 ≺ ω ∧ ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) ) → 𝑦 ∈ Fin )
48		simprl	⊢ ( ( 𝐴 ≺ ω ∧ ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) ) → 𝐴 ≈ 𝑦 )
49		enfii	⊢ ( ( 𝑦 ∈ Fin ∧ 𝐴 ≈ 𝑦 ) → 𝐴 ∈ Fin )
50	47 48 49	syl2anc	⊢ ( ( 𝐴 ≺ ω ∧ ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) ) → 𝐴 ∈ Fin )
51	50	ex	⊢ ( 𝐴 ≺ ω → ( ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) → 𝐴 ∈ Fin ) )
52	51	exlimdv	⊢ ( 𝐴 ≺ ω → ( ∃ 𝑦 ( 𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω ) → 𝐴 ∈ Fin ) )
53	5 52	sylcom	⊢ ( ω ∈ V → ( 𝐴 ≺ ω → 𝐴 ∈ Fin ) )
54	2 53	mpcom	⊢ ( 𝐴 ≺ ω → 𝐴 ∈ Fin )