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

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

Proof of Theorem fin1a2lem13
Dummy variables  e 
f  g  h  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 447 . . 3  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B 
\  C )  e. FinII )  ->  ( B  \  C )  e. FinII )
2 simpll1 994 . . . 4  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B 
\  C )  e. FinII )  ->  A  C_  ~P B )
3 ssel2 3188 . . . . . . . . . 10  |-  ( ( A  C_  ~P B  /\  g  e.  A
)  ->  g  e.  ~P B )
4 vex 2804 . . . . . . . . . . 11  |-  g  e. 
_V
54elpw 3644 . . . . . . . . . 10  |-  ( g  e.  ~P B  <->  g  C_  B )
63, 5sylib 188 . . . . . . . . 9  |-  ( ( A  C_  ~P B  /\  g  e.  A
)  ->  g  C_  B )
7 ssdif 3324 . . . . . . . . 9  |-  ( g 
C_  B  ->  (
g  \  C )  C_  ( B  \  C
) )
86, 7syl 15 . . . . . . . 8  |-  ( ( A  C_  ~P B  /\  g  e.  A
)  ->  ( g  \  C )  C_  ( B  \  C ) )
9 sseq1 3212 . . . . . . . 8  |-  ( f  =  ( g  \  C )  ->  (
f  C_  ( B  \  C )  <->  ( g  \  C )  C_  ( B  \  C ) ) )
108, 9syl5ibrcom 213 . . . . . . 7  |-  ( ( A  C_  ~P B  /\  g  e.  A
)  ->  ( f  =  ( g  \  C )  ->  f  C_  ( B  \  C
) ) )
1110rexlimdva 2680 . . . . . 6  |-  ( A 
C_  ~P B  ->  ( E. g  e.  A  f  =  ( g  \  C )  ->  f  C_  ( B  \  C
) ) )
12 vex 2804 . . . . . . 7  |-  f  e. 
_V
13 eqid 2296 . . . . . . . 8  |-  ( g  e.  A  |->  ( g 
\  C ) )  =  ( g  e.  A  |->  ( g  \  C ) )
1413elrnmpt 4942 . . . . . . 7  |-  ( f  e.  _V  ->  (
f  e.  ran  (
g  e.  A  |->  ( g  \  C ) )  <->  E. g  e.  A  f  =  ( g  \  C ) ) )
1512, 14ax-mp 8 . . . . . 6  |-  ( f  e.  ran  ( g  e.  A  |->  ( g 
\  C ) )  <->  E. g  e.  A  f  =  ( g  \  C ) )
1612elpw 3644 . . . . . 6  |-  ( f  e.  ~P ( B 
\  C )  <->  f  C_  ( B  \  C ) )
1711, 15, 163imtr4g 261 . . . . 5  |-  ( A 
C_  ~P B  ->  (
f  e.  ran  (
g  e.  A  |->  ( g  \  C ) )  ->  f  e.  ~P ( B  \  C
) ) )
1817ssrdv 3198 . . . 4  |-  ( A 
C_  ~P B  ->  ran  ( g  e.  A  |->  ( g  \  C
) )  C_  ~P ( B  \  C ) )
192, 18syl 15 . . 3  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B 
\  C )  e. FinII )  ->  ran  ( g  e.  A  |->  ( g 
\  C ) ) 
C_  ~P ( B  \  C ) )
20 simplrr 737 . . . 4  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B 
\  C )  e. FinII )  ->  C  e.  A
)
21 difid 3535 . . . . . . 7  |-  ( C 
\  C )  =  (/)
2221eqcomi 2300 . . . . . 6  |-  (/)  =  ( C  \  C )
23 difeq1 3300 . . . . . . . 8  |-  ( g  =  C  ->  (
g  \  C )  =  ( C  \  C ) )
2423eqeq2d 2307 . . . . . . 7  |-  ( g  =  C  ->  ( (/)  =  ( g  \  C )  <->  (/)  =  ( C  \  C ) ) )
2524rspcev 2897 . . . . . 6  |-  ( ( C  e.  A  /\  (/)  =  ( C  \  C ) )  ->  E. g  e.  A  (/)  =  ( g  \  C ) )
2622, 25mpan2 652 . . . . 5  |-  ( C  e.  A  ->  E. g  e.  A  (/)  =  ( g  \  C ) )
27 0ex 4166 . . . . . 6  |-  (/)  e.  _V
2813elrnmpt 4942 . . . . . 6  |-  ( (/)  e.  _V  ->  ( (/)  e.  ran  ( g  e.  A  |->  ( g  \  C
) )  <->  E. g  e.  A  (/)  =  ( g  \  C ) ) )
2927, 28ax-mp 8 . . . . 5  |-  ( (/)  e.  ran  ( g  e.  A  |->  ( g  \  C ) )  <->  E. g  e.  A  (/)  =  ( g  \  C ) )
3026, 29sylibr 203 . . . 4  |-  ( C  e.  A  ->  (/)  e.  ran  ( g  e.  A  |->  ( g  \  C
) ) )
31 ne0i 3474 . . . 4  |-  ( (/)  e.  ran  ( g  e.  A  |->  ( g  \  C ) )  ->  ran  ( g  e.  A  |->  ( g  \  C
) )  =/=  (/) )
3220, 30, 313syl 18 . . 3  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B 
\  C )  e. FinII )  ->  ran  ( g  e.  A  |->  ( g 
\  C ) )  =/=  (/) )
33 simpll2 995 . . . 4  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B 
\  C )  e. FinII )  -> [ C.]  Or  A
)
34 vex 2804 . . . . . . . 8  |-  x  e. 
_V
3513elrnmpt 4942 . . . . . . . 8  |-  ( x  e.  _V  ->  (
x  e.  ran  (
g  e.  A  |->  ( g  \  C ) )  <->  E. g  e.  A  x  =  ( g  \  C ) ) )
3634, 35ax-mp 8 . . . . . . 7  |-  ( x  e.  ran  ( g  e.  A  |->  ( g 
\  C ) )  <->  E. g  e.  A  x  =  ( g  \  C ) )
37 difeq1 3300 . . . . . . . . . 10  |-  ( g  =  e  ->  (
g  \  C )  =  ( e  \  C ) )
3837eqeq2d 2307 . . . . . . . . 9  |-  ( g  =  e  ->  (
x  =  ( g 
\  C )  <->  x  =  ( e  \  C
) ) )
3938cbvrexv 2778 . . . . . . . 8  |-  ( E. g  e.  A  x  =  ( g  \  C )  <->  E. e  e.  A  x  =  ( e  \  C
) )
40 sorpssi 6299 . . . . . . . . . . . . . . . 16  |-  ( ( [
C.]  Or  A  /\  ( e  e.  A  /\  g  e.  A
) )  ->  (
e  C_  g  \/  g  C_  e ) )
41 ssdif 3324 . . . . . . . . . . . . . . . . 17  |-  ( e 
C_  g  ->  (
e  \  C )  C_  ( g  \  C
) )
42 ssdif 3324 . . . . . . . . . . . . . . . . 17  |-  ( g 
C_  e  ->  (
g  \  C )  C_  ( e  \  C
) )
4341, 42orim12i 502 . . . . . . . . . . . . . . . 16  |-  ( ( e  C_  g  \/  g  C_  e )  -> 
( ( e  \  C )  C_  (
g  \  C )  \/  ( g  \  C
)  C_  ( e  \  C ) ) )
4440, 43syl 15 . . . . . . . . . . . . . . 15  |-  ( ( [
C.]  Or  A  /\  ( e  e.  A  /\  g  e.  A
) )  ->  (
( e  \  C
)  C_  ( g  \  C )  \/  (
g  \  C )  C_  ( e  \  C
) ) )
45 sseq2 3213 . . . . . . . . . . . . . . . 16  |-  ( f  =  ( g  \  C )  ->  (
( e  \  C
)  C_  f  <->  ( e  \  C )  C_  (
g  \  C )
) )
46 sseq1 3212 . . . . . . . . . . . . . . . 16  |-  ( f  =  ( g  \  C )  ->  (
f  C_  ( e  \  C )  <->  ( g  \  C )  C_  (
e  \  C )
) )
4745, 46orbi12d 690 . . . . . . . . . . . . . . 15  |-  ( f  =  ( g  \  C )  ->  (
( ( e  \  C )  C_  f  \/  f  C_  ( e 
\  C ) )  <-> 
( ( e  \  C )  C_  (
g  \  C )  \/  ( g  \  C
)  C_  ( e  \  C ) ) ) )
4844, 47syl5ibrcom 213 . . . . . . . . . . . . . 14  |-  ( ( [
C.]  Or  A  /\  ( e  e.  A  /\  g  e.  A
) )  ->  (
f  =  ( g 
\  C )  -> 
( ( e  \  C )  C_  f  \/  f  C_  ( e 
\  C ) ) ) )
4948expr 598 . . . . . . . . . . . . 13  |-  ( ( [
C.]  Or  A  /\  e  e.  A )  ->  ( g  e.  A  ->  ( f  =  ( g  \  C )  ->  ( ( e 
\  C )  C_  f  \/  f  C_  ( e  \  C
) ) ) ) )
5049rexlimdv 2679 . . . . . . . . . . . 12  |-  ( ( [
C.]  Or  A  /\  e  e.  A )  ->  ( E. g  e.  A  f  =  ( g  \  C )  ->  ( ( e 
\  C )  C_  f  \/  f  C_  ( e  \  C
) ) ) )
5115, 50syl5bi 208 . . . . . . . . . . 11  |-  ( ( [
C.]  Or  A  /\  e  e.  A )  ->  ( f  e.  ran  ( g  e.  A  |->  ( g  \  C
) )  ->  (
( e  \  C
)  C_  f  \/  f  C_  ( e  \  C ) ) ) )
5251ralrimiv 2638 . . . . . . . . . 10  |-  ( ( [
C.]  Or  A  /\  e  e.  A )  ->  A. f  e.  ran  ( g  e.  A  |->  ( g  \  C
) ) ( ( e  \  C ) 
C_  f  \/  f  C_  ( e  \  C
) ) )
53 sseq1 3212 . . . . . . . . . . . 12  |-  ( x  =  ( e  \  C )  ->  (
x  C_  f  <->  ( e  \  C )  C_  f
) )
54 sseq2 3213 . . . . . . . . . . . 12  |-  ( x  =  ( e  \  C )  ->  (
f  C_  x  <->  f  C_  ( e  \  C
) ) )
5553, 54orbi12d 690 . . . . . . . . . . 11  |-  ( x  =  ( e  \  C )  ->  (
( x  C_  f  \/  f  C_  x )  <-> 
( ( e  \  C )  C_  f  \/  f  C_  ( e 
\  C ) ) ) )
5655ralbidv 2576 . . . . . . . . . 10  |-  ( x  =  ( e  \  C )  ->  ( A. f  e.  ran  ( g  e.  A  |->  ( g  \  C
) ) ( x 
C_  f  \/  f  C_  x )  <->  A. f  e.  ran  ( g  e.  A  |->  ( g  \  C ) ) ( ( e  \  C
)  C_  f  \/  f  C_  ( e  \  C ) ) ) )
5752, 56syl5ibrcom 213 . . . . . . . . 9  |-  ( ( [
C.]  Or  A  /\  e  e.  A )  ->  ( x  =  ( e  \  C )  ->  A. f  e.  ran  ( g  e.  A  |->  ( g  \  C
) ) ( x 
C_  f  \/  f  C_  x ) ) )
5857rexlimdva 2680 . . . . . . . 8  |-  ( [ C.]  Or  A  ->  ( E. e  e.  A  x  =  ( e  \  C )  ->  A. f  e.  ran  ( g  e.  A  |->  ( g  \  C ) ) ( x  C_  f  \/  f  C_  x ) ) )
5939, 58syl5bi 208 . . . . . . 7  |-  ( [ C.]  Or  A  ->  ( E. g  e.  A  x  =  ( g  \  C )  ->  A. f  e.  ran  ( g  e.  A  |->  ( g  \  C ) ) ( x  C_  f  \/  f  C_  x ) ) )
6036, 59syl5bi 208 . . . . . 6  |-  ( [ C.]  Or  A  ->  ( x  e.  ran  ( g  e.  A  |->  ( g 
\  C ) )  ->  A. f  e.  ran  ( g  e.  A  |->  ( g  \  C
) ) ( x 
C_  f  \/  f  C_  x ) ) )
6160ralrimiv 2638 . . . . 5  |-  ( [ C.]  Or  A  ->  A. x  e.  ran  ( g  e.  A  |->  ( g  \  C ) ) A. f  e.  ran  ( g  e.  A  |->  ( g 
\  C ) ) ( x  C_  f  \/  f  C_  x ) )
62 sorpss 6298 . . . . 5  |-  ( [ C.]  Or  ran  ( g  e.  A  |->  ( g  \  C ) )  <->  A. x  e.  ran  ( g  e.  A  |->  ( g  \  C ) ) A. f  e.  ran  ( g  e.  A  |->  ( g 
\  C ) ) ( x  C_  f  \/  f  C_  x ) )
6361, 62sylibr 203 . . . 4  |-  ( [ C.]  Or  A  -> [ C.]  Or  ran  ( g  e.  A  |->  ( g  \  C
) ) )
6433, 63syl 15 . . 3  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B 
\  C )  e. FinII )  -> [ C.]  Or  ran  ( g  e.  A  |->  ( g  \  C
) ) )
65 fin2i 7937 . . 3  |-  ( ( ( ( B  \  C )  e. FinII  /\  ran  ( g  e.  A  |->  ( g  \  C
) )  C_  ~P ( B  \  C ) )  /\  ( ran  ( g  e.  A  |->  ( g  \  C
) )  =/=  (/)  /\ [ C.]  Or  ran  ( g  e.  A  |->  ( g  \  C ) ) ) )  ->  U. ran  (
g  e.  A  |->  ( g  \  C ) )  e.  ran  (
g  e.  A  |->  ( g  \  C ) ) )
661, 19, 32, 64, 65syl22anc 1183 . 2  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B 
\  C )  e. FinII )  ->  U. ran  ( g  e.  A  |->  ( g 
\  C ) )  e.  ran  ( g  e.  A  |->  ( g 
\  C ) ) )
67 simpll3 996 . . 3  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B 
\  C )  e. FinII )  ->  -.  U. A  e.  A )
68 difeq1 3300 . . . . . . 7  |-  ( g  =  f  ->  (
g  \  C )  =  ( f  \  C ) )
6968cbvmptv 4127 . . . . . 6  |-  ( g  e.  A  |->  ( g 
\  C ) )  =  ( f  e.  A  |->  ( f  \  C ) )
7069elrnmpt 4942 . . . . 5  |-  ( U. ran  ( g  e.  A  |->  ( g  \  C
) )  e.  ran  ( g  e.  A  |->  ( g  \  C
) )  ->  ( U. ran  ( g  e.  A  |->  ( g  \  C ) )  e. 
ran  ( g  e.  A  |->  ( g  \  C ) )  <->  E. f  e.  A  U. ran  (
g  e.  A  |->  ( g  \  C ) )  =  ( f 
\  C ) ) )
7170ibi 232 . . . 4  |-  ( U. ran  ( g  e.  A  |->  ( g  \  C
) )  e.  ran  ( g  e.  A  |->  ( g  \  C
) )  ->  E. f  e.  A  U. ran  (
g  e.  A  |->  ( g  \  C ) )  =  ( f 
\  C ) )
72 eqid 2296 . . . . . . . . . . . . . . . . 17  |-  ( h 
\  C )  =  ( h  \  C
)
73 difeq1 3300 . . . . . . . . . . . . . . . . . . 19  |-  ( g  =  h  ->  (
g  \  C )  =  ( h  \  C ) )
7473eqeq2d 2307 . . . . . . . . . . . . . . . . . 18  |-  ( g  =  h  ->  (
( h  \  C
)  =  ( g 
\  C )  <->  ( h  \  C )  =  ( h  \  C ) ) )
7574rspcev 2897 . . . . . . . . . . . . . . . . 17  |-  ( ( h  e.  A  /\  ( h  \  C )  =  ( h  \  C ) )  ->  E. g  e.  A  ( h  \  C )  =  ( g  \  C ) )
7672, 75mpan2 652 . . . . . . . . . . . . . . . 16  |-  ( h  e.  A  ->  E. g  e.  A  ( h  \  C )  =  ( g  \  C ) )
7776adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g 
\  C ) )  =  ( f  \  C ) )  /\  h  e.  A )  ->  E. g  e.  A  ( h  \  C )  =  ( g  \  C ) )
78 vex 2804 . . . . . . . . . . . . . . . 16  |-  h  e. 
_V
79 difexg 4178 . . . . . . . . . . . . . . . 16  |-  ( h  e.  _V  ->  (
h  \  C )  e.  _V )
8013elrnmpt 4942 . . . . . . . . . . . . . . . 16  |-  ( ( h  \  C )  e.  _V  ->  (
( h  \  C
)  e.  ran  (
g  e.  A  |->  ( g  \  C ) )  <->  E. g  e.  A  ( h  \  C )  =  ( g  \  C ) ) )
8178, 79, 80mp2b 9 . . . . . . . . . . . . . . 15  |-  ( ( h  \  C )  e.  ran  ( g  e.  A  |->  ( g 
\  C ) )  <->  E. g  e.  A  ( h  \  C )  =  ( g  \  C ) )
8277, 81sylibr 203 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g 
\  C ) )  =  ( f  \  C ) )  /\  h  e.  A )  ->  ( h  \  C
)  e.  ran  (
g  e.  A  |->  ( g  \  C ) ) )
83 elssuni 3871 . . . . . . . . . . . . . 14  |-  ( ( h  \  C )  e.  ran  ( g  e.  A  |->  ( g 
\  C ) )  ->  ( h  \  C )  C_  U. ran  ( g  e.  A  |->  ( g  \  C
) ) )
8482, 83syl 15 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g 
\  C ) )  =  ( f  \  C ) )  /\  h  e.  A )  ->  ( h  \  C
)  C_  U. ran  (
g  e.  A  |->  ( g  \  C ) ) )
85 simplr 731 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g 
\  C ) )  =  ( f  \  C ) )  /\  h  e.  A )  ->  U. ran  ( g  e.  A  |->  ( g 
\  C ) )  =  ( f  \  C ) )
8684, 85sseqtrd 3227 . . . . . . . . . . . 12  |-  ( ( ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g 
\  C ) )  =  ( f  \  C ) )  /\  h  e.  A )  ->  ( h  \  C
)  C_  ( f  \  C ) )
8786adantll 694 . . . . . . . . . . 11  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  (
h  \  C )  C_  ( f  \  C
) )
88 unss2 3359 . . . . . . . . . . . 12  |-  ( ( h  \  C ) 
C_  ( f  \  C )  ->  ( C  u.  ( h  \  C ) )  C_  ( C  u.  (
f  \  C )
) )
89 uncom 3332 . . . . . . . . . . . . . . . 16  |-  ( C  u.  ( h  \  C ) )  =  ( ( h  \  C )  u.  C
)
90 undif1 3542 . . . . . . . . . . . . . . . 16  |-  ( ( h  \  C )  u.  C )  =  ( h  u.  C
)
9189, 90eqtri 2316 . . . . . . . . . . . . . . 15  |-  ( C  u.  ( h  \  C ) )  =  ( h  u.  C
)
9291a1i 10 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  ( C  u.  ( h  \  C ) )  =  ( h  u.  C
) )
9367ad2antrr 706 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  -.  U. A  e.  A )
9420ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  C  e.  A )
95 simplrr 737 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) )
96 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x 
\  C )  =  ( x  \  C
)
97 difeq1 3300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( g  =  x  ->  (
g  \  C )  =  ( x  \  C ) )
9897eqeq2d 2307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( g  =  x  ->  (
( x  \  C
)  =  ( g 
\  C )  <->  ( x  \  C )  =  ( x  \  C ) ) )
9998rspcev 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  e.  A  /\  ( x  \  C )  =  ( x  \  C ) )  ->  E. g  e.  A  ( x  \  C )  =  ( g  \  C ) )
10096, 99mpan2 652 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  A  ->  E. g  e.  A  ( x  \  C )  =  ( g  \  C ) )
101 difexg 4178 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  _V  ->  (
x  \  C )  e.  _V )
10213elrnmpt 4942 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  \  C )  e.  _V  ->  (
( x  \  C
)  e.  ran  (
g  e.  A  |->  ( g  \  C ) )  <->  E. g  e.  A  ( x  \  C )  =  ( g  \  C ) ) )
10334, 101, 102mp2b 9 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  \  C )  e.  ran  ( g  e.  A  |->  ( g 
\  C ) )  <->  E. g  e.  A  ( x  \  C )  =  ( g  \  C ) )
104100, 103sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  A  ->  (
x  \  C )  e.  ran  ( g  e.  A  |->  ( g  \  C ) ) )
105104adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( C  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) )  /\  f  C_  C )  /\  x  e.  A )  ->  (
x  \  C )  e.  ran  ( g  e.  A  |->  ( g  \  C ) ) )
106 simpllr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( C  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) )  /\  f  C_  C )  /\  x  e.  A )  ->  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) )
107 ssdif0 3526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f 
C_  C  <->  ( f  \  C )  =  (/) )
108107biimpi 186 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f 
C_  C  ->  (
f  \  C )  =  (/) )
109108ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( C  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) )  /\  f  C_  C )  /\  x  e.  A )  ->  (
f  \  C )  =  (/) )
110106, 109eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( C  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) )  /\  f  C_  C )  /\  x  e.  A )  ->  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  (/) )
111 uni0c 3869 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  (/)  <->  A. e  e.  ran  ( g  e.  A  |->  ( g 
\  C ) ) e  =  (/) )
112110, 111sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( C  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) )  /\  f  C_  C )  /\  x  e.  A )  ->  A. e  e.  ran  ( g  e.  A  |->  ( g  \  C ) ) e  =  (/) )
113 eqeq1 2302 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( e  =  ( x  \  C )  ->  (
e  =  (/)  <->  ( x  \  C )  =  (/) ) )
114113rspcva 2895 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  \  C
)  e.  ran  (
g  e.  A  |->  ( g  \  C ) )  /\  A. e  e.  ran  ( g  e.  A  |->  ( g  \  C ) ) e  =  (/) )  ->  (
x  \  C )  =  (/) )
115105, 112, 114syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( C  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) )  /\  f  C_  C )  /\  x  e.  A )  ->  (
x  \  C )  =  (/) )
116 ssdif0 3526 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x 
C_  C  <->  ( x  \  C )  =  (/) )
117115, 116sylibr 203 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( C  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) )  /\  f  C_  C )  /\  x  e.  A )  ->  x  C_  C )
118117ralrimiva 2639 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( C  e.  A  /\  U. ran  ( g  e.  A  |->  ( g 
\  C ) )  =  ( f  \  C ) )  /\  f  C_  C )  ->  A. x  e.  A  x  C_  C )
119 unissb 3873 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U. A  C_  C  <->  A. x  e.  A  x  C_  C
)
120118, 119sylibr 203 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( C  e.  A  /\  U. ran  ( g  e.  A  |->  ( g 
\  C ) )  =  ( f  \  C ) )  /\  f  C_  C )  ->  U. A  C_  C )
121 elssuni 3871 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( C  e.  A  ->  C  C_ 
U. A )
122121ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( C  e.  A  /\  U. ran  ( g  e.  A  |->  ( g 
\  C ) )  =  ( f  \  C ) )  /\  f  C_  C )  ->  C  C_  U. A )
123120, 122eqssd 3209 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( C  e.  A  /\  U. ran  ( g  e.  A  |->  ( g 
\  C ) )  =  ( f  \  C ) )  /\  f  C_  C )  ->  U. A  =  C
)
124 simpll 730 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( C  e.  A  /\  U. ran  ( g  e.  A  |->  ( g 
\  C ) )  =  ( f  \  C ) )  /\  f  C_  C )  ->  C  e.  A )
125123, 124eqeltrd 2370 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( C  e.  A  /\  U. ran  ( g  e.  A  |->  ( g 
\  C ) )  =  ( f  \  C ) )  /\  f  C_  C )  ->  U. A  e.  A
)
126125ex 423 . . . . . . . . . . . . . . . . . 18  |-  ( ( C  e.  A  /\  U.
ran  ( g  e.  A  |->  ( g  \  C ) )  =  ( f  \  C
) )  ->  (
f  C_  C  ->  U. A  e.  A ) )
12794, 95, 126syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  (
f  C_  C  ->  U. A  e.  A ) )
12893, 127mtod 168 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  -.  f  C_  C )
12933ad2antrr 706 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  -> [ C.]  Or  A )
130 simplrl 736 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  f  e.  A )
131 sorpssi 6299 . . . . . . . . . . . . . . . . 17  |-  ( ( [
C.]  Or  A  /\  ( f  e.  A  /\  C  e.  A
) )  ->  (
f  C_  C  \/  C  C_  f ) )
132129, 130, 94, 131syl12anc 1180 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  (
f  C_  C  \/  C  C_  f ) )
133 orel1 371 . . . . . . . . . . . . . . . 16  |-  ( -.  f  C_  C  ->  ( ( f  C_  C  \/  C  C_  f )  ->  C  C_  f
) )
134128, 132, 133sylc 56 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  C  C_  f )
135 undif 3547 . . . . . . . . . . . . . . 15  |-  ( C 
C_  f  <->  ( C  u.  ( f  \  C
) )  =  f )
136134, 135sylib 188 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  ( C  u.  ( f  \  C ) )  =  f )
13792, 136sseq12d 3220 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  (
( C  u.  (
h  \  C )
)  C_  ( C  u.  ( f  \  C
) )  <->  ( h  u.  C )  C_  f
) )
138 ssun1 3351 . . . . . . . . . . . . . 14  |-  h  C_  ( h  u.  C
)
139 sstr 3200 . . . . . . . . . . . . . 14  |-  ( ( h  C_  ( h  u.  C )  /\  (
h  u.  C ) 
C_  f )  ->  h  C_  f )
140138, 139mpan 651 . . . . . . . . . . . . 13  |-  ( ( h  u.  C ) 
C_  f  ->  h  C_  f )
141137, 140syl6bi 219 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  (
( C  u.  (
h  \  C )
)  C_  ( C  u.  ( f  \  C
) )  ->  h  C_  f ) )
14288, 141syl5 28 . . . . . . . . . . 11  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  (
( h  \  C
)  C_  ( f  \  C )  ->  h  C_  f ) )
14387, 142mpd 14 . . . . . . . . . 10  |-  ( ( ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A
)  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  /\  h  e.  A )  ->  h  C_  f )
144143ralrimiva 2639 . . . . . . . . 9  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e. 
Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  ->  A. h  e.  A  h  C_  f
)
145 unissb 3873 . . . . . . . . 9  |-  ( U. A  C_  f  <->  A. h  e.  A  h  C_  f
)
146144, 145sylibr 203 . . . . . . . 8  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e. 
Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  ->  U. A  C_  f )
147 elssuni 3871 . . . . . . . . 9  |-  ( f  e.  A  ->  f  C_ 
U. A )
148147ad2antrl 708 . . . . . . . 8  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e. 
Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  ->  f  C_ 
U. A )
149146, 148eqssd 3209 . . . . . . 7  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e. 
Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  ->  U. A  =  f )
150 simprl 732 . . . . . . 7  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e. 
Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  ->  f  e.  A )
151149, 150eqeltrd 2370 . . . . . 6  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e. 
Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  ( f  e.  A  /\  U. ran  ( g  e.  A  |->  ( g  \  C
) )  =  ( f  \  C ) ) )  ->  U. A  e.  A )
152151expr 598 . . . . 5  |-  ( ( ( ( ( A 
C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e. 
Fin  /\  C  e.  A ) )  /\  ( B  \  C )  e. FinII )  /\  f  e.  A )  ->  ( U. ran  ( g  e.  A  |->  ( g  \  C ) )  =  ( f  \  C
)  ->  U. A  e.  A ) )
153152rexlimdva 2680 . . . 4  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B 
\  C )  e. FinII )  ->  ( E. f  e.  A  U. ran  (
g  e.  A  |->  ( g  \  C ) )  =  ( f 
\  C )  ->  U. A  e.  A
) )
15471, 153syl5 28 . . 3  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B 
\  C )  e. FinII )  ->  ( U. ran  ( g  e.  A  |->  ( g  \  C
) )  e.  ran  ( g  e.  A  |->  ( g  \  C
) )  ->  U. A  e.  A ) )
15567, 154mtod 168 . 2  |-  ( ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  /\  ( B 
\  C )  e. FinII )  ->  -.  U. ran  (
g  e.  A  |->  ( g  \  C ) )  e.  ran  (
g  e.  A  |->  ( g  \  C ) ) )
15666, 155pm2.65da 559 1  |-  ( ( ( A  C_  ~P B  /\ [ C.]  Or  A  /\  -.  U. A  e.  A )  /\  ( -.  C  e.  Fin  /\  C  e.  A ) )  ->  -.  ( B  \  C )  e. FinII )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 934    = wceq 1632    e. wcel 1696    =/= wne 2459   A.wral 2556   E.wrex 2557   _Vcvv 2801    \ cdif 3162    u. cun 3163    C_ wss 3165   (/)c0 3468   ~Pcpw 3638   U.cuni 3843    e. cmpt 4093    Or wor 4329   ran crn 4706   [ C.] crpss 6292   Fincfn 6879  FinIIcfin2 7921
This theorem is referenced by:  fin1a2s  8056
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-po 4330  df-so 4331  df-xp 4711  df-rel 4712  df-cnv 4713  df-dm 4715  df-rn 4716  df-rpss 6293  df-fin2 7928
  Copyright terms: Public domain W3C validator