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	|- ( A e. V -> ( A e. Fin7 <-> ( A e. dom card -> A e. Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfin7	|- ( A e. Fin7 -> ( A e. Fin7 <-> -. E. x e. ( On \ _om ) A ~~ x ) )
2	1	ibi	|- ( A e. Fin7 -> -. E. x e. ( On \ _om ) A ~~ x )
3		isnum2	|- ( A e. dom card <-> E. x e. On x ~~ A )
4		ensym	|- ( x ~~ A -> A ~~ x )
5		simprl	|- ( ( -. A e. Fin /\ ( x e. On /\ A ~~ x ) ) -> x e. On )
6		enfi	|- ( A ~~ x -> ( A e. Fin <-> x e. Fin ) )
7		onfin	|- ( x e. On -> ( x e. Fin <-> x e. _om ) )
8	6 7	sylan9bbr	|- ( ( x e. On /\ A ~~ x ) -> ( A e. Fin <-> x e. _om ) )
9	8	biimprd	|- ( ( x e. On /\ A ~~ x ) -> ( x e. _om -> A e. Fin ) )
10	9	con3d	|- ( ( x e. On /\ A ~~ x ) -> ( -. A e. Fin -> -. x e. _om ) )
11	10	impcom	|- ( ( -. A e. Fin /\ ( x e. On /\ A ~~ x ) ) -> -. x e. _om )
12	5 11	eldifd	|- ( ( -. A e. Fin /\ ( x e. On /\ A ~~ x ) ) -> x e. ( On \ _om ) )
13		simprr	|- ( ( -. A e. Fin /\ ( x e. On /\ A ~~ x ) ) -> A ~~ x )
14	12 13	jca	|- ( ( -. A e. Fin /\ ( x e. On /\ A ~~ x ) ) -> ( x e. ( On \ _om ) /\ A ~~ x ) )
15	4 14	sylanr2	|- ( ( -. A e. Fin /\ ( x e. On /\ x ~~ A ) ) -> ( x e. ( On \ _om ) /\ A ~~ x ) )
16	15	ex	|- ( -. A e. Fin -> ( ( x e. On /\ x ~~ A ) -> ( x e. ( On \ _om ) /\ A ~~ x ) ) )
17	16	reximdv2	|- ( -. A e. Fin -> ( E. x e. On x ~~ A -> E. x e. ( On \ _om ) A ~~ x ) )
18	17	com12	|- ( E. x e. On x ~~ A -> ( -. A e. Fin -> E. x e. ( On \ _om ) A ~~ x ) )
19	3 18	sylbi	|- ( A e. dom card -> ( -. A e. Fin -> E. x e. ( On \ _om ) A ~~ x ) )
20	19	con1d	|- ( A e. dom card -> ( -. E. x e. ( On \ _om ) A ~~ x -> A e. Fin ) )
21	2 20	syl5com	|- ( A e. Fin7 -> ( A e. dom card -> A e. Fin ) )
22		eldifi	|- ( x e. ( On \ _om ) -> x e. On )
23		ensym	|- ( A ~~ x -> x ~~ A )
24		isnumi	|- ( ( x e. On /\ x ~~ A ) -> A e. dom card )
25	22 23 24	syl2an	|- ( ( x e. ( On \ _om ) /\ A ~~ x ) -> A e. dom card )
26	25	rexlimiva	|- ( E. x e. ( On \ _om ) A ~~ x -> A e. dom card )
27	26	con3i	|- ( -. A e. dom card -> -. E. x e. ( On \ _om ) A ~~ x )
28		isfin7	|- ( A e. V -> ( A e. Fin7 <-> -. E. x e. ( On \ _om ) A ~~ x ) )
29	27 28	syl5ibr	|- ( A e. V -> ( -. A e. dom card -> A e. Fin7 ) )
30		fin17	|- ( A e. Fin -> A e. Fin7 )
31	30	a1i	|- ( A e. V -> ( A e. Fin -> A e. Fin7 ) )
32	29 31	jad	|- ( A e. V -> ( ( A e. dom card -> A e. Fin ) -> A e. Fin7 ) )
33	21 32	impbid2	|- ( A e. V -> ( A e. Fin7 <-> ( A e. dom card -> A e. Fin ) ) )