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