MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fin1a2lem12 Structured version   Visualization version   Unicode version

Theorem fin1a2lem12 8867
Description: Lemma for fin1a2 8871. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
Assertion
Ref Expression
fin1a2lem12  |-  ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  ->  -.  B  e. FinIII )

Proof of Theorem fin1a2lem12
Dummy variables  d 
e  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 467 . . 3  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  B  e. FinIII )
2 simpll1 1053 . . . . . . 7  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  A  C_ 
~P B )
32adantr 471 . . . . . 6  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  /\  e  e.  om )  ->  A  C_ 
~P B )
4 ssrab2 3526 . . . . . . . 8  |-  { f  e.  A  |  f  ~<_  e }  C_  A
54unissi 4235 . . . . . . 7  |-  U. {
f  e.  A  | 
f  ~<_  e }  C_  U. A
6 sspwuni 4381 . . . . . . . 8  |-  ( A 
C_  ~P B  <->  U. A  C_  B )
76biimpi 199 . . . . . . 7  |-  ( A 
C_  ~P B  ->  U. A  C_  B )
85, 7syl5ss 3455 . . . . . 6  |-  ( A 
C_  ~P B  ->  U. {
f  e.  A  | 
f  ~<_  e }  C_  B )
93, 8syl 17 . . . . 5  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  /\  e  e.  om )  ->  U. {
f  e.  A  | 
f  ~<_  e }  C_  B )
10 elpw2g 4580 . . . . . 6  |-  ( B  e. FinIII  ->  ( U. {
f  e.  A  | 
f  ~<_  e }  e.  ~P B  <->  U. { f  e.  A  |  f  ~<_  e }  C_  B )
)
1110ad2antlr 738 . . . . 5  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  /\  e  e.  om )  ->  ( U. { f  e.  A  |  f  ~<_  e }  e.  ~P B  <->  U. { f  e.  A  |  f  ~<_  e }  C_  B
) )
129, 11mpbird 240 . . . 4  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  /\  e  e.  om )  ->  U. {
f  e.  A  | 
f  ~<_  e }  e.  ~P B )
13 eqid 2462 . . . 4  |-  ( e  e.  om  |->  U. {
f  e.  A  | 
f  ~<_  e } )  =  ( e  e. 
om  |->  U. { f  e.  A  |  f  ~<_  e } )
1412, 13fmptd 6069 . . 3  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  (
e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
) : om --> ~P B
)
15 vex 3060 . . . . . . . . . . 11  |-  d  e. 
_V
1615sucex 6665 . . . . . . . . . 10  |-  suc  d  e.  _V
17 sssucid 5519 . . . . . . . . . 10  |-  d  C_  suc  d
18 ssdomg 7641 . . . . . . . . . 10  |-  ( suc  d  e.  _V  ->  ( d  C_  suc  d  -> 
d  ~<_  suc  d )
)
1916, 17, 18mp2 9 . . . . . . . . 9  |-  d  ~<_  suc  d
20 domtr 7648 . . . . . . . . 9  |-  ( ( f  ~<_  d  /\  d  ~<_  suc  d )  ->  f  ~<_  suc  d )
2119, 20mpan2 682 . . . . . . . 8  |-  ( f  ~<_  d  ->  f  ~<_  suc  d
)
2221a1i 11 . . . . . . 7  |-  ( f  e.  A  ->  (
f  ~<_  d  ->  f  ~<_  suc  d ) )
2322ss2rabi 3523 . . . . . 6  |-  { f  e.  A  |  f  ~<_  d }  C_  { f  e.  A  |  f  ~<_  suc  d }
24 uniss 4233 . . . . . 6  |-  ( { f  e.  A  | 
f  ~<_  d }  C_  { f  e.  A  | 
f  ~<_  suc  d }  ->  U. { f  e.  A  |  f  ~<_  d }  C_  U. { f  e.  A  |  f  ~<_  suc  d } )
2523, 24mp1i 13 . . . . 5  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  /\  d  e.  om )  ->  U. {
f  e.  A  | 
f  ~<_  d }  C_  U. { f  e.  A  |  f  ~<_  suc  d } )
26 id 22 . . . . . 6  |-  ( d  e.  om  ->  d  e.  om )
27 pwexg 4601 . . . . . . . . 9  |-  ( B  e. FinIII  ->  ~P B  e. 
_V )
2827adantl 472 . . . . . . . 8  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  ~P B  e.  _V )
2928, 2ssexd 4564 . . . . . . 7  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  A  e.  _V )
30 rabexg 4567 . . . . . . 7  |-  ( A  e.  _V  ->  { f  e.  A  |  f  ~<_  d }  e.  _V )
31 uniexg 6615 . . . . . . 7  |-  ( { f  e.  A  | 
f  ~<_  d }  e.  _V  ->  U. { f  e.  A  |  f  ~<_  d }  e.  _V )
3229, 30, 313syl 18 . . . . . 6  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  U. {
f  e.  A  | 
f  ~<_  d }  e.  _V )
33 breq2 4420 . . . . . . . . 9  |-  ( e  =  d  ->  (
f  ~<_  e  <->  f  ~<_  d ) )
3433rabbidv 3048 . . . . . . . 8  |-  ( e  =  d  ->  { f  e.  A  |  f  ~<_  e }  =  {
f  e.  A  | 
f  ~<_  d } )
3534unieqd 4222 . . . . . . 7  |-  ( e  =  d  ->  U. {
f  e.  A  | 
f  ~<_  e }  =  U. { f  e.  A  |  f  ~<_  d }
)
3635, 13fvmptg 5969 . . . . . 6  |-  ( ( d  e.  om  /\  U. { f  e.  A  |  f  ~<_  d }  e.  _V )  ->  (
( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
) `  d )  =  U. { f  e.  A  |  f  ~<_  d } )
3726, 32, 36syl2anr 485 . . . . 5  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  /\  d  e.  om )  ->  (
( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
) `  d )  =  U. { f  e.  A  |  f  ~<_  d } )
38 peano2 6740 . . . . . 6  |-  ( d  e.  om  ->  suc  d  e.  om )
39 rabexg 4567 . . . . . . 7  |-  ( A  e.  _V  ->  { f  e.  A  |  f  ~<_  suc  d }  e.  _V )
40 uniexg 6615 . . . . . . 7  |-  ( { f  e.  A  | 
f  ~<_  suc  d }  e.  _V  ->  U. { f  e.  A  |  f  ~<_  suc  d }  e.  _V )
4129, 39, 403syl 18 . . . . . 6  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  U. {
f  e.  A  | 
f  ~<_  suc  d }  e.  _V )
42 breq2 4420 . . . . . . . . 9  |-  ( e  =  suc  d  -> 
( f  ~<_  e  <->  f  ~<_  suc  d
) )
4342rabbidv 3048 . . . . . . . 8  |-  ( e  =  suc  d  ->  { f  e.  A  |  f  ~<_  e }  =  { f  e.  A  |  f  ~<_  suc  d } )
4443unieqd 4222 . . . . . . 7  |-  ( e  =  suc  d  ->  U. { f  e.  A  |  f  ~<_  e }  =  U. { f  e.  A  |  f  ~<_  suc  d } )
4544, 13fvmptg 5969 . . . . . 6  |-  ( ( suc  d  e.  om  /\ 
U. { f  e.  A  |  f  ~<_  suc  d }  e.  _V )  ->  ( ( e  e.  om  |->  U. {
f  e.  A  | 
f  ~<_  e } ) `
 suc  d )  =  U. { f  e.  A  |  f  ~<_  suc  d } )
4638, 41, 45syl2anr 485 . . . . 5  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  /\  d  e.  om )  ->  (
( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
) `  suc  d )  =  U. { f  e.  A  |  f  ~<_  suc  d } )
4725, 37, 463sstr4d 3487 . . . 4  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  /\  d  e.  om )  ->  (
( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
) `  d )  C_  ( ( e  e. 
om  |->  U. { f  e.  A  |  f  ~<_  e } ) `  suc  d ) )
4847ralrimiva 2814 . . 3  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  A. d  e.  om  ( ( e  e.  om  |->  U. {
f  e.  A  | 
f  ~<_  e } ) `
 d )  C_  ( ( e  e. 
om  |->  U. { f  e.  A  |  f  ~<_  e } ) `  suc  d ) )
49 fin34i 8837 . . 3  |-  ( ( B  e. FinIII  /\  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e } ) : om --> ~P B  /\  A. d  e.  om  ( ( e  e.  om  |->  U. {
f  e.  A  | 
f  ~<_  e } ) `
 d )  C_  ( ( e  e. 
om  |->  U. { f  e.  A  |  f  ~<_  e } ) `  suc  d ) )  ->  U. ran  ( e  e. 
om  |->  U. { f  e.  A  |  f  ~<_  e } )  e.  ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
) )
501, 14, 48, 49syl3anc 1276 . 2  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  U. ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  e.  ran  (
e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
) )
51 fin1a2lem11 8866 . . . . . 6  |-  ( ( [ C.]  Or  A  /\  A  C_ 
Fin )  ->  ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  =  ( A  u.  { (/) } ) )
5251adantrr 728 . . . . 5  |-  ( ( [ C.]  Or  A  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  ->  ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  =  ( A  u.  { (/) } ) )
53523ad2antl2 1177 . . . 4  |-  ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  ->  ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  =  ( A  u.  { (/) } ) )
5453adantr 471 . . 3  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  =  ( A  u.  { (/) } ) )
55 simpll3 1055 . . . . . 6  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  -.  U. A  e.  A )
56 simplrr 776 . . . . . . 7  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  A  =/=  (/) )
57 sspwuni 4381 . . . . . . . . . . 11  |-  ( A 
C_  ~P (/)  <->  U. A  C_  (/) )
58 ss0b 3776 . . . . . . . . . . 11  |-  ( U. A  C_  (/)  <->  U. A  =  (/) )
5957, 58bitri 257 . . . . . . . . . 10  |-  ( A 
C_  ~P (/)  <->  U. A  =  (/) )
60 pw0 4132 . . . . . . . . . . . . 13  |-  ~P (/)  =  { (/)
}
6160sseq2i 3469 . . . . . . . . . . . 12  |-  ( A 
C_  ~P (/)  <->  A  C_  { (/) } )
62 sssn 4143 . . . . . . . . . . . 12  |-  ( A 
C_  { (/) }  <->  ( A  =  (/)  \/  A  =  { (/) } ) )
6361, 62bitri 257 . . . . . . . . . . 11  |-  ( A 
C_  ~P (/)  <->  ( A  =  (/)  \/  A  =  { (/)
} ) )
64 df-ne 2635 . . . . . . . . . . . 12  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
65 0ex 4549 . . . . . . . . . . . . . . . . 17  |-  (/)  e.  _V
6665unisn 4227 . . . . . . . . . . . . . . . 16  |-  U. { (/)
}  =  (/)
6765snid 4008 . . . . . . . . . . . . . . . 16  |-  (/)  e.  { (/)
}
6866, 67eqeltri 2536 . . . . . . . . . . . . . . 15  |-  U. { (/)
}  e.  { (/) }
69 unieq 4220 . . . . . . . . . . . . . . . 16  |-  ( A  =  { (/) }  ->  U. A  =  U. { (/)
} )
70 id 22 . . . . . . . . . . . . . . . 16  |-  ( A  =  { (/) }  ->  A  =  { (/) } )
7169, 70eleq12d 2534 . . . . . . . . . . . . . . 15  |-  ( A  =  { (/) }  ->  ( U. A  e.  A  <->  U. { (/) }  e.  { (/)
} ) )
7268, 71mpbiri 241 . . . . . . . . . . . . . 14  |-  ( A  =  { (/) }  ->  U. A  e.  A )
7372orim2i 525 . . . . . . . . . . . . 13  |-  ( ( A  =  (/)  \/  A  =  { (/) } )  -> 
( A  =  (/)  \/ 
U. A  e.  A
) )
7473ord 383 . . . . . . . . . . . 12  |-  ( ( A  =  (/)  \/  A  =  { (/) } )  -> 
( -.  A  =  (/)  ->  U. A  e.  A
) )
7564, 74syl5bi 225 . . . . . . . . . . 11  |-  ( ( A  =  (/)  \/  A  =  { (/) } )  -> 
( A  =/=  (/)  ->  U. A  e.  A ) )
7663, 75sylbi 200 . . . . . . . . . 10  |-  ( A 
C_  ~P (/)  ->  ( A  =/=  (/)  ->  U. A  e.  A ) )
7759, 76sylbir 218 . . . . . . . . 9  |-  ( U. A  =  (/)  ->  ( A  =/=  (/)  ->  U. A  e.  A ) )
7877com12 32 . . . . . . . 8  |-  ( A  =/=  (/)  ->  ( U. A  =  (/)  ->  U. A  e.  A ) )
7978con3d 140 . . . . . . 7  |-  ( A  =/=  (/)  ->  ( -.  U. A  e.  A  ->  -.  U. A  =  (/) ) )
8056, 55, 79sylc 62 . . . . . 6  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  -.  U. A  =  (/) )
81 ioran 497 . . . . . 6  |-  ( -.  ( U. A  e.  A  \/  U. A  =  (/) )  <->  ( -.  U. A  e.  A  /\  -.  U. A  =  (/) ) )
8255, 80, 81sylanbrc 675 . . . . 5  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  -.  ( U. A  e.  A  \/  U. A  =  (/) ) )
83 uniun 4231 . . . . . . . 8  |-  U. ( A  u.  { (/) } )  =  ( U. A  u.  U. { (/) } )
8466uneq2i 3597 . . . . . . . 8  |-  ( U. A  u.  U. { (/) } )  =  ( U. A  u.  (/) )
85 un0 3771 . . . . . . . 8  |-  ( U. A  u.  (/) )  = 
U. A
8683, 84, 853eqtri 2488 . . . . . . 7  |-  U. ( A  u.  { (/) } )  =  U. A
8786eleq1i 2531 . . . . . 6  |-  ( U. ( A  u.  { (/) } )  e.  ( A  u.  { (/) } )  <->  U. A  e.  ( A  u.  { (/) } ) )
88 elun 3586 . . . . . 6  |-  ( U. A  e.  ( A  u.  { (/) } )  <->  ( U. A  e.  A  \/  U. A  e.  { (/) } ) )
8965elsnc2 4011 . . . . . . 7  |-  ( U. A  e.  { (/) }  <->  U. A  =  (/) )
9089orbi2i 526 . . . . . 6  |-  ( ( U. A  e.  A  \/  U. A  e.  { (/)
} )  <->  ( U. A  e.  A  \/  U. A  =  (/) ) )
9187, 88, 903bitri 279 . . . . 5  |-  ( U. ( A  u.  { (/) } )  e.  ( A  u.  { (/) } )  <-> 
( U. A  e.  A  \/  U. A  =  (/) ) )
9282, 91sylnibr 311 . . . 4  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  -.  U. ( A  u.  { (/)
} )  e.  ( A  u.  { (/) } ) )
93 unieq 4220 . . . . . 6  |-  ( ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  =  ( A  u.  { (/) } )  ->  U. ran  ( e  e.  om  |->  U. {
f  e.  A  | 
f  ~<_  e } )  =  U. ( A  u.  { (/) } ) )
94 id 22 . . . . . 6  |-  ( ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  =  ( A  u.  { (/) } )  ->  ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e } )  =  ( A  u.  { (/) } ) )
9593, 94eleq12d 2534 . . . . 5  |-  ( ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  =  ( A  u.  { (/) } )  ->  ( U. ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  e.  ran  (
e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  <->  U. ( A  u.  {
(/) } )  e.  ( A  u.  { (/) } ) ) )
9695notbid 300 . . . 4  |-  ( ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  =  ( A  u.  { (/) } )  ->  ( -.  U. ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  e.  ran  (
e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  <->  -.  U. ( A  u.  { (/) } )  e.  ( A  u.  {
(/) } ) ) )
9792, 96syl5ibrcom 230 . . 3  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  ( ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  =  ( A  u.  { (/) } )  ->  -.  U. ran  (
e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
)  e.  ran  (
e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
) ) )
9854, 97mpd 15 . 2  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  /\  B  e. FinIII )  ->  -.  U.
ran  ( e  e. 
om  |->  U. { f  e.  A  |  f  ~<_  e } )  e.  ran  ( e  e.  om  |->  U. { f  e.  A  |  f  ~<_  e }
) )
9950, 98pm2.65da 584 1  |-  ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( A  C_  Fin  /\  A  =/=  (/) ) )  ->  -.  B  e. FinIII )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    \/ wo 374    /\ wa 375    /\ w3a 991    = wceq 1455    e. wcel 1898    =/= wne 2633   A.wral 2749   {crab 2753   _Vcvv 3057    u. cun 3414    C_ wss 3416   (/)c0 3743   ~Pcpw 3963   {csn 3980   U.cuni 4212   class class class wbr 4416    |-> cmpt 4475    Or wor 4773   ran crn 4854   suc csuc 5444   -->wf 5597   ` cfv 5601   [ C.] crpss 6597   omcom 6719    ~<_ cdom 7593   Fincfn 7595  FinIIIcfin3 8737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6277  df-rpss 6598  df-om 6720  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-wdom 8100  df-card 8399  df-fin4 8743  df-fin3 8744
This theorem is referenced by:  fin1a2s  8870
  Copyright terms: Public domain W3C validator