Metamath Proof Explorer

Theorem isfin2-2

Description: Fin2 expressed in terms of minimal elements. (Contributed by Stefan O'Rear, 2-Nov-2014) (Proof shortened by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion isfin2-2 
|- ( A e. V -> ( A e. Fin2 <-> A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) ) )

Proof

Step Hyp Ref Expression
1 elpwi 
 |-  ( y e. ~P ~P A -> y C_ ~P A )
2 fin2i2 
 |-  ( ( ( A e. Fin2 /\ y C_ ~P A ) /\ ( y =/= (/) /\ [C.] Or y ) ) -> |^| y e. y )
3 2 ex 
 |-  ( ( A e. Fin2 /\ y C_ ~P A ) -> ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) )
4 1 3 sylan2 
 |-  ( ( A e. Fin2 /\ y e. ~P ~P A ) -> ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) )
5 4 ralrimiva 
 |-  ( A e. Fin2 -> A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) )
6 elpwi 
 |-  ( b e. ~P ~P A -> b C_ ~P A )
7 simp1r 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> b C_ ~P A )
8 simp1l 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> A e. V )
9 simp3l 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> b =/= (/) )
10 fin23lem7 
 |-  ( ( A e. V /\ b C_ ~P A /\ b =/= (/) ) -> { c e. ~P A | ( A \ c ) e. b } =/= (/) )
11 8 7 9 10 syl3anc 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> { c e. ~P A | ( A \ c ) e. b } =/= (/) )
12 sorpsscmpl 
 |-  ( [C.] Or b -> [C.] Or { c e. ~P A | ( A \ c ) e. b } )
13 12 adantl 
 |-  ( ( b =/= (/) /\ [C.] Or b ) -> [C.] Or { c e. ~P A | ( A \ c ) e. b } )
14 13 3ad2ant3 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> [C.] Or { c e. ~P A | ( A \ c ) e. b } )
15 neeq1 
 |-  ( y = { c e. ~P A | ( A \ c ) e. b } -> ( y =/= (/) <-> { c e. ~P A | ( A \ c ) e. b } =/= (/) ) )
16 soeq2 
 |-  ( y = { c e. ~P A | ( A \ c ) e. b } -> ( [C.] Or y <-> [C.] Or { c e. ~P A | ( A \ c ) e. b } ) )
17 15 16 anbi12d 
 |-  ( y = { c e. ~P A | ( A \ c ) e. b } -> ( ( y =/= (/) /\ [C.] Or y ) <-> ( { c e. ~P A | ( A \ c ) e. b } =/= (/) /\ [C.] Or { c e. ~P A | ( A \ c ) e. b } ) ) )
18 inteq 
 |-  ( y = { c e. ~P A | ( A \ c ) e. b } -> |^| y = |^| { c e. ~P A | ( A \ c ) e. b } )
19 id 
 |-  ( y = { c e. ~P A | ( A \ c ) e. b } -> y = { c e. ~P A | ( A \ c ) e. b } )
20 18 19 eleq12d 
 |-  ( y = { c e. ~P A | ( A \ c ) e. b } -> ( |^| y e. y <-> |^| { c e. ~P A | ( A \ c ) e. b } e. { c e. ~P A | ( A \ c ) e. b } ) )
21 17 20 imbi12d 
 |-  ( y = { c e. ~P A | ( A \ c ) e. b } -> ( ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) <-> ( ( { c e. ~P A | ( A \ c ) e. b } =/= (/) /\ [C.] Or { c e. ~P A | ( A \ c ) e. b } ) -> |^| { c e. ~P A | ( A \ c ) e. b } e. { c e. ~P A | ( A \ c ) e. b } ) ) )
22 simp2 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) )
23 ssrab2 
 |-  { c e. ~P A | ( A \ c ) e. b } C_ ~P A
24 pwexg 
 |-  ( A e. V -> ~P A e. _V )
25 elpw2g 
 |-  ( ~P A e. _V -> ( { c e. ~P A | ( A \ c ) e. b } e. ~P ~P A <-> { c e. ~P A | ( A \ c ) e. b } C_ ~P A ) )
26 8 24 25 3syl 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> ( { c e. ~P A | ( A \ c ) e. b } e. ~P ~P A <-> { c e. ~P A | ( A \ c ) e. b } C_ ~P A ) )
27 23 26 mpbiri 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> { c e. ~P A | ( A \ c ) e. b } e. ~P ~P A )
28 21 22 27 rspcdva 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> ( ( { c e. ~P A | ( A \ c ) e. b } =/= (/) /\ [C.] Or { c e. ~P A | ( A \ c ) e. b } ) -> |^| { c e. ~P A | ( A \ c ) e. b } e. { c e. ~P A | ( A \ c ) e. b } ) )
29 11 14 28 mp2and 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> |^| { c e. ~P A | ( A \ c ) e. b } e. { c e. ~P A | ( A \ c ) e. b } )
30 sorpssint 
 |-  ( [C.] Or { c e. ~P A | ( A \ c ) e. b } -> ( E. z e. { c e. ~P A | ( A \ c ) e. b } A. w e. { c e. ~P A | ( A \ c ) e. b } -. w C. z <-> |^| { c e. ~P A | ( A \ c ) e. b } e. { c e. ~P A | ( A \ c ) e. b } ) )
31 14 30 syl 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> ( E. z e. { c e. ~P A | ( A \ c ) e. b } A. w e. { c e. ~P A | ( A \ c ) e. b } -. w C. z <-> |^| { c e. ~P A | ( A \ c ) e. b } e. { c e. ~P A | ( A \ c ) e. b } ) )
32 29 31 mpbird 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> E. z e. { c e. ~P A | ( A \ c ) e. b } A. w e. { c e. ~P A | ( A \ c ) e. b } -. w C. z )
33 psseq1 
 |-  ( m = ( A \ z ) -> ( m C. n <-> ( A \ z ) C. n ) )
34 psseq1 
 |-  ( w = ( A \ n ) -> ( w C. z <-> ( A \ n ) C. z ) )
35 pssdifcom1 
 |-  ( ( z C_ A /\ n C_ A ) -> ( ( A \ z ) C. n <-> ( A \ n ) C. z ) )
36 33 34 35 fin23lem11 
 |-  ( b C_ ~P A -> ( E. z e. { c e. ~P A | ( A \ c ) e. b } A. w e. { c e. ~P A | ( A \ c ) e. b } -. w C. z -> E. m e. b A. n e. b -. m C. n ) )
37 7 32 36 sylc 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> E. m e. b A. n e. b -. m C. n )
38 simp3r 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> [C.] Or b )
39 sorpssuni 
 |-  ( [C.] Or b -> ( E. m e. b A. n e. b -. m C. n <-> U. b e. b ) )
40 38 39 syl 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> ( E. m e. b A. n e. b -. m C. n <-> U. b e. b ) )
41 37 40 mpbid 
 |-  ( ( ( A e. V /\ b C_ ~P A ) /\ A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> U. b e. b )
42 41 3exp 
 |-  ( ( A e. V /\ b C_ ~P A ) -> ( A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) -> ( ( b =/= (/) /\ [C.] Or b ) -> U. b e. b ) ) )
43 6 42 sylan2 
 |-  ( ( A e. V /\ b e. ~P ~P A ) -> ( A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) -> ( ( b =/= (/) /\ [C.] Or b ) -> U. b e. b ) ) )
44 43 ralrimdva 
 |-  ( A e. V -> ( A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) -> A. b e. ~P ~P A ( ( b =/= (/) /\ [C.] Or b ) -> U. b e. b ) ) )
45 isfin2 
 |-  ( A e. V -> ( A e. Fin2 <-> A. b e. ~P ~P A ( ( b =/= (/) /\ [C.] Or b ) -> U. b e. b ) ) )
46 44 45 sylibrd 
 |-  ( A e. V -> ( A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) -> A e. Fin2 ) )
47 5 46 impbid2 
 |-  ( A e. V -> ( A e. Fin2 <-> A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> |^| y e. y ) ) )