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	⊢ ( 𝐴 ∈ FinVI → 𝐴 ∈ FinVII )

Proof

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