Metamath Proof Explorer

Theorem fin67

Description: Every VI-finite set is VII-finite. (Contributed by Stefan O'Rear, 29-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin67 ⊢ A ∈ FinVI → A ∈ FinVII

Proof

Step Hyp Ref Expression
1 isfin6 ⊢ A ∈ FinVI ↔ A ≺ 2 𝑜 ∨ A ≺ A × A
2 2onn ⊢ 2 𝑜 ∈ ω
3 ssid ⊢ 2 𝑜 ⊆ 2 𝑜
4 ssnnfi ⊢ 2 𝑜 ∈ ω ∧ 2 𝑜 ⊆ 2 𝑜 → 2 𝑜 ∈ Fin
5 2 3 4 mp2an ⊢ 2 𝑜 ∈ Fin
6 sdomdom ⊢ A ≺ 2 𝑜 → A ≼ 2 𝑜
7 domfi ⊢ 2 𝑜 ∈ Fin ∧ A ≼ 2 𝑜 → A ∈ Fin
8 5 6 7 sylancr ⊢ A ≺ 2 𝑜 → A ∈ Fin
9 fin17 ⊢ A ∈ Fin → A ∈ FinVII
10 8 9 syl ⊢ A ≺ 2 𝑜 → A ∈ FinVII
11 sdomnen ⊢ A ≺ A × A → ¬ A ≈ A × A
12 eldifi ⊢ b ∈ On ∖ ω → b ∈ On
13 ensym ⊢ A ≈ b → b ≈ A
14 isnumi ⊢ b ∈ On ∧ b ≈ A → A ∈ dom ⁡ card
15 12 13 14 syl2an ⊢ b ∈ On ∖ ω ∧ A ≈ b → A ∈ dom ⁡ card
16 vex ⊢ b ∈ V
17 eldif ⊢ b ∈ On ∖ ω ↔ b ∈ On ∧ ¬ b ∈ ω
18 ordom ⊢ Ord ⁡ ω
19 eloni ⊢ b ∈ On → Ord ⁡ b
20 ordtri1 ⊢ Ord ⁡ ω ∧ Ord ⁡ b → ω ⊆ b ↔ ¬ b ∈ ω
21 18 19 20 sylancr ⊢ b ∈ On → ω ⊆ b ↔ ¬ b ∈ ω
22 21 biimpar ⊢ b ∈ On ∧ ¬ b ∈ ω → ω ⊆ b
23 17 22 sylbi ⊢ b ∈ On ∖ ω → ω ⊆ b
24 ssdomg ⊢ b ∈ V → ω ⊆ b → ω ≼ b
25 16 23 24 mpsyl ⊢ b ∈ On ∖ ω → ω ≼ b
26 domen2 ⊢ A ≈ b → ω ≼ A ↔ ω ≼ b
27 25 26 imbitrrid ⊢ A ≈ b → b ∈ On ∖ ω → ω ≼ A
28 27 impcom ⊢ b ∈ On ∖ ω ∧ A ≈ b → ω ≼ A
29 infxpidm2 ⊢ A ∈ dom ⁡ card ∧ ω ≼ A → A × A ≈ A
30 15 28 29 syl2anc ⊢ b ∈ On ∖ ω ∧ A ≈ b → A × A ≈ A
31 ensym ⊢ A × A ≈ A → A ≈ A × A
32 30 31 syl ⊢ b ∈ On ∖ ω ∧ A ≈ b → A ≈ A × A
33 32 rexlimiva ⊢ ∃ b ∈ On ∖ ω A ≈ b → A ≈ A × A
34 11 33 nsyl ⊢ A ≺ A × A → ¬ ∃ b ∈ On ∖ ω A ≈ b
35 relsdom ⊢ Rel ⁡ ≺
36 35 brrelex1i ⊢ A ≺ A × A → A ∈ V
37 isfin7 ⊢ A ∈ V → A ∈ FinVII ↔ ¬ ∃ b ∈ On ∖ ω A ≈ b
38 36 37 syl ⊢ A ≺ A × A → A ∈ FinVII ↔ ¬ ∃ b ∈ On ∖ ω A ≈ b
39 34 38 mpbird ⊢ A ≺ A × A → A ∈ FinVII
40 10 39 jaoi ⊢ A ≺ 2 𝑜 ∨ A ≺ A × A → A ∈ FinVII
41 1 40 sylbi ⊢ A ∈ FinVI → A ∈ FinVII