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

Metamath Proof Explorer

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 imbitrrid 
 |-  ( 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 ) ) )