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	$⊢ A ≺ ω \to A \in Fin$

Proof

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

Metamath Proof Explorer

Theorem isfinite2

Proof