Metamath Proof Explorer

Theorem fin2i2

Description: A II-finite set contains minimal elements for every nonempty chain. (Contributed by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion fin2i2 
|- ( ( ( A e. Fin2 /\ B C_ ~P A ) /\ ( B =/= (/) /\ [C.] Or B ) ) -> |^| B e. B )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( A e. Fin2 /\ B C_ ~P A ) /\ ( B =/= (/) /\ [C.] Or B ) ) -> B C_ ~P A )
2 simpll 
 |-  ( ( ( A e. Fin2 /\ B C_ ~P A ) /\ ( B =/= (/) /\ [C.] Or B ) ) -> A e. Fin2 )
3 ssrab2 
 |-  { c e. ~P A | ( A \ c ) e. B } C_ ~P A
4 3 a1i 
 |-  ( ( ( A e. Fin2 /\ B C_ ~P A ) /\ ( B =/= (/) /\ [C.] Or B ) ) -> { c e. ~P A | ( A \ c ) e. B } C_ ~P A )
5 simprl 
 |-  ( ( ( A e. Fin2 /\ B C_ ~P A ) /\ ( B =/= (/) /\ [C.] Or B ) ) -> B =/= (/) )
6 fin23lem7 
 |-  ( ( A e. Fin2 /\ B C_ ~P A /\ B =/= (/) ) -> { c e. ~P A | ( A \ c ) e. B } =/= (/) )
7 2 1 5 6 syl3anc 
 |-  ( ( ( A e. Fin2 /\ B C_ ~P A ) /\ ( B =/= (/) /\ [C.] Or B ) ) -> { c e. ~P A | ( A \ c ) e. B } =/= (/) )
8 sorpsscmpl 
 |-  ( [C.] Or B -> [C.] Or { c e. ~P A | ( A \ c ) e. B } )
9 8 ad2antll 
 |-  ( ( ( A e. Fin2 /\ B C_ ~P A ) /\ ( B =/= (/) /\ [C.] Or B ) ) -> [C.] Or { c e. ~P A | ( A \ c ) e. B } )
10 fin2i 
 |-  ( ( ( A e. Fin2 /\ { c e. ~P A | ( A \ c ) e. B } C_ ~P A ) /\ ( { c e. ~P A | ( A \ c ) e. B } =/= (/) /\ [C.] Or { c e. ~P A | ( A \ c ) e. B } ) ) -> U. { c e. ~P A | ( A \ c ) e. B } e. { c e. ~P A | ( A \ c ) e. B } )
11 2 4 7 9 10 syl22anc 
 |-  ( ( ( A e. Fin2 /\ B C_ ~P A ) /\ ( B =/= (/) /\ [C.] Or B ) ) -> U. { c e. ~P A | ( A \ c ) e. B } e. { c e. ~P A | ( A \ c ) e. B } )
12 sorpssuni 
 |-  ( [C.] Or { c e. ~P A | ( A \ c ) e. B } -> ( E. m e. { c e. ~P A | ( A \ c ) e. B } A. n e. { c e. ~P A | ( A \ c ) e. B } -. m C. n <-> U. { c e. ~P A | ( A \ c ) e. B } e. { c e. ~P A | ( A \ c ) e. B } ) )
13 9 12 syl 
 |-  ( ( ( A e. Fin2 /\ B C_ ~P A ) /\ ( B =/= (/) /\ [C.] Or B ) ) -> ( E. m e. { c e. ~P A | ( A \ c ) e. B } A. n e. { c e. ~P A | ( A \ c ) e. B } -. m C. n <-> U. { c e. ~P A | ( A \ c ) e. B } e. { c e. ~P A | ( A \ c ) e. B } ) )
14 11 13 mpbird 
 |-  ( ( ( A e. Fin2 /\ B C_ ~P A ) /\ ( B =/= (/) /\ [C.] Or B ) ) -> E. m e. { c e. ~P A | ( A \ c ) e. B } A. n e. { c e. ~P A | ( A \ c ) e. B } -. m C. n )
15 psseq2 
 |-  ( z = ( A \ m ) -> ( w C. z <-> w C. ( A \ m ) ) )
16 psseq2 
 |-  ( n = ( A \ w ) -> ( m C. n <-> m C. ( A \ w ) ) )
17 pssdifcom2 
 |-  ( ( m C_ A /\ w C_ A ) -> ( w C. ( A \ m ) <-> m C. ( A \ w ) ) )
18 15 16 17 fin23lem11 
 |-  ( B C_ ~P A -> ( E. m e. { c e. ~P A | ( A \ c ) e. B } A. n e. { c e. ~P A | ( A \ c ) e. B } -. m C. n -> E. z e. B A. w e. B -. w C. z ) )
19 1 14 18 sylc 
 |-  ( ( ( A e. Fin2 /\ B C_ ~P A ) /\ ( B =/= (/) /\ [C.] Or B ) ) -> E. z e. B A. w e. B -. w C. z )
20 sorpssint 
 |-  ( [C.] Or B -> ( E. z e. B A. w e. B -. w C. z <-> |^| B e. B ) )
21 20 ad2antll 
 |-  ( ( ( A e. Fin2 /\ B C_ ~P A ) /\ ( B =/= (/) /\ [C.] Or B ) ) -> ( E. z e. B A. w e. B -. w C. z <-> |^| B e. B ) )
22 19 21 mpbid 
 |-  ( ( ( A e. Fin2 /\ B C_ ~P A ) /\ ( B =/= (/) /\ [C.] Or B ) ) -> |^| B e. B )