Metamath Proof Explorer


Theorem isfin1-3

Description: A set is I-finite iff every system of subsets contains a maximal subset. Definition I of Levy58 p. 2. (Contributed by Stefan O'Rear, 4-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion isfin1-3
|- ( A e. V -> ( A e. Fin <-> `' [C.] Fr ~P A ) )

Proof

Step Hyp Ref Expression
1 porpss
 |-  [C.] Po ~P A
2 cnvpo
 |-  ( [C.] Po ~P A <-> `' [C.] Po ~P A )
3 1 2 mpbi
 |-  `' [C.] Po ~P A
4 pwfi
 |-  ( A e. Fin <-> ~P A e. Fin )
5 4 biimpi
 |-  ( A e. Fin -> ~P A e. Fin )
6 frfi
 |-  ( ( `' [C.] Po ~P A /\ ~P A e. Fin ) -> `' [C.] Fr ~P A )
7 3 5 6 sylancr
 |-  ( A e. Fin -> `' [C.] Fr ~P A )
8 inss2
 |-  ( Fin i^i ~P A ) C_ ~P A
9 pwexg
 |-  ( A e. V -> ~P A e. _V )
10 ssexg
 |-  ( ( ( Fin i^i ~P A ) C_ ~P A /\ ~P A e. _V ) -> ( Fin i^i ~P A ) e. _V )
11 8 9 10 sylancr
 |-  ( A e. V -> ( Fin i^i ~P A ) e. _V )
12 0fin
 |-  (/) e. Fin
13 0elpw
 |-  (/) e. ~P A
14 12 13 elini
 |-  (/) e. ( Fin i^i ~P A )
15 14 ne0ii
 |-  ( Fin i^i ~P A ) =/= (/)
16 fri
 |-  ( ( ( ( Fin i^i ~P A ) e. _V /\ `' [C.] Fr ~P A ) /\ ( ( Fin i^i ~P A ) C_ ~P A /\ ( Fin i^i ~P A ) =/= (/) ) ) -> E. b e. ( Fin i^i ~P A ) A. c e. ( Fin i^i ~P A ) -. c `' [C.] b )
17 8 15 16 mpanr12
 |-  ( ( ( Fin i^i ~P A ) e. _V /\ `' [C.] Fr ~P A ) -> E. b e. ( Fin i^i ~P A ) A. c e. ( Fin i^i ~P A ) -. c `' [C.] b )
18 11 17 sylan
 |-  ( ( A e. V /\ `' [C.] Fr ~P A ) -> E. b e. ( Fin i^i ~P A ) A. c e. ( Fin i^i ~P A ) -. c `' [C.] b )
19 18 ex
 |-  ( A e. V -> ( `' [C.] Fr ~P A -> E. b e. ( Fin i^i ~P A ) A. c e. ( Fin i^i ~P A ) -. c `' [C.] b ) )
20 elinel1
 |-  ( b e. ( Fin i^i ~P A ) -> b e. Fin )
21 ralnex
 |-  ( A. c e. ( Fin i^i ~P A ) -. c `' [C.] b <-> -. E. c e. ( Fin i^i ~P A ) c `' [C.] b )
22 20 adantr
 |-  ( ( b e. ( Fin i^i ~P A ) /\ ( d e. A /\ -. d e. b ) ) -> b e. Fin )
23 snfi
 |-  { d } e. Fin
24 unfi
 |-  ( ( b e. Fin /\ { d } e. Fin ) -> ( b u. { d } ) e. Fin )
25 22 23 24 sylancl
 |-  ( ( b e. ( Fin i^i ~P A ) /\ ( d e. A /\ -. d e. b ) ) -> ( b u. { d } ) e. Fin )
26 elinel2
 |-  ( b e. ( Fin i^i ~P A ) -> b e. ~P A )
27 26 elpwid
 |-  ( b e. ( Fin i^i ~P A ) -> b C_ A )
28 27 adantr
 |-  ( ( b e. ( Fin i^i ~P A ) /\ ( d e. A /\ -. d e. b ) ) -> b C_ A )
29 snssi
 |-  ( d e. A -> { d } C_ A )
30 29 ad2antrl
 |-  ( ( b e. ( Fin i^i ~P A ) /\ ( d e. A /\ -. d e. b ) ) -> { d } C_ A )
31 28 30 unssd
 |-  ( ( b e. ( Fin i^i ~P A ) /\ ( d e. A /\ -. d e. b ) ) -> ( b u. { d } ) C_ A )
32 vex
 |-  b e. _V
33 snex
 |-  { d } e. _V
34 32 33 unex
 |-  ( b u. { d } ) e. _V
35 34 elpw
 |-  ( ( b u. { d } ) e. ~P A <-> ( b u. { d } ) C_ A )
36 31 35 sylibr
 |-  ( ( b e. ( Fin i^i ~P A ) /\ ( d e. A /\ -. d e. b ) ) -> ( b u. { d } ) e. ~P A )
37 25 36 elind
 |-  ( ( b e. ( Fin i^i ~P A ) /\ ( d e. A /\ -. d e. b ) ) -> ( b u. { d } ) e. ( Fin i^i ~P A ) )
38 disjsn
 |-  ( ( b i^i { d } ) = (/) <-> -. d e. b )
39 38 biimpri
 |-  ( -. d e. b -> ( b i^i { d } ) = (/) )
40 vex
 |-  d e. _V
41 40 snnz
 |-  { d } =/= (/)
42 disjpss
 |-  ( ( ( b i^i { d } ) = (/) /\ { d } =/= (/) ) -> b C. ( b u. { d } ) )
43 39 41 42 sylancl
 |-  ( -. d e. b -> b C. ( b u. { d } ) )
44 43 ad2antll
 |-  ( ( b e. ( Fin i^i ~P A ) /\ ( d e. A /\ -. d e. b ) ) -> b C. ( b u. { d } ) )
45 34 32 brcnv
 |-  ( ( b u. { d } ) `' [C.] b <-> b [C.] ( b u. { d } ) )
46 34 brrpss
 |-  ( b [C.] ( b u. { d } ) <-> b C. ( b u. { d } ) )
47 45 46 bitri
 |-  ( ( b u. { d } ) `' [C.] b <-> b C. ( b u. { d } ) )
48 44 47 sylibr
 |-  ( ( b e. ( Fin i^i ~P A ) /\ ( d e. A /\ -. d e. b ) ) -> ( b u. { d } ) `' [C.] b )
49 breq1
 |-  ( c = ( b u. { d } ) -> ( c `' [C.] b <-> ( b u. { d } ) `' [C.] b ) )
50 49 rspcev
 |-  ( ( ( b u. { d } ) e. ( Fin i^i ~P A ) /\ ( b u. { d } ) `' [C.] b ) -> E. c e. ( Fin i^i ~P A ) c `' [C.] b )
51 37 48 50 syl2anc
 |-  ( ( b e. ( Fin i^i ~P A ) /\ ( d e. A /\ -. d e. b ) ) -> E. c e. ( Fin i^i ~P A ) c `' [C.] b )
52 51 expr
 |-  ( ( b e. ( Fin i^i ~P A ) /\ d e. A ) -> ( -. d e. b -> E. c e. ( Fin i^i ~P A ) c `' [C.] b ) )
53 52 con1d
 |-  ( ( b e. ( Fin i^i ~P A ) /\ d e. A ) -> ( -. E. c e. ( Fin i^i ~P A ) c `' [C.] b -> d e. b ) )
54 21 53 syl5bi
 |-  ( ( b e. ( Fin i^i ~P A ) /\ d e. A ) -> ( A. c e. ( Fin i^i ~P A ) -. c `' [C.] b -> d e. b ) )
55 54 impancom
 |-  ( ( b e. ( Fin i^i ~P A ) /\ A. c e. ( Fin i^i ~P A ) -. c `' [C.] b ) -> ( d e. A -> d e. b ) )
56 55 ssrdv
 |-  ( ( b e. ( Fin i^i ~P A ) /\ A. c e. ( Fin i^i ~P A ) -. c `' [C.] b ) -> A C_ b )
57 ssfi
 |-  ( ( b e. Fin /\ A C_ b ) -> A e. Fin )
58 20 56 57 syl2an2r
 |-  ( ( b e. ( Fin i^i ~P A ) /\ A. c e. ( Fin i^i ~P A ) -. c `' [C.] b ) -> A e. Fin )
59 58 rexlimiva
 |-  ( E. b e. ( Fin i^i ~P A ) A. c e. ( Fin i^i ~P A ) -. c `' [C.] b -> A e. Fin )
60 19 59 syl6
 |-  ( A e. V -> ( `' [C.] Fr ~P A -> A e. Fin ) )
61 7 60 impbid2
 |-  ( A e. V -> ( A e. Fin <-> `' [C.] Fr ~P A ) )