Theorem isfin7-2

Description: A set is VII-finite iff it is non-well-orderable or finite. (Contributed by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	isfin7-2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinVII ↔ ( 𝐴 ∈ dom card → 𝐴 ∈ Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfin7	⊢ ( 𝐴 ∈ FinVII → ( 𝐴 ∈ FinVII ↔ ¬ ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 ) )
2	1	ibi	⊢ ( 𝐴 ∈ FinVII → ¬ ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 )
3		isnum2	⊢ ( 𝐴 ∈ dom card ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 )
4		ensym	⊢ ( 𝑥 ≈ 𝐴 → 𝐴 ≈ 𝑥 )
5		simprl	⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) ) → 𝑥 ∈ On )
6		enfi	⊢ ( 𝐴 ≈ 𝑥 → ( 𝐴 ∈ Fin ↔ 𝑥 ∈ Fin ) )
7		onfin	⊢ ( 𝑥 ∈ On → ( 𝑥 ∈ Fin ↔ 𝑥 ∈ ω ) )
8	6 7	sylan9bbr	⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) → ( 𝐴 ∈ Fin ↔ 𝑥 ∈ ω ) )
9	8	biimprd	⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) → ( 𝑥 ∈ ω → 𝐴 ∈ Fin ) )
10	9	con3d	⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) → ( ¬ 𝐴 ∈ Fin → ¬ 𝑥 ∈ ω ) )
11	10	impcom	⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) ) → ¬ 𝑥 ∈ ω )
12	5 11	eldifd	⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) ) → 𝑥 ∈ ( On ∖ ω ) )
13		simprr	⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) ) → 𝐴 ≈ 𝑥 )
14	12 13	jca	⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) ) → ( 𝑥 ∈ ( On ∖ ω ) ∧ 𝐴 ≈ 𝑥 ) )
15	4 14	sylanr2	⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 ∈ On ∧ 𝑥 ≈ 𝐴 ) ) → ( 𝑥 ∈ ( On ∖ ω ) ∧ 𝐴 ≈ 𝑥 ) )
16	15	ex	⊢ ( ¬ 𝐴 ∈ Fin → ( ( 𝑥 ∈ On ∧ 𝑥 ≈ 𝐴 ) → ( 𝑥 ∈ ( On ∖ ω ) ∧ 𝐴 ≈ 𝑥 ) ) )
17	16	reximdv2	⊢ ( ¬ 𝐴 ∈ Fin → ( ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 → ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 ) )
18	17	com12	⊢ ( ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 → ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 ) )
19	3 18	sylbi	⊢ ( 𝐴 ∈ dom card → ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 ) )
20	19	con1d	⊢ ( 𝐴 ∈ dom card → ( ¬ ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 → 𝐴 ∈ Fin ) )
21	2 20	syl5com	⊢ ( 𝐴 ∈ FinVII → ( 𝐴 ∈ dom card → 𝐴 ∈ Fin ) )
22		eldifi	⊢ ( 𝑥 ∈ ( On ∖ ω ) → 𝑥 ∈ On )
23		ensym	⊢ ( 𝐴 ≈ 𝑥 → 𝑥 ≈ 𝐴 )
24		isnumi	⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ≈ 𝐴 ) → 𝐴 ∈ dom card )
25	22 23 24	syl2an	⊢ ( ( 𝑥 ∈ ( On ∖ ω ) ∧ 𝐴 ≈ 𝑥 ) → 𝐴 ∈ dom card )
26	25	rexlimiva	⊢ ( ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 → 𝐴 ∈ dom card )
27	26	con3i	⊢ ( ¬ 𝐴 ∈ dom card → ¬ ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 )
28		isfin7	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinVII ↔ ¬ ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 ) )
29	27 28	syl5ibr	⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ dom card → 𝐴 ∈ FinVII ) )
30		fin17	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ FinVII )
31	30	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ Fin → 𝐴 ∈ FinVII ) )
32	29 31	jad	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∈ dom card → 𝐴 ∈ Fin ) → 𝐴 ∈ FinVII ) )
33	21 32	impbid2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinVII ↔ ( 𝐴 ∈ dom card → 𝐴 ∈ Fin ) ) )