This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )