Metamath Proof Explorer

Theorem fin23lem30

Description: Lemma for fin23 . The residual is disjoint from the common set. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypotheses fin23lem.a 
|- U = seqom ( ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )
fin23lem17.f 
|- F = { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }
fin23lem.b 
|- P = { v e. _om | |^| ran U C_ ( t ` v ) }
fin23lem.c 
|- Q = ( w e. _om |-> ( iota_ x e. P ( x i^i P ) ~~ w ) )
fin23lem.d 
|- R = ( w e. _om |-> ( iota_ x e. ( _om \ P ) ( x i^i ( _om \ P ) ) ~~ w ) )
fin23lem.e 
|- Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) )
Assertion fin23lem30 
|- ( Fun t -> ( U. ran Z i^i |^| ran U ) = (/) )

Proof

Step Hyp Ref Expression
1 fin23lem.a 
 |-  U = seqom ( ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )
2 fin23lem17.f 
 |-  F = { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }
3 fin23lem.b 
 |-  P = { v e. _om | |^| ran U C_ ( t ` v ) }
4 fin23lem.c 
 |-  Q = ( w e. _om |-> ( iota_ x e. P ( x i^i P ) ~~ w ) )
5 fin23lem.d 
 |-  R = ( w e. _om |-> ( iota_ x e. ( _om \ P ) ( x i^i ( _om \ P ) ) ~~ w ) )
6 fin23lem.e 
 |-  Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) )
7 eqif 
 |-  ( Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) ) <-> ( ( P e. Fin /\ Z = ( t o. R ) ) \/ ( -. P e. Fin /\ Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) ) ) )
8 7 biimpi 
 |-  ( Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) ) -> ( ( P e. Fin /\ Z = ( t o. R ) ) \/ ( -. P e. Fin /\ Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) ) ) )
9 simpr 
 |-  ( ( P e. Fin /\ Fun t ) -> Fun t )
10 5 funmpt2 
 |-  Fun R
11 funco 
 |-  ( ( Fun t /\ Fun R ) -> Fun ( t o. R ) )
12 9 10 11 sylancl 
 |-  ( ( P e. Fin /\ Fun t ) -> Fun ( t o. R ) )
13 elunirn 
 |-  ( Fun ( t o. R ) -> ( a e. U. ran ( t o. R ) <-> E. b e. dom ( t o. R ) a e. ( ( t o. R ) ` b ) ) )
14 12 13 syl 
 |-  ( ( P e. Fin /\ Fun t ) -> ( a e. U. ran ( t o. R ) <-> E. b e. dom ( t o. R ) a e. ( ( t o. R ) ` b ) ) )
15 dmcoss 
 |-  dom ( t o. R ) C_ dom R
16 15 sseli 
 |-  ( b e. dom ( t o. R ) -> b e. dom R )
17 fvco 
 |-  ( ( Fun R /\ b e. dom R ) -> ( ( t o. R ) ` b ) = ( t ` ( R ` b ) ) )
18 10 17 mpan 
 |-  ( b e. dom R -> ( ( t o. R ) ` b ) = ( t ` ( R ` b ) ) )
19 18 adantl 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> ( ( t o. R ) ` b ) = ( t ` ( R ` b ) ) )
20 19 eleq2d 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> ( a e. ( ( t o. R ) ` b ) <-> a e. ( t ` ( R ` b ) ) ) )
21 incom 
 |-  ( ( t ` ( R ` b ) ) i^i |^| ran U ) = ( |^| ran U i^i ( t ` ( R ` b ) ) )
22 difss 
 |-  ( _om \ P ) C_ _om
23 ominf 
 |-  -. _om e. Fin
24 3 ssrab3 
 |-  P C_ _om
25 undif 
 |-  ( P C_ _om <-> ( P u. ( _om \ P ) ) = _om )
26 24 25 mpbi 
 |-  ( P u. ( _om \ P ) ) = _om
27 unfi 
 |-  ( ( P e. Fin /\ ( _om \ P ) e. Fin ) -> ( P u. ( _om \ P ) ) e. Fin )
28 26 27 eqeltrrid 
 |-  ( ( P e. Fin /\ ( _om \ P ) e. Fin ) -> _om e. Fin )
29 28 ex 
 |-  ( P e. Fin -> ( ( _om \ P ) e. Fin -> _om e. Fin ) )
30 23 29 mtoi 
 |-  ( P e. Fin -> -. ( _om \ P ) e. Fin )
31 30 ad2antrr 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> -. ( _om \ P ) e. Fin )
32 5 fin23lem22 
 |-  ( ( ( _om \ P ) C_ _om /\ -. ( _om \ P ) e. Fin ) -> R : _om -1-1-onto-> ( _om \ P ) )
33 22 31 32 sylancr 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> R : _om -1-1-onto-> ( _om \ P ) )
34 f1of 
 |-  ( R : _om -1-1-onto-> ( _om \ P ) -> R : _om --> ( _om \ P ) )
35 33 34 syl 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> R : _om --> ( _om \ P ) )
36 simpr 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> b e. dom R )
37 35 fdmd 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> dom R = _om )
38 36 37 eleqtrd 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> b e. _om )
39 35 38 ffvelrnd 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> ( R ` b ) e. ( _om \ P ) )
40 39 eldifbd 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> -. ( R ` b ) e. P )
41 3 eleq2i 
 |-  ( ( R ` b ) e. P <-> ( R ` b ) e. { v e. _om | |^| ran U C_ ( t ` v ) } )
42 40 41 sylnib 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> -. ( R ` b ) e. { v e. _om | |^| ran U C_ ( t ` v ) } )
43 39 eldifad 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> ( R ` b ) e. _om )
44 fveq2 
 |-  ( v = ( R ` b ) -> ( t ` v ) = ( t ` ( R ` b ) ) )
45 44 sseq2d 
 |-  ( v = ( R ` b ) -> ( |^| ran U C_ ( t ` v ) <-> |^| ran U C_ ( t ` ( R ` b ) ) ) )
46 45 elrab3 
 |-  ( ( R ` b ) e. _om -> ( ( R ` b ) e. { v e. _om | |^| ran U C_ ( t ` v ) } <-> |^| ran U C_ ( t ` ( R ` b ) ) ) )
47 43 46 syl 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> ( ( R ` b ) e. { v e. _om | |^| ran U C_ ( t ` v ) } <-> |^| ran U C_ ( t ` ( R ` b ) ) ) )
48 42 47 mtbid 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> -. |^| ran U C_ ( t ` ( R ` b ) ) )
49 1 fin23lem20 
 |-  ( ( R ` b ) e. _om -> ( |^| ran U C_ ( t ` ( R ` b ) ) \/ ( |^| ran U i^i ( t ` ( R ` b ) ) ) = (/) ) )
50 43 49 syl 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> ( |^| ran U C_ ( t ` ( R ` b ) ) \/ ( |^| ran U i^i ( t ` ( R ` b ) ) ) = (/) ) )
51 orel1 
 |-  ( -. |^| ran U C_ ( t ` ( R ` b ) ) -> ( ( |^| ran U C_ ( t ` ( R ` b ) ) \/ ( |^| ran U i^i ( t ` ( R ` b ) ) ) = (/) ) -> ( |^| ran U i^i ( t ` ( R ` b ) ) ) = (/) ) )
52 48 50 51 sylc 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> ( |^| ran U i^i ( t ` ( R ` b ) ) ) = (/) )
53 21 52 syl5eq 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> ( ( t ` ( R ` b ) ) i^i |^| ran U ) = (/) )
54 disj 
 |-  ( ( ( t ` ( R ` b ) ) i^i |^| ran U ) = (/) <-> A. a e. ( t ` ( R ` b ) ) -. a e. |^| ran U )
55 53 54 sylib 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> A. a e. ( t ` ( R ` b ) ) -. a e. |^| ran U )
56 rsp 
 |-  ( A. a e. ( t ` ( R ` b ) ) -. a e. |^| ran U -> ( a e. ( t ` ( R ` b ) ) -> -. a e. |^| ran U ) )
57 55 56 syl 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> ( a e. ( t ` ( R ` b ) ) -> -. a e. |^| ran U ) )
58 20 57 sylbid 
 |-  ( ( ( P e. Fin /\ Fun t ) /\ b e. dom R ) -> ( a e. ( ( t o. R ) ` b ) -> -. a e. |^| ran U ) )
59 58 ex 
 |-  ( ( P e. Fin /\ Fun t ) -> ( b e. dom R -> ( a e. ( ( t o. R ) ` b ) -> -. a e. |^| ran U ) ) )
60 16 59 syl5 
 |-  ( ( P e. Fin /\ Fun t ) -> ( b e. dom ( t o. R ) -> ( a e. ( ( t o. R ) ` b ) -> -. a e. |^| ran U ) ) )
61 60 rexlimdv 
 |-  ( ( P e. Fin /\ Fun t ) -> ( E. b e. dom ( t o. R ) a e. ( ( t o. R ) ` b ) -> -. a e. |^| ran U ) )
62 14 61 sylbid 
 |-  ( ( P e. Fin /\ Fun t ) -> ( a e. U. ran ( t o. R ) -> -. a e. |^| ran U ) )
63 62 ralrimiv 
 |-  ( ( P e. Fin /\ Fun t ) -> A. a e. U. ran ( t o. R ) -. a e. |^| ran U )
64 disj 
 |-  ( ( U. ran ( t o. R ) i^i |^| ran U ) = (/) <-> A. a e. U. ran ( t o. R ) -. a e. |^| ran U )
65 63 64 sylibr 
 |-  ( ( P e. Fin /\ Fun t ) -> ( U. ran ( t o. R ) i^i |^| ran U ) = (/) )
66 rneq 
 |-  ( Z = ( t o. R ) -> ran Z = ran ( t o. R ) )
67 66 unieqd 
 |-  ( Z = ( t o. R ) -> U. ran Z = U. ran ( t o. R ) )
68 67 ineq1d 
 |-  ( Z = ( t o. R ) -> ( U. ran Z i^i |^| ran U ) = ( U. ran ( t o. R ) i^i |^| ran U ) )
69 68 eqeq1d 
 |-  ( Z = ( t o. R ) -> ( ( U. ran Z i^i |^| ran U ) = (/) <-> ( U. ran ( t o. R ) i^i |^| ran U ) = (/) ) )
70 65 69 syl5ibr 
 |-  ( Z = ( t o. R ) -> ( ( P e. Fin /\ Fun t ) -> ( U. ran Z i^i |^| ran U ) = (/) ) )
71 70 expd 
 |-  ( Z = ( t o. R ) -> ( P e. Fin -> ( Fun t -> ( U. ran Z i^i |^| ran U ) = (/) ) ) )
72 71 impcom 
 |-  ( ( P e. Fin /\ Z = ( t o. R ) ) -> ( Fun t -> ( U. ran Z i^i |^| ran U ) = (/) ) )
73 rneq 
 |-  ( Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) -> ran Z = ran ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) )
74 73 unieqd 
 |-  ( Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) -> U. ran Z = U. ran ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) )
75 74 ineq1d 
 |-  ( Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) -> ( U. ran Z i^i |^| ran U ) = ( U. ran ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) i^i |^| ran U ) )
76 rncoss 
 |-  ran ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) C_ ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) )
77 76 unissi 
 |-  U. ran ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) C_ U. ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) )
78 disj 
 |-  ( ( U. ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) i^i |^| ran U ) = (/) <-> A. a e. U. ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) -. a e. |^| ran U )
79 eluniab 
 |-  ( a e. U. { b | E. z e. P b = ( ( t ` z ) \ |^| ran U ) } <-> E. b ( a e. b /\ E. z e. P b = ( ( t ` z ) \ |^| ran U ) ) )
80 eleq2 
 |-  ( b = ( ( t ` z ) \ |^| ran U ) -> ( a e. b <-> a e. ( ( t ` z ) \ |^| ran U ) ) )
81 eldifn 
 |-  ( a e. ( ( t ` z ) \ |^| ran U ) -> -. a e. |^| ran U )
82 80 81 syl6bi 
 |-  ( b = ( ( t ` z ) \ |^| ran U ) -> ( a e. b -> -. a e. |^| ran U ) )
83 82 rexlimivw 
 |-  ( E. z e. P b = ( ( t ` z ) \ |^| ran U ) -> ( a e. b -> -. a e. |^| ran U ) )
84 83 impcom 
 |-  ( ( a e. b /\ E. z e. P b = ( ( t ` z ) \ |^| ran U ) ) -> -. a e. |^| ran U )
85 84 exlimiv 
 |-  ( E. b ( a e. b /\ E. z e. P b = ( ( t ` z ) \ |^| ran U ) ) -> -. a e. |^| ran U )
86 79 85 sylbi 
 |-  ( a e. U. { b | E. z e. P b = ( ( t ` z ) \ |^| ran U ) } -> -. a e. |^| ran U )
87 eqid 
 |-  ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) = ( z e. P |-> ( ( t ` z ) \ |^| ran U ) )
88 87 rnmpt 
 |-  ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) = { b | E. z e. P b = ( ( t ` z ) \ |^| ran U ) }
89 88 unieqi 
 |-  U. ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) = U. { b | E. z e. P b = ( ( t ` z ) \ |^| ran U ) }
90 86 89 eleq2s 
 |-  ( a e. U. ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) -> -. a e. |^| ran U )
91 78 90 mprgbir 
 |-  ( U. ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) i^i |^| ran U ) = (/)
92 ssdisj 
 |-  ( ( U. ran ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) C_ U. ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) /\ ( U. ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) i^i |^| ran U ) = (/) ) -> ( U. ran ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) i^i |^| ran U ) = (/) )
93 77 91 92 mp2an 
 |-  ( U. ran ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) i^i |^| ran U ) = (/)
94 75 93 eqtrdi 
 |-  ( Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) -> ( U. ran Z i^i |^| ran U ) = (/) )
95 94 a1d 
 |-  ( Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) -> ( Fun t -> ( U. ran Z i^i |^| ran U ) = (/) ) )
96 95 adantl 
 |-  ( ( -. P e. Fin /\ Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) ) -> ( Fun t -> ( U. ran Z i^i |^| ran U ) = (/) ) )
97 72 96 jaoi 
 |-  ( ( ( P e. Fin /\ Z = ( t o. R ) ) \/ ( -. P e. Fin /\ Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) ) ) -> ( Fun t -> ( U. ran Z i^i |^| ran U ) = (/) ) )
98 6 8 97 mp2b 
 |-  ( Fun t -> ( U. ran Z i^i |^| ran U ) = (/) )