ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ctssdccl Unicode version

Theorem ctssdccl 6962
Description: A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 6964 but expressed in terms of classes rather than  E.. (Contributed by Jim Kingdon, 30-Oct-2023.)
Hypotheses
Ref Expression
ctssdccl.f  |-  ( ph  ->  F : om -onto-> ( A 1o ) )
ctssdccl.s  |-  S  =  { x  e.  om  |  ( F `  x )  e.  (inl " A ) }
ctssdccl.g  |-  G  =  ( `'inl  o.  F
)
Assertion
Ref Expression
ctssdccl  |-  ( ph  ->  ( S  C_  om  /\  G : S -onto-> A  /\  A. n  e.  om DECID  n  e.  S ) )
Distinct variable groups:    x, A    n, F, x    n, G    S, n    ph, n
Allowed substitution hints:    ph( x)    A( n)    S( x)    G( x)

Proof of Theorem ctssdccl
Dummy variables  m  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ctssdccl.s . . . 4  |-  S  =  { x  e.  om  |  ( F `  x )  e.  (inl " A ) }
2 ssrab2 3150 . . . 4  |-  { x  e.  om  |  ( F `
 x )  e.  (inl " A ) }  C_  om
31, 2eqsstri 3097 . . 3  |-  S  C_  om
43a1i 9 . 2  |-  ( ph  ->  S  C_  om )
5 djulf1o 6909 . . . . . . 7  |- inl : _V -1-1-onto-> ( { (/) }  X.  _V )
6 f1ocnv 5346 . . . . . . 7  |-  (inl : _V
-1-1-onto-> ( { (/) }  X.  _V )  ->  `'inl : ( { (/) }  X.  _V ) -1-1-onto-> _V )
7 f1ofun 5335 . . . . . . 7  |-  ( `'inl
: ( { (/) }  X.  _V ) -1-1-onto-> _V  ->  Fun  `'inl )
85, 6, 7mp2b 8 . . . . . 6  |-  Fun  `'inl
9 ctssdccl.f . . . . . . 7  |-  ( ph  ->  F : om -onto-> ( A 1o ) )
10 fofun 5314 . . . . . . 7  |-  ( F : om -onto-> ( A 1o )  ->  Fun  F
)
119, 10syl 14 . . . . . 6  |-  ( ph  ->  Fun  F )
12 funco 5131 . . . . . . 7  |-  ( ( Fun  `'inl  /\  Fun  F
)  ->  Fun  ( `'inl 
o.  F ) )
13 ctssdccl.g . . . . . . . 8  |-  G  =  ( `'inl  o.  F
)
1413funeqi 5112 . . . . . . 7  |-  ( Fun 
G  <->  Fun  ( `'inl  o.  F ) )
1512, 14sylibr 133 . . . . . 6  |-  ( ( Fun  `'inl  /\  Fun  F
)  ->  Fun  G )
168, 11, 15sylancr 408 . . . . 5  |-  ( ph  ->  Fun  G )
17 fof 5313 . . . . . . . . . . . 12  |-  ( F : om -onto-> ( A 1o )  ->  F : om
--> ( A 1o )
)
189, 17syl 14 . . . . . . . . . . 11  |-  ( ph  ->  F : om --> ( A 1o ) )
1918fdmd 5247 . . . . . . . . . 10  |-  ( ph  ->  dom  F  =  om )
2019eleq2d 2185 . . . . . . . . 9  |-  ( ph  ->  ( n  e.  dom  F  <-> 
n  e.  om )
)
2120anbi1d 458 . . . . . . . 8  |-  ( ph  ->  ( ( n  e. 
dom  F  /\  ( F `  n )  e.  dom  `'inl )  <->  ( n  e.  om  /\  ( F `
 n )  e. 
dom  `'inl ) ) )
22 dmcoss 4776 . . . . . . . . . . . 12  |-  dom  ( `'inl  o.  F )  C_  dom  F
2322sseli 3061 . . . . . . . . . . 11  |-  ( n  e.  dom  ( `'inl 
o.  F )  ->  n  e.  dom  F )
2423pm4.71ri 387 . . . . . . . . . 10  |-  ( n  e.  dom  ( `'inl 
o.  F )  <->  ( n  e.  dom  F  /\  n  e.  dom  ( `'inl  o.  F ) ) )
25 dmfco 5455 . . . . . . . . . . 11  |-  ( ( Fun  F  /\  n  e.  dom  F )  -> 
( n  e.  dom  ( `'inl  o.  F )  <->  ( F `  n )  e.  dom  `'inl ) )
2625pm5.32da 445 . . . . . . . . . 10  |-  ( Fun 
F  ->  ( (
n  e.  dom  F  /\  n  e.  dom  ( `'inl  o.  F ) )  <-> 
( n  e.  dom  F  /\  ( F `  n )  e.  dom  `'inl ) ) )
2724, 26syl5bb 191 . . . . . . . . 9  |-  ( Fun 
F  ->  ( n  e.  dom  ( `'inl  o.  F )  <->  ( n  e.  dom  F  /\  ( F `  n )  e.  dom  `'inl ) ) )
2811, 27syl 14 . . . . . . . 8  |-  ( ph  ->  ( n  e.  dom  ( `'inl  o.  F )  <->  ( n  e.  dom  F  /\  ( F `  n )  e.  dom  `'inl ) ) )
29 simpr 109 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  om )  /\  ( F `  n )  e.  (inl " A ) )  ->  ( F `  n )  e.  (inl " A ) )
30 imassrn 4860 . . . . . . . . . . . . . 14  |-  (inl " A )  C_  ran inl
3130sseli 3061 . . . . . . . . . . . . 13  |-  ( ( F `  n )  e.  (inl " A
)  ->  ( F `  n )  e.  ran inl )
3231adantl 273 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  om )  /\  ( F `  n )  e.  (inl " A ) )  ->  ( F `  n )  e.  ran inl )
33 df-rn 4518 . . . . . . . . . . . . 13  |-  ran inl  =  dom  `'inl
3433eleq2i 2182 . . . . . . . . . . . 12  |-  ( ( F `  n )  e.  ran inl  <->  ( F `  n )  e.  dom  `'inl )
3532, 34sylib 121 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  om )  /\  ( F `  n )  e.  (inl " A ) )  ->  ( F `  n )  e.  dom  `'inl )
3629, 352thd 174 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  om )  /\  ( F `  n )  e.  (inl " A ) )  ->  ( ( F `  n )  e.  (inl " A )  <-> 
( F `  n
)  e.  dom  `'inl ) )
37 djuin 6915 . . . . . . . . . . . . . 14  |-  ( (inl " A )  i^i  (inr " 1o ) )  =  (/)
38 disjel 3385 . . . . . . . . . . . . . 14  |-  ( ( ( (inl " A
)  i^i  (inr " 1o ) )  =  (/)  /\  ( F `  n
)  e.  (inl " A ) )  ->  -.  ( F `  n
)  e.  (inr " 1o ) )
3937, 38mpan 418 . . . . . . . . . . . . 13  |-  ( ( F `  n )  e.  (inl " A
)  ->  -.  ( F `  n )  e.  (inr " 1o ) )
4039con2i 599 . . . . . . . . . . . 12  |-  ( ( F `  n )  e.  (inr " 1o )  ->  -.  ( F `  n )  e.  (inl " A ) )
4140adantl 273 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  om )  /\  ( F `  n )  e.  (inr " 1o ) )  ->  -.  ( F `  n )  e.  (inl " A ) )
42 djuin 6915 . . . . . . . . . . . . . . . 16  |-  ( (inl " _V )  i^i  (inr " 1o ) )  =  (/)
43 disjel 3385 . . . . . . . . . . . . . . . 16  |-  ( ( ( (inl " _V )  i^i  (inr " 1o ) )  =  (/)  /\  ( F `  n
)  e.  (inl " _V ) )  ->  -.  ( F `  n )  e.  (inr " 1o ) )
4442, 43mpan 418 . . . . . . . . . . . . . . 15  |-  ( ( F `  n )  e.  (inl " _V )  ->  -.  ( F `  n )  e.  (inr " 1o ) )
45 dfrn4 4967 . . . . . . . . . . . . . . 15  |-  ran inl  =  (inl " _V )
4644, 45eleq2s 2210 . . . . . . . . . . . . . 14  |-  ( ( F `  n )  e.  ran inl  ->  -.  ( F `  n )  e.  (inr " 1o ) )
4746con2i 599 . . . . . . . . . . . . 13  |-  ( ( F `  n )  e.  (inr " 1o )  ->  -.  ( F `  n )  e.  ran inl )
4847adantl 273 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  om )  /\  ( F `  n )  e.  (inr " 1o ) )  ->  -.  ( F `  n )  e.  ran inl )
4948, 34sylnib 648 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  om )  /\  ( F `  n )  e.  (inr " 1o ) )  ->  -.  ( F `  n )  e.  dom  `'inl )
5041, 492falsed 674 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  om )  /\  ( F `  n )  e.  (inr " 1o ) )  ->  ( ( F `  n )  e.  (inl " A )  <-> 
( F `  n
)  e.  dom  `'inl ) )
5118ffvelrnda 5521 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  om )  ->  ( F `  n )  e.  ( A 1o ) )
52 djuun 6918 . . . . . . . . . . . . 13  |-  ( (inl " A )  u.  (inr " 1o ) )  =  ( A 1o )
5352eleq2i 2182 . . . . . . . . . . . 12  |-  ( ( F `  n )  e.  ( (inl " A )  u.  (inr " 1o ) )  <->  ( F `  n )  e.  ( A 1o ) )
5451, 53sylibr 133 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  om )  ->  ( F `  n )  e.  ( (inl " A )  u.  (inr " 1o ) ) )
55 elun 3185 . . . . . . . . . . 11  |-  ( ( F `  n )  e.  ( (inl " A )  u.  (inr " 1o ) )  <->  ( ( F `  n )  e.  (inl " A )  \/  ( F `  n )  e.  (inr " 1o ) ) )
5654, 55sylib 121 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  om )  ->  ( ( F `  n )  e.  (inl " A )  \/  ( F `  n )  e.  (inr " 1o ) ) )
5736, 50, 56mpjaodan 770 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  om )  ->  ( ( F `  n )  e.  (inl " A )  <-> 
( F `  n
)  e.  dom  `'inl ) )
5857pm5.32da 445 . . . . . . . 8  |-  ( ph  ->  ( ( n  e. 
om  /\  ( F `  n )  e.  (inl " A ) )  <->  ( n  e.  om  /\  ( F `
 n )  e. 
dom  `'inl ) ) )
5921, 28, 583bitr4d 219 . . . . . . 7  |-  ( ph  ->  ( n  e.  dom  ( `'inl  o.  F )  <->  ( n  e.  om  /\  ( F `
 n )  e.  (inl " A ) ) ) )
6013dmeqi 4708 . . . . . . . 8  |-  dom  G  =  dom  ( `'inl  o.  F )
6160eleq2i 2182 . . . . . . 7  |-  ( n  e.  dom  G  <->  n  e.  dom  ( `'inl  o.  F
) )
62 fveq2 5387 . . . . . . . . 9  |-  ( x  =  n  ->  ( F `  x )  =  ( F `  n ) )
6362eleq1d 2184 . . . . . . . 8  |-  ( x  =  n  ->  (
( F `  x
)  e.  (inl " A )  <->  ( F `  n )  e.  (inl " A ) ) )
6463, 1elrab2 2814 . . . . . . 7  |-  ( n  e.  S  <->  ( n  e.  om  /\  ( F `
 n )  e.  (inl " A ) ) )
6559, 61, 643bitr4g 222 . . . . . 6  |-  ( ph  ->  ( n  e.  dom  G  <-> 
n  e.  S ) )
6665eqrdv 2113 . . . . 5  |-  ( ph  ->  dom  G  =  S )
67 df-fn 5094 . . . . 5  |-  ( G  Fn  S  <->  ( Fun  G  /\  dom  G  =  S ) )
6816, 66, 67sylanbrc 411 . . . 4  |-  ( ph  ->  G  Fn  S )
6913fveq1i 5388 . . . . . . 7  |-  ( G `
 m )  =  ( ( `'inl  o.  F ) `  m
)
7018adantr 272 . . . . . . . 8  |-  ( (
ph  /\  m  e.  S )  ->  F : om --> ( A 1o ) )
71 fveq2 5387 . . . . . . . . . . . . 13  |-  ( x  =  m  ->  ( F `  x )  =  ( F `  m ) )
7271eleq1d 2184 . . . . . . . . . . . 12  |-  ( x  =  m  ->  (
( F `  x
)  e.  (inl " A )  <->  ( F `  m )  e.  (inl " A ) ) )
7372, 1elrab2 2814 . . . . . . . . . . 11  |-  ( m  e.  S  <->  ( m  e.  om  /\  ( F `
 m )  e.  (inl " A ) ) )
7473biimpi 119 . . . . . . . . . 10  |-  ( m  e.  S  ->  (
m  e.  om  /\  ( F `  m )  e.  (inl " A
) ) )
7574adantl 273 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  S )  ->  (
m  e.  om  /\  ( F `  m )  e.  (inl " A
) ) )
7675simpld 111 . . . . . . . 8  |-  ( (
ph  /\  m  e.  S )  ->  m  e.  om )
77 fvco3 5458 . . . . . . . 8  |-  ( ( F : om --> ( A 1o )  /\  m  e.  om )  ->  (
( `'inl  o.  F
) `  m )  =  ( `'inl `  ( F `  m )
) )
7870, 76, 77syl2anc 406 . . . . . . 7  |-  ( (
ph  /\  m  e.  S )  ->  (
( `'inl  o.  F
) `  m )  =  ( `'inl `  ( F `  m )
) )
7969, 78syl5eq 2160 . . . . . 6  |-  ( (
ph  /\  m  e.  S )  ->  ( G `  m )  =  ( `'inl `  ( F `  m )
) )
80 f1ofun 5335 . . . . . . . . . 10  |-  (inl : _V
-1-1-onto-> ( { (/) }  X.  _V )  ->  Fun inl )
815, 80ax-mp 5 . . . . . . . . 9  |-  Fun inl
82 fvelima 5439 . . . . . . . . 9  |-  ( ( Fun inl  /\  ( F `  m )  e.  (inl " A ) )  ->  E. z  e.  A  (inl `  z )  =  ( F `  m
) )
8381, 82mpan 418 . . . . . . . 8  |-  ( ( F `  m )  e.  (inl " A
)  ->  E. z  e.  A  (inl `  z
)  =  ( F `
 m ) )
8475, 83simpl2im 381 . . . . . . 7  |-  ( (
ph  /\  m  e.  S )  ->  E. z  e.  A  (inl `  z
)  =  ( F `
 m ) )
85 simprr 504 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  S )  /\  (
z  e.  A  /\  (inl `  z )  =  ( F `  m
) ) )  -> 
(inl `  z )  =  ( F `  m ) )
8685fveq2d 5391 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  S )  /\  (
z  e.  A  /\  (inl `  z )  =  ( F `  m
) ) )  -> 
( `'inl `  (inl `  z ) )  =  ( `'inl `  ( F `  m )
) )
87 vex 2661 . . . . . . . . . 10  |-  z  e. 
_V
88 f1ocnvfv1 5644 . . . . . . . . . 10  |-  ( (inl : _V -1-1-onto-> ( { (/) }  X.  _V )  /\  z  e.  _V )  ->  ( `'inl `  (inl `  z
) )  =  z )
895, 87, 88mp2an 420 . . . . . . . . 9  |-  ( `'inl `  (inl `  z )
)  =  z
90 simprl 503 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  S )  /\  (
z  e.  A  /\  (inl `  z )  =  ( F `  m
) ) )  -> 
z  e.  A )
9189, 90eqeltrid 2202 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  S )  /\  (
z  e.  A  /\  (inl `  z )  =  ( F `  m
) ) )  -> 
( `'inl `  (inl `  z ) )  e.  A )
9286, 91eqeltrrd 2193 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  S )  /\  (
z  e.  A  /\  (inl `  z )  =  ( F `  m
) ) )  -> 
( `'inl `  ( F `  m )
)  e.  A )
9384, 92rexlimddv 2529 . . . . . 6  |-  ( (
ph  /\  m  e.  S )  ->  ( `'inl `  ( F `  m ) )  e.  A )
9479, 93eqeltrd 2192 . . . . 5  |-  ( (
ph  /\  m  e.  S )  ->  ( G `  m )  e.  A )
9594ralrimiva 2480 . . . 4  |-  ( ph  ->  A. m  e.  S  ( G `  m )  e.  A )
96 ffnfv 5544 . . . 4  |-  ( G : S --> A  <->  ( G  Fn  S  /\  A. m  e.  S  ( G `  m )  e.  A
) )
9768, 95, 96sylanbrc 411 . . 3  |-  ( ph  ->  G : S --> A )
98 djulcl 6902 . . . . . . . 8  |-  ( m  e.  A  ->  (inl `  m )  e.  ( A 1o ) )
99 foelrn 5620 . . . . . . . . . 10  |-  ( ( F : om -onto-> ( A 1o )  /\  (inl `  m )  e.  ( A 1o ) )  ->  E. y  e.  om  (inl `  m )  =  ( F `  y
) )
1009, 99sylan 279 . . . . . . . . 9  |-  ( (
ph  /\  (inl `  m
)  e.  ( A 1o ) )  ->  E. y  e.  om  (inl `  m
)  =  ( F `
 y ) )
101 df-rex 2397 . . . . . . . . 9  |-  ( E. y  e.  om  (inl `  m )  =  ( F `  y )  <->  E. y ( y  e. 
om  /\  (inl `  m
)  =  ( F `
 y ) ) )
102100, 101sylib 121 . . . . . . . 8  |-  ( (
ph  /\  (inl `  m
)  e.  ( A 1o ) )  ->  E. y
( y  e.  om  /\  (inl `  m )  =  ( F `  y ) ) )
10398, 102sylan2 282 . . . . . . 7  |-  ( (
ph  /\  m  e.  A )  ->  E. y
( y  e.  om  /\  (inl `  m )  =  ( F `  y ) ) )
104 fveq2 5387 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
105104eleq1d 2184 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( F `  x
)  e.  (inl " A )  <->  ( F `  y )  e.  (inl " A ) ) )
106 simprl 503 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  A )  /\  (
y  e.  om  /\  (inl `  m )  =  ( F `  y
) ) )  -> 
y  e.  om )
107 simprr 504 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  A )  /\  (
y  e.  om  /\  (inl `  m )  =  ( F `  y
) ) )  -> 
(inl `  m )  =  ( F `  y ) )
108 vex 2661 . . . . . . . . . . . . . . . 16  |-  m  e. 
_V
109 f1odm 5337 . . . . . . . . . . . . . . . . 17  |-  (inl : _V
-1-1-onto-> ( { (/) }  X.  _V )  ->  dom inl  =  _V )
1105, 109ax-mp 5 . . . . . . . . . . . . . . . 16  |-  dom inl  =  _V
111108, 110eleqtrri 2191 . . . . . . . . . . . . . . 15  |-  m  e. 
dom inl
112 funfvima 5615 . . . . . . . . . . . . . . 15  |-  ( ( Fun inl  /\  m  e.  dom inl )  ->  ( m  e.  A  ->  (inl `  m )  e.  (inl " A ) ) )
11381, 111, 112mp2an 420 . . . . . . . . . . . . . 14  |-  ( m  e.  A  ->  (inl `  m )  e.  (inl " A ) )
114113ad2antlr 478 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  A )  /\  (
y  e.  om  /\  (inl `  m )  =  ( F `  y
) ) )  -> 
(inl `  m )  e.  (inl " A ) )
115107, 114eqeltrrd 2193 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  A )  /\  (
y  e.  om  /\  (inl `  m )  =  ( F `  y
) ) )  -> 
( F `  y
)  e.  (inl " A ) )
116105, 106, 115elrabd 2813 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  A )  /\  (
y  e.  om  /\  (inl `  m )  =  ( F `  y
) ) )  -> 
y  e.  { x  e.  om  |  ( F `
 x )  e.  (inl " A ) } )
117116, 1syl6eleqr 2209 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  A )  /\  (
y  e.  om  /\  (inl `  m )  =  ( F `  y
) ) )  -> 
y  e.  S )
118117, 107jca 302 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  A )  /\  (
y  e.  om  /\  (inl `  m )  =  ( F `  y
) ) )  -> 
( y  e.  S  /\  (inl `  m )  =  ( F `  y ) ) )
119118ex 114 . . . . . . . 8  |-  ( (
ph  /\  m  e.  A )  ->  (
( y  e.  om  /\  (inl `  m )  =  ( F `  y ) )  -> 
( y  e.  S  /\  (inl `  m )  =  ( F `  y ) ) ) )
120119eximdv 1834 . . . . . . 7  |-  ( (
ph  /\  m  e.  A )  ->  ( E. y ( y  e. 
om  /\  (inl `  m
)  =  ( F `
 y ) )  ->  E. y ( y  e.  S  /\  (inl `  m )  =  ( F `  y ) ) ) )
121103, 120mpd 13 . . . . . 6  |-  ( (
ph  /\  m  e.  A )  ->  E. y
( y  e.  S  /\  (inl `  m )  =  ( F `  y ) ) )
122 df-rex 2397 . . . . . 6  |-  ( E. y  e.  S  (inl
`  m )  =  ( F `  y
)  <->  E. y ( y  e.  S  /\  (inl `  m )  =  ( F `  y ) ) )
123121, 122sylibr 133 . . . . 5  |-  ( (
ph  /\  m  e.  A )  ->  E. y  e.  S  (inl `  m
)  =  ( F `
 y ) )
124 f1ocnvfv1 5644 . . . . . . . . . 10  |-  ( (inl : _V -1-1-onto-> ( { (/) }  X.  _V )  /\  m  e.  _V )  ->  ( `'inl `  (inl `  m
) )  =  m )
1255, 108, 124mp2an 420 . . . . . . . . 9  |-  ( `'inl `  (inl `  m )
)  =  m
126 simpr 109 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  A )  /\  y  e.  S
)  /\  (inl `  m
)  =  ( F `
 y ) )  ->  (inl `  m
)  =  ( F `
 y ) )
127126fveq2d 5391 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  A )  /\  y  e.  S
)  /\  (inl `  m
)  =  ( F `
 y ) )  ->  ( `'inl `  (inl `  m ) )  =  ( `'inl `  ( F `  y )
) )
128125, 127syl5eqr 2162 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  A )  /\  y  e.  S
)  /\  (inl `  m
)  =  ( F `
 y ) )  ->  m  =  ( `'inl `  ( F `  y ) ) )
12913fveq1i 5388 . . . . . . . . . 10  |-  ( G `
 y )  =  ( ( `'inl  o.  F ) `  y
)
13018ad2antrr 477 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  A )  /\  y  e.  S )  ->  F : om --> ( A 1o ) )
1313sseli 3061 . . . . . . . . . . . 12  |-  ( y  e.  S  ->  y  e.  om )
132131adantl 273 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  A )  /\  y  e.  S )  ->  y  e.  om )
133 fvco3 5458 . . . . . . . . . . 11  |-  ( ( F : om --> ( A 1o )  /\  y  e.  om )  ->  (
( `'inl  o.  F
) `  y )  =  ( `'inl `  ( F `  y )
) )
134130, 132, 133syl2anc 406 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  A )  /\  y  e.  S )  ->  (
( `'inl  o.  F
) `  y )  =  ( `'inl `  ( F `  y )
) )
135129, 134syl5eq 2160 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  A )  /\  y  e.  S )  ->  ( G `  y )  =  ( `'inl `  ( F `  y )
) )
136135adantr 272 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  A )  /\  y  e.  S
)  /\  (inl `  m
)  =  ( F `
 y ) )  ->  ( G `  y )  =  ( `'inl `  ( F `  y ) ) )
137128, 136eqtr4d 2151 . . . . . . 7  |-  ( ( ( ( ph  /\  m  e.  A )  /\  y  e.  S
)  /\  (inl `  m
)  =  ( F `
 y ) )  ->  m  =  ( G `  y ) )
138137ex 114 . . . . . 6  |-  ( ( ( ph  /\  m  e.  A )  /\  y  e.  S )  ->  (
(inl `  m )  =  ( F `  y )  ->  m  =  ( G `  y ) ) )
139138reximdva 2509 . . . . 5  |-  ( (
ph  /\  m  e.  A )  ->  ( E. y  e.  S  (inl `  m )  =  ( F `  y
)  ->  E. y  e.  S  m  =  ( G `  y ) ) )
140123, 139mpd 13 . . . 4  |-  ( (
ph  /\  m  e.  A )  ->  E. y  e.  S  m  =  ( G `  y ) )
141140ralrimiva 2480 . . 3  |-  ( ph  ->  A. m  e.  A  E. y  e.  S  m  =  ( G `  y ) )
142 dffo3 5533 . . 3  |-  ( G : S -onto-> A  <->  ( G : S --> A  /\  A. m  e.  A  E. y  e.  S  m  =  ( G `  y ) ) )
14397, 141, 142sylanbrc 411 . 2  |-  ( ph  ->  G : S -onto-> A
)
14453, 55bitr3i 185 . . . . . . 7  |-  ( ( F `  n )  e.  ( A 1o )  <-> 
( ( F `  n )  e.  (inl " A )  \/  ( F `  n )  e.  (inr " 1o ) ) )
14551, 144sylib 121 . . . . . 6  |-  ( (
ph  /\  n  e.  om )  ->  ( ( F `  n )  e.  (inl " A )  \/  ( F `  n )  e.  (inr " 1o ) ) )
14640orim2i 733 . . . . . 6  |-  ( ( ( F `  n
)  e.  (inl " A )  \/  ( F `  n )  e.  (inr " 1o ) )  ->  ( ( F `  n )  e.  (inl " A )  \/  -.  ( F `
 n )  e.  (inl " A ) ) )
147145, 146syl 14 . . . . 5  |-  ( (
ph  /\  n  e.  om )  ->  ( ( F `  n )  e.  (inl " A )  \/  -.  ( F `
 n )  e.  (inl " A ) ) )
148 df-dc 803 . . . . 5  |-  (DECID  ( F `
 n )  e.  (inl " A )  <-> 
( ( F `  n )  e.  (inl " A )  \/  -.  ( F `  n )  e.  (inl " A
) ) )
149147, 148sylibr 133 . . . 4  |-  ( (
ph  /\  n  e.  om )  -> DECID  ( F `  n
)  e.  (inl " A ) )
150 ibar 297 . . . . . . 7  |-  ( n  e.  om  ->  (
( F `  n
)  e.  (inl " A )  <->  ( n  e.  om  /\  ( F `
 n )  e.  (inl " A ) ) ) )
151150adantl 273 . . . . . 6  |-  ( (
ph  /\  n  e.  om )  ->  ( ( F `  n )  e.  (inl " A )  <-> 
( n  e.  om  /\  ( F `  n
)  e.  (inl " A ) ) ) )
152151, 64syl6bbr 197 . . . . 5  |-  ( (
ph  /\  n  e.  om )  ->  ( ( F `  n )  e.  (inl " A )  <-> 
n  e.  S ) )
153152dcbid 806 . . . 4  |-  ( (
ph  /\  n  e.  om )  ->  (DECID  ( F `  n )  e.  (inl " A )  <-> DECID  n  e.  S
) )
154149, 153mpbid 146 . . 3  |-  ( (
ph  /\  n  e.  om )  -> DECID  n  e.  S
)
155154ralrimiva 2480 . 2  |-  ( ph  ->  A. n  e.  om DECID  n  e.  S )
1564, 143, 1553jca 1144 1  |-  ( ph  ->  ( S  C_  om  /\  G : S -onto-> A  /\  A. n  e.  om DECID  n  e.  S ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 680  DECID wdc 802    /\ w3a 945    = wceq 1314   E.wex 1451    e. wcel 1463   A.wral 2391   E.wrex 2392   {crab 2395   _Vcvv 2658    u. cun 3037    i^i cin 3038    C_ wss 3039   (/)c0 3331   {csn 3495   omcom 4472    X. cxp 4505   `'ccnv 4506   dom cdm 4507   ran crn 4508   "cima 4510    o. ccom 4511   Fun wfun 5085    Fn wfn 5086   -->wf 5087   -onto->wfo 5089   -1-1-onto->wf1o 5090   ` cfv 5091   1oc1o 6272   ⊔ cdju 6888  inlcinl 6896  inrcinr 6897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-ral 2396  df-rex 2397  df-rab 2400  df-v 2660  df-sbc 2881  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-iord 4256  df-on 4258  df-suc 4261  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-1st 6004  df-2nd 6005  df-1o 6279  df-dju 6889  df-inl 6898  df-inr 6899
This theorem is referenced by:  ctssdclemr  6963  ctiunct  11848
  Copyright terms: Public domain W3C validator