Theorem isfin2-2 9141

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

Assertion

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

Distinct variable group:   y, A

Allowed substitution hint:   V( y)

Proof of Theorem isfin2-2

Dummy variables b c m n w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpwi 4168	. . . 4 |- ( y e. ~P ~P A -> y C_ ~P A )
2		fin2i2 9140	. . . . 5 |- ( ( ( A e. FinII /\ y C_ ~P A ) /\ ( y =/= (/) /\ [ C.] Or y ) ) -> |^| y e. y )
3	2	ex 450	. . . 4 |- ( ( A e. FinII /\ y C_ ~P A ) -> ( ( y =/= (/) /\ [ C.] Or y ) -> |^| y e. y ) )
4	1, 3	sylan2 491	. . 3 |- ( ( A e. FinII /\ y e. ~P ~P A ) -> ( ( y =/= (/) /\ [ C.] Or y ) -> |^| y e. y ) )
5	4	ralrimiva 2966	. 2 |- ( A e. FinII -> A. y e. ~P ~P A ( ( y =/= (/) /\ [ C.] Or y ) -> |^| y e. y ) )
6		elpwi 4168	. . . . 5 |- ( b e. ~P ~P A -> b C_ ~P A )
7		simp1r 1086	. . . . . . . 8 |- ( ( ( 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		ssrab2 3687	. . . . . . . . . . 11 |- { c e. ~P A | ( A \ c ) e. b } C_ ~P A
9		simp1l 1085	. . . . . . . . . . . 12 |- ( ( ( 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 )
10		pwexg 4850	. . . . . . . . . . . 12 |- ( A e. V -> ~P A e. _V )
11		elpw2g 4827	. . . . . . . . . . . 12 |- ( ~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 ) )
12	9, 10, 11	3syl 18	. . . . . . . . . . 11 |- ( ( ( 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 ) )
13	8, 12	mpbiri 248	. . . . . . . . . 10 |- ( ( ( 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 )
14		simp2 1062	. . . . . . . . . 10 |- ( ( ( 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 ) )
15		simp3l 1089	. . . . . . . . . . . 12 |- ( ( ( 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 =/= (/) )
16		fin23lem7 9138	. . . . . . . . . . . 12 |- ( ( A e. V /\ b C_ ~P A /\ b =/= (/) ) -> { c e. ~P A | ( A \ c ) e. b } =/= (/) )
17	9, 7, 15, 16	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ( 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 } =/= (/) )
18		sorpsscmpl 6948	. . . . . . . . . . . . 13 |- ( [ C.] Or b -> [ C.] Or { c e. ~P A | ( A \ c ) e. b } )
19	18	adantl 482	. . . . . . . . . . . 12 |- ( ( b =/= (/) /\ [ C.] Or b ) -> [ C.] Or { c e. ~P A | ( A \ c ) e. b } )
20	19	3ad2ant3 1084	. . . . . . . . . . 11 |- ( ( ( 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 } )
21	17, 20	jca 554	. . . . . . . . . 10 |- ( ( ( 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 } ) )
22		neeq1 2856	. . . . . . . . . . . . 13 |- ( y = { c e. ~P A | ( A \ c ) e. b } -> ( y =/= (/) <-> { c e. ~P A | ( A \ c ) e. b } =/= (/) ) )
23		soeq2 5055	. . . . . . . . . . . . 13 |- ( y = { c e. ~P A | ( A \ c ) e. b } -> ( [ C.] Or y <-> [ C.] Or { c e. ~P A | ( A \ c ) e. b } ) )
24	22, 23	anbi12d 747	. . . . . . . . . . . 12 |- ( 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 } ) ) )
25		inteq 4478	. . . . . . . . . . . . 13 |- ( y = { c e. ~P A | ( A \ c ) e. b } -> |^| y = |^| { c e. ~P A | ( A \ c ) e. b } )
26		id 22	. . . . . . . . . . . . 13 |- ( y = { c e. ~P A | ( A \ c ) e. b } -> y = { c e. ~P A | ( A \ c ) e. b } )
27	25, 26	eleq12d 2695	. . . . . . . . . . . 12 |- ( 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 } ) )
28	24, 27	imbi12d 334	. . . . . . . . . . 11 |- ( 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 } ) ) )
29	28	rspcv 3305	. . . . . . . . . 10 |- ( { c e. ~P A | ( A \ c ) e. b } e. ~P ~P A -> ( A. y e. ~P ~P A ( ( 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 } ) ) )
30	13, 14, 21, 29	syl3c 66	. . . . . . . . 9 |- ( ( ( 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 } )
31		sorpssint 6947	. . . . . . . . . 10 |- ( [ 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 } ) )
32	20, 31	syl 17	. . . . . . . . 9 |- ( ( ( 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 } ) )
33	30, 32	mpbird 247	. . . . . . . 8 |- ( ( ( 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 )
34		psseq1 3694	. . . . . . . . 9 |- ( m = ( A \ z ) -> ( m C. n <-> ( A \ z ) C. n ) )
35		psseq1 3694	. . . . . . . . 9 |- ( w = ( A \ n ) -> ( w C. z <-> ( A \ n ) C. z ) )
36		pssdifcom1 4054	. . . . . . . . 9 |- ( ( z C_ A /\ n C_ A ) -> ( ( A \ z ) C. n <-> ( A \ n ) C. z ) )
37	34, 35, 36	fin23lem11 9139	. . . . . . . 8 |- ( 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 ) )
38	7, 33, 37	sylc 65	. . . . . . 7 |- ( ( ( 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 )
39		simp3r 1090	. . . . . . . 8 |- ( ( ( 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 )
40		sorpssuni 6946	. . . . . . . 8 |- ( [ C.] Or b -> ( E. m e. b A. n e. b -. m C. n <-> U. b e. b ) )
41	39, 40	syl 17	. . . . . . 7 |- ( ( ( 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 ) )
42	38, 41	mpbid 222	. . . . . 6 |- ( ( ( 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	42	3exp 1264	. . . . 5 |- ( ( 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 ) ) )
44	6, 43	sylan2 491	. . . 4 |- ( ( 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 ) ) )
45	44	ralrimdva 2969	. . 3 |- ( 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 ) ) )
46		isfin2 9116	. . 3 |- ( A e. V -> ( A e. FinII <-> A. b e. ~P ~P A ( ( b =/= (/) /\ [ C.] Or b ) -> U. b e. b ) ) )
47	45, 46	sylibrd 249	. 2 |- ( A e. V -> ( A. y e. ~P ~P A ( ( y =/= (/) /\ [ C.] Or y ) -> |^| y e. y ) -> A e. FinII ) )
48	5, 47	impbid2 216	1 |- ( A e. V -> ( A e. FinII <-> A. y e. ~P ~P A ( ( y =/= (/) /\ [ C.] Or y ) -> |^| y e. y ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   C_ wss 3574   C. wpss 3575   (/)c0 3915   ~Pcpw 4158   U.cuni 4436   |^|cint 4475   Or wor 5034   [ C.] crpss 6936  Fin^IIcfin2 9101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-int 4476  df-br 4654  df-opab 4713  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-rpss 6937  df-fin2 9108

This theorem is referenced by: (None)