Theorem ctssdccl 7088

Description: A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7090 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.

Step	Hyp	Ref	Expression
1		ctssdccl.s	. . . 4 |- S = { x e. om | ( F ` x ) e. (inl " A ) }
2		ssrab2 3232	. . . 4 |- { x e. om | ( F ` x ) e. (inl " A ) } C_ om
3	1, 2	eqsstri 3179	. . 3 |- S C_ om
4	3	a1i 9	. 2 |- ( ph -> S C_ om )
5		djulf1o 7035	. . . . . . 7 |- inl : _V -1-1-onto-> ( { (/) } X. _V )
6		f1ocnv 5455	. . . . . . 7 |- (inl : _V -1-1-onto-> ( { (/) } X. _V ) -> `'inl : ( { (/) } X. _V ) -1-1-onto-> _V )
7		f1ofun 5444	. . . . . . 7 |- ( `'inl : ( { (/) } X. _V ) -1-1-onto-> _V -> Fun `'inl )
8	5, 6, 7	mp2b 8	. . . . . 6 |- Fun `'inl
9		ctssdccl.f	. . . . . . 7 |- ( ph -> F : om -onto-> ( A ⊔ 1o ) )
10		fofun 5421	. . . . . . 7 |- ( F : om -onto-> ( A ⊔ 1o ) -> Fun F )
11	9, 10	syl 14	. . . . . 6 |- ( ph -> Fun F )
12		funco 5238	. . . . . . 7 |- ( ( Fun `'inl /\ Fun F ) -> Fun ( `'inl o. F ) )
13		ctssdccl.g	. . . . . . . 8 |- G = ( `'inl o. F )
14	13	funeqi 5219	. . . . . . 7 |- ( Fun G <-> Fun ( `'inl o. F ) )
15	12, 14	sylibr 133	. . . . . 6 |- ( ( Fun `'inl /\ Fun F ) -> Fun G )
16	8, 11, 15	sylancr 412	. . . . 5 |- ( ph -> Fun G )
17		fof 5420	. . . . . . . . . . . 12 |- ( F : om -onto-> ( A ⊔ 1o ) -> F : om --> ( A ⊔ 1o ) )
18	9, 17	syl 14	. . . . . . . . . . 11 |- ( ph -> F : om --> ( A ⊔ 1o ) )
19	18	fdmd 5354	. . . . . . . . . 10 |- ( ph -> dom F = om )
20	19	eleq2d 2240	. . . . . . . . 9 |- ( ph -> ( n e. dom F <-> n e. om ) )
21	20	anbi1d 462	. . . . . . . 8 |- ( ph -> ( ( n e. dom F /\ ( F ` n ) e. dom `'inl ) <-> ( n e. om /\ ( F ` n ) e. dom `'inl ) ) )
22		dmcoss 4880	. . . . . . . . . . . 12 |- dom ( `'inl o. F ) C_ dom F
23	22	sseli 3143	. . . . . . . . . . 11 |- ( n e. dom ( `'inl o. F ) -> n e. dom F )
24	23	pm4.71ri 390	. . . . . . . . . 10 |- ( n e. dom ( `'inl o. F ) <-> ( n e. dom F /\ n e. dom ( `'inl o. F ) ) )
25		dmfco 5564	. . . . . . . . . . 11 |- ( ( Fun F /\ n e. dom F ) -> ( n e. dom ( `'inl o. F ) <-> ( F ` n ) e. dom `'inl ) )
26	25	pm5.32da 449	. . . . . . . . . 10 |- ( Fun F -> ( ( n e. dom F /\ n e. dom ( `'inl o. F ) ) <-> ( n e. dom F /\ ( F ` n ) e. dom `'inl ) ) )
27	24, 26	syl5bb 191	. . . . . . . . 9 |- ( Fun F -> ( n e. dom ( `'inl o. F ) <-> ( n e. dom F /\ ( F ` n ) e. dom `'inl ) ) )
28	11, 27	syl 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 4964	. . . . . . . . . . . . . 14 |- (inl " A ) C_ ran inl
31	30	sseli 3143	. . . . . . . . . . . . 13 |- ( ( F ` n ) e. (inl " A ) -> ( F ` n ) e. ran inl )
32	31	adantl 275	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inl " A ) ) -> ( F ` n ) e. ran inl )
33		df-rn 4622	. . . . . . . . . . . . 13 |- ran inl = dom `'inl
34	33	eleq2i 2237	. . . . . . . . . . . 12 |- ( ( F ` n ) e. ran inl <-> ( F ` n ) e. dom `'inl )
35	32, 34	sylib 121	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inl " A ) ) -> ( F ` n ) e. dom `'inl )
36	29, 35	2thd 174	. . . . . . . . . 10 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inl " A ) ) -> ( ( F ` n ) e. (inl " A ) <-> ( F ` n ) e. dom `'inl ) )
37		djuin 7041	. . . . . . . . . . . . . 14 |- ( (inl " A ) i^i (inr " 1o ) ) = (/)
38		disjel 3469	. . . . . . . . . . . . . 14 |- ( ( ( (inl " A ) i^i (inr " 1o ) ) = (/) /\ ( F ` n ) e. (inl " A ) ) -> -. ( F ` n ) e. (inr " 1o ) )
39	37, 38	mpan 422	. . . . . . . . . . . . 13 |- ( ( F ` n ) e. (inl " A ) -> -. ( F ` n ) e. (inr " 1o ) )
40	39	con2i 622	. . . . . . . . . . . 12 |- ( ( F ` n ) e. (inr " 1o ) -> -. ( F ` n ) e. (inl " A ) )
41	40	adantl 275	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> -. ( F ` n ) e. (inl " A ) )
42		djuin 7041	. . . . . . . . . . . . . . . 16 |- ( (inl " _V ) i^i (inr " 1o ) ) = (/)
43		disjel 3469	. . . . . . . . . . . . . . . 16 |- ( ( ( (inl " _V ) i^i (inr " 1o ) ) = (/) /\ ( F ` n ) e. (inl " _V ) ) -> -. ( F ` n ) e. (inr " 1o ) )
44	42, 43	mpan 422	. . . . . . . . . . . . . . 15 |- ( ( F ` n ) e. (inl " _V ) -> -. ( F ` n ) e. (inr " 1o ) )
45		dfrn4 5071	. . . . . . . . . . . . . . 15 |- ran inl = (inl " _V )
46	44, 45	eleq2s 2265	. . . . . . . . . . . . . 14 |- ( ( F ` n ) e. ran inl -> -. ( F ` n ) e. (inr " 1o ) )
47	46	con2i 622	. . . . . . . . . . . . 13 |- ( ( F ` n ) e. (inr " 1o ) -> -. ( F ` n ) e. ran inl )
48	47	adantl 275	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> -. ( F ` n ) e. ran inl )
49	48, 34	sylnib 671	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> -. ( F ` n ) e. dom `'inl )
50	41, 49	2falsed 697	. . . . . . . . . 10 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> ( ( F ` n ) e. (inl " A ) <-> ( F ` n ) e. dom `'inl ) )
51	18	ffvelrnda 5631	. . . . . . . . . . . 12 |- ( ( ph /\ n e. om ) -> ( F ` n ) e. ( A ⊔ 1o ) )
52		djuun 7044	. . . . . . . . . . . . 13 |- ( (inl " A ) u. (inr " 1o ) ) = ( A ⊔ 1o )
53	52	eleq2i 2237	. . . . . . . . . . . 12 |- ( ( F ` n ) e. ( (inl " A ) u. (inr " 1o ) ) <-> ( F ` n ) e. ( A ⊔ 1o ) )
54	51, 53	sylibr 133	. . . . . . . . . . 11 |- ( ( ph /\ n e. om ) -> ( F ` n ) e. ( (inl " A ) u. (inr " 1o ) ) )
55		elun 3268	. . . . . . . . . . 11 |- ( ( F ` n ) e. ( (inl " A ) u. (inr " 1o ) ) <-> ( ( F ` n ) e. (inl " A ) \/ ( F ` n ) e. (inr " 1o ) ) )
56	54, 55	sylib 121	. . . . . . . . . 10 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) \/ ( F ` n ) e. (inr " 1o ) ) )
57	36, 50, 56	mpjaodan 793	. . . . . . . . 9 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) <-> ( F ` n ) e. dom `'inl ) )
58	57	pm5.32da 449	. . . . . . . 8 |- ( ph -> ( ( n e. om /\ ( F ` n ) e. (inl " A ) ) <-> ( n e. om /\ ( F ` n ) e. dom `'inl ) ) )
59	21, 28, 58	3bitr4d 219	. . . . . . 7 |- ( ph -> ( n e. dom ( `'inl o. F ) <-> ( n e. om /\ ( F ` n ) e. (inl " A ) ) ) )
60	13	dmeqi 4812	. . . . . . . 8 |- dom G = dom ( `'inl o. F )
61	60	eleq2i 2237	. . . . . . 7 |- ( n e. dom G <-> n e. dom ( `'inl o. F ) )
62		fveq2 5496	. . . . . . . . 9 |- ( x = n -> ( F ` x ) = ( F ` n ) )
63	62	eleq1d 2239	. . . . . . . 8 |- ( x = n -> ( ( F ` x ) e. (inl " A ) <-> ( F ` n ) e. (inl " A ) ) )
64	63, 1	elrab2 2889	. . . . . . 7 |- ( n e. S <-> ( n e. om /\ ( F ` n ) e. (inl " A ) ) )
65	59, 61, 64	3bitr4g 222	. . . . . 6 |- ( ph -> ( n e. dom G <-> n e. S ) )
66	65	eqrdv 2168	. . . . 5 |- ( ph -> dom G = S )
67		df-fn 5201	. . . . 5 |- ( G Fn S <-> ( Fun G /\ dom G = S ) )
68	16, 66, 67	sylanbrc 415	. . . 4 |- ( ph -> G Fn S )
69	13	fveq1i 5497	. . . . . . 7 |- ( G ` m ) = ( ( `'inl o. F ) ` m )
70	18	adantr 274	. . . . . . . 8 |- ( ( ph /\ m e. S ) -> F : om --> ( A ⊔ 1o ) )
71		fveq2 5496	. . . . . . . . . . . . 13 |- ( x = m -> ( F ` x ) = ( F ` m ) )
72	71	eleq1d 2239	. . . . . . . . . . . 12 |- ( x = m -> ( ( F ` x ) e. (inl " A ) <-> ( F ` m ) e. (inl " A ) ) )
73	72, 1	elrab2 2889	. . . . . . . . . . 11 |- ( m e. S <-> ( m e. om /\ ( F ` m ) e. (inl " A ) ) )
74	73	biimpi 119	. . . . . . . . . 10 |- ( m e. S -> ( m e. om /\ ( F ` m ) e. (inl " A ) ) )
75	74	adantl 275	. . . . . . . . 9 |- ( ( ph /\ m e. S ) -> ( m e. om /\ ( F ` m ) e. (inl " A ) ) )
76	75	simpld 111	. . . . . . . 8 |- ( ( ph /\ m e. S ) -> m e. om )
77		fvco3 5567	. . . . . . . 8 |- ( ( F : om --> ( A ⊔ 1o ) /\ m e. om ) -> ( ( `'inl o. F ) ` m ) = ( `'inl ` ( F ` m ) ) )
78	70, 76, 77	syl2anc 409	. . . . . . 7 |- ( ( ph /\ m e. S ) -> ( ( `'inl o. F ) ` m ) = ( `'inl ` ( F ` m ) ) )
79	69, 78	eqtrid 2215	. . . . . 6 |- ( ( ph /\ m e. S ) -> ( G ` m ) = ( `'inl ` ( F ` m ) ) )
80		f1ofun 5444	. . . . . . . . . 10 |- (inl : _V -1-1-onto-> ( { (/) } X. _V ) -> Fun inl )
81	5, 80	ax-mp 5	. . . . . . . . 9 |- Fun inl
82		fvelima 5548	. . . . . . . . 9 |- ( ( Fun inl /\ ( F ` m ) e. (inl " A ) ) -> E. z e. A (inl ` z ) = ( F ` m ) )
83	81, 82	mpan 422	. . . . . . . 8 |- ( ( F ` m ) e. (inl " A ) -> E. z e. A (inl ` z ) = ( F ` m ) )
84	75, 83	simpl2im 384	. . . . . . 7 |- ( ( ph /\ m e. S ) -> E. z e. A (inl ` z ) = ( F ` m ) )
85		simprr 527	. . . . . . . . 9 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> (inl ` z ) = ( F ` m ) )
86	85	fveq2d 5500	. . . . . . . 8 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` (inl ` z ) ) = ( `'inl ` ( F ` m ) ) )
87		vex 2733	. . . . . . . . . 10 |- z e. _V
88		f1ocnvfv1 5756	. . . . . . . . . 10 |- ( (inl : _V -1-1-onto-> ( { (/) } X. _V ) /\ z e. _V ) -> ( `'inl ` (inl ` z ) ) = z )
89	5, 87, 88	mp2an 424	. . . . . . . . 9 |- ( `'inl ` (inl ` z ) ) = z
90		simprl 526	. . . . . . . . 9 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> z e. A )
91	89, 90	eqeltrid 2257	. . . . . . . 8 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` (inl ` z ) ) e. A )
92	86, 91	eqeltrrd 2248	. . . . . . 7 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` ( F ` m ) ) e. A )
93	84, 92	rexlimddv 2592	. . . . . 6 |- ( ( ph /\ m e. S ) -> ( `'inl ` ( F ` m ) ) e. A )
94	79, 93	eqeltrd 2247	. . . . 5 |- ( ( ph /\ m e. S ) -> ( G ` m ) e. A )
95	94	ralrimiva 2543	. . . 4 |- ( ph -> A. m e. S ( G ` m ) e. A )
96		ffnfv 5654	. . . 4 |- ( G : S --> A <-> ( G Fn S /\ A. m e. S ( G ` m ) e. A ) )
97	68, 95, 96	sylanbrc 415	. . 3 |- ( ph -> G : S --> A )
98		djulcl 7028	. . . . . . . 8 |- ( m e. A -> (inl ` m ) e. ( A ⊔ 1o ) )
99		foelrn 5732	. . . . . . . . . 10 |- ( ( F : om -onto-> ( A ⊔ 1o ) /\ (inl ` m ) e. ( A ⊔ 1o ) ) -> E. y e. om (inl ` m ) = ( F ` y ) )
100	9, 99	sylan 281	. . . . . . . . 9 |- ( ( ph /\ (inl ` m ) e. ( A ⊔ 1o ) ) -> E. y e. om (inl ` m ) = ( F ` y ) )
101		df-rex 2454	. . . . . . . . 9 |- ( E. y e. om (inl ` m ) = ( F ` y ) <-> E. y ( y e. om /\ (inl ` m ) = ( F ` y ) ) )
102	100, 101	sylib 121	. . . . . . . 8 |- ( ( ph /\ (inl ` m ) e. ( A ⊔ 1o ) ) -> E. y ( y e. om /\ (inl ` m ) = ( F ` y ) ) )
103	98, 102	sylan2 284	. . . . . . 7 |- ( ( ph /\ m e. A ) -> E. y ( y e. om /\ (inl ` m ) = ( F ` y ) ) )
104		fveq2 5496	. . . . . . . . . . . . 13 |- ( x = y -> ( F ` x ) = ( F ` y ) )
105	104	eleq1d 2239	. . . . . . . . . . . 12 |- ( x = y -> ( ( F ` x ) e. (inl " A ) <-> ( F ` y ) e. (inl " A ) ) )
106		simprl 526	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> y e. om )
107		simprr 527	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> (inl ` m ) = ( F ` y ) )
108		vex 2733	. . . . . . . . . . . . . . . 16 |- m e. _V
109		f1odm 5446	. . . . . . . . . . . . . . . . 17 |- (inl : _V -1-1-onto-> ( { (/) } X. _V ) -> dom inl = _V )
110	5, 109	ax-mp 5	. . . . . . . . . . . . . . . 16 |- dom inl = _V
111	108, 110	eleqtrri 2246	. . . . . . . . . . . . . . 15 |- m e. dom inl
112		funfvima 5727	. . . . . . . . . . . . . . 15 |- ( ( Fun inl /\ m e. dom inl ) -> ( m e. A -> (inl ` m ) e. (inl " A ) ) )
113	81, 111, 112	mp2an 424	. . . . . . . . . . . . . 14 |- ( m e. A -> (inl ` m ) e. (inl " A ) )
114	113	ad2antlr 486	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> (inl ` m ) e. (inl " A ) )
115	107, 114	eqeltrrd 2248	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> ( F ` y ) e. (inl " A ) )
116	105, 106, 115	elrabd 2888	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> y e. { x e. om | ( F ` x ) e. (inl " A ) } )
117	116, 1	eleqtrrdi 2264	. . . . . . . . . 10 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> y e. S )
118	117, 107	jca 304	. . . . . . . . 9 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> ( y e. S /\ (inl ` m ) = ( F ` y ) ) )
119	118	ex 114	. . . . . . . 8 |- ( ( ph /\ m e. A ) -> ( ( y e. om /\ (inl ` m ) = ( F ` y ) ) -> ( y e. S /\ (inl ` m ) = ( F ` y ) ) ) )
120	119	eximdv 1873	. . . . . . 7 |- ( ( ph /\ m e. A ) -> ( E. y ( y e. om /\ (inl ` m ) = ( F ` y ) ) -> E. y ( y e. S /\ (inl ` m ) = ( F ` y ) ) ) )
121	103, 120	mpd 13	. . . . . 6 |- ( ( ph /\ m e. A ) -> E. y ( y e. S /\ (inl ` m ) = ( F ` y ) ) )
122		df-rex 2454	. . . . . 6 |- ( E. y e. S (inl ` m ) = ( F ` y ) <-> E. y ( y e. S /\ (inl ` m ) = ( F ` y ) ) )
123	121, 122	sylibr 133	. . . . 5 |- ( ( ph /\ m e. A ) -> E. y e. S (inl ` m ) = ( F ` y ) )
124		f1ocnvfv1 5756	. . . . . . . . . 10 |- ( (inl : _V -1-1-onto-> ( { (/) } X. _V ) /\ m e. _V ) -> ( `'inl ` (inl ` m ) ) = m )
125	5, 108, 124	mp2an 424	. . . . . . . . 9 |- ( `'inl ` (inl ` m ) ) = m
126		simpr 109	. . . . . . . . . 10 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> (inl ` m ) = ( F ` y ) )
127	126	fveq2d 5500	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> ( `'inl ` (inl ` m ) ) = ( `'inl ` ( F ` y ) ) )
128	125, 127	eqtr3id 2217	. . . . . . . 8 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> m = ( `'inl ` ( F ` y ) ) )
129	13	fveq1i 5497	. . . . . . . . . 10 |- ( G ` y ) = ( ( `'inl o. F ) ` y )
130	18	ad2antrr 485	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> F : om --> ( A ⊔ 1o ) )
131	3	sseli 3143	. . . . . . . . . . . 12 |- ( y e. S -> y e. om )
132	131	adantl 275	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> y e. om )
133		fvco3 5567	. . . . . . . . . . 11 |- ( ( F : om --> ( A ⊔ 1o ) /\ y e. om ) -> ( ( `'inl o. F ) ` y ) = ( `'inl ` ( F ` y ) ) )
134	130, 132, 133	syl2anc 409	. . . . . . . . . 10 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> ( ( `'inl o. F ) ` y ) = ( `'inl ` ( F ` y ) ) )
135	129, 134	eqtrid 2215	. . . . . . . . 9 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> ( G ` y ) = ( `'inl ` ( F ` y ) ) )
136	135	adantr 274	. . . . . . . 8 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> ( G ` y ) = ( `'inl ` ( F ` y ) ) )
137	128, 136	eqtr4d 2206	. . . . . . 7 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> m = ( G ` y ) )
138	137	ex 114	. . . . . 6 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> ( (inl ` m ) = ( F ` y ) -> m = ( G ` y ) ) )
139	138	reximdva 2572	. . . . 5 |- ( ( ph /\ m e. A ) -> ( E. y e. S (inl ` m ) = ( F ` y ) -> E. y e. S m = ( G ` y ) ) )
140	123, 139	mpd 13	. . . 4 |- ( ( ph /\ m e. A ) -> E. y e. S m = ( G ` y ) )
141	140	ralrimiva 2543	. . 3 |- ( ph -> A. m e. A E. y e. S m = ( G ` y ) )
142		dffo3 5643	. . 3 |- ( G : S -onto-> A <-> ( G : S --> A /\ A. m e. A E. y e. S m = ( G ` y ) ) )
143	97, 141, 142	sylanbrc 415	. 2 |- ( ph -> G : S -onto-> A )
144	53, 55	bitr3i 185	. . . . . . 7 |- ( ( F ` n ) e. ( A ⊔ 1o ) <-> ( ( F ` n ) e. (inl " A ) \/ ( F ` n ) e. (inr " 1o ) ) )
145	51, 144	sylib 121	. . . . . 6 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) \/ ( F ` n ) e. (inr " 1o ) ) )
146	40	orim2i 756	. . . . . 6 |- ( ( ( F ` n ) e. (inl " A ) \/ ( F ` n ) e. (inr " 1o ) ) -> ( ( F ` n ) e. (inl " A ) \/ -. ( F ` n ) e. (inl " A ) ) )
147	145, 146	syl 14	. . . . 5 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) \/ -. ( F ` n ) e. (inl " A ) ) )
148		df-dc 830	. . . . 5 |- (DECID ( F ` n ) e. (inl " A ) <-> ( ( F ` n ) e. (inl " A ) \/ -. ( F ` n ) e. (inl " A ) ) )
149	147, 148	sylibr 133	. . . 4 |- ( ( ph /\ n e. om ) -> DECID ( F ` n ) e. (inl " A ) )
150		ibar 299	. . . . . . 7 |- ( n e. om -> ( ( F ` n ) e. (inl " A ) <-> ( n e. om /\ ( F ` n ) e. (inl " A ) ) ) )
151	150	adantl 275	. . . . . 6 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) <-> ( n e. om /\ ( F ` n ) e. (inl " A ) ) ) )
152	151, 64	bitr4di 197	. . . . 5 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) <-> n e. S ) )
153	152	dcbid 833	. . . 4 |- ( ( ph /\ n e. om ) -> (DECID ( F ` n ) e. (inl " A ) <-> DECID n e. S ) )
154	149, 153	mpbid 146	. . 3 |- ( ( ph /\ n e. om ) -> DECID n e. S )
155	154	ralrimiva 2543	. 2 |- ( ph -> A. n e. om DECID n e. S )
156	4, 143, 155	3jca 1172	1 |- ( ph -> ( S C_ om /\ G : S -onto-> A /\ A. n e. om DECID n e. S ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 703  DECID wdc 829   /\ w3a 973   = wceq 1348   E.wex 1485   e. wcel 2141   A.wral 2448   E.wrex 2449   {crab 2452   _Vcvv 2730   u. cun 3119   i^i cin 3120   C_ wss 3121   (/)c0 3414   {csn 3583   omcom 4574   X. cxp 4609   `'ccnv 4610   dom cdm 4611   ran crn 4612   "cima 4614   o. ccom 4615   Fun wfun 5192   Fn wfn 5193   -->wf 5194   -onto->wfo 5196   -1-1-onto->wf1o 5197   ` cfv 5198   1oc1o 6388   ⊔ cdju 7014  inlcinl 7022  inrcinr 7023

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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418

This theorem depends on definitions:  df-bi 116  df-dc 830  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-iord 4351  df-on 4353  df-suc 4356  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-1st 6119  df-2nd 6120  df-1o 6395  df-dju 7015  df-inl 7024  df-inr 7025

This theorem is referenced by:  ctssdclemr  7089  ctiunct  12395