Theorem ctssdccl 7370

Description: A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7372 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 3313	. . . 4 |- { x e. om | ( F ` x ) e. (inl " A ) } C_ om
3	1, 2	eqsstri 3260	. . 3 |- S C_ om
4	3	a1i 9	. 2 |- ( ph -> S C_ om )
5		djulf1o 7317	. . . . . . 7 |- inl : _V -1-1-onto-> ( { (/) } X. _V )
6		f1ocnv 5605	. . . . . . 7 |- (inl : _V -1-1-onto-> ( { (/) } X. _V ) -> `'inl : ( { (/) } X. _V ) -1-1-onto-> _V )
7		f1ofun 5594	. . . . . . 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 5569	. . . . . . 7 |- ( F : om -onto-> ( A ⊔ 1o ) -> Fun F )
11	9, 10	syl 14	. . . . . 6 |- ( ph -> Fun F )
12		funco 5373	. . . . . . 7 |- ( ( Fun `'inl /\ Fun F ) -> Fun ( `'inl o. F ) )
13		ctssdccl.g	. . . . . . . 8 |- G = ( `'inl o. F )
14	13	funeqi 5354	. . . . . . 7 |- ( Fun G <-> Fun ( `'inl o. F ) )
15	12, 14	sylibr 134	. . . . . 6 |- ( ( Fun `'inl /\ Fun F ) -> Fun G )
16	8, 11, 15	sylancr 414	. . . . 5 |- ( ph -> Fun G )
17		fof 5568	. . . . . . . . . . . 12 |- ( F : om -onto-> ( A ⊔ 1o ) -> F : om --> ( A ⊔ 1o ) )
18	9, 17	syl 14	. . . . . . . . . . 11 |- ( ph -> F : om --> ( A ⊔ 1o ) )
19	18	fdmd 5496	. . . . . . . . . 10 |- ( ph -> dom F = om )
20	19	eleq2d 2301	. . . . . . . . 9 |- ( ph -> ( n e. dom F <-> n e. om ) )
21	20	anbi1d 465	. . . . . . . 8 |- ( ph -> ( ( n e. dom F /\ ( F ` n ) e. dom `'inl ) <-> ( n e. om /\ ( F ` n ) e. dom `'inl ) ) )
22		dmcoss 5008	. . . . . . . . . . . 12 |- dom ( `'inl o. F ) C_ dom F
23	22	sseli 3224	. . . . . . . . . . 11 |- ( n e. dom ( `'inl o. F ) -> n e. dom F )
24	23	pm4.71ri 392	. . . . . . . . . 10 |- ( n e. dom ( `'inl o. F ) <-> ( n e. dom F /\ n e. dom ( `'inl o. F ) ) )
25		dmfco 5723	. . . . . . . . . . 11 |- ( ( Fun F /\ n e. dom F ) -> ( n e. dom ( `'inl o. F ) <-> ( F ` n ) e. dom `'inl ) )
26	25	pm5.32da 452	. . . . . . . . . 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	bitrid 192	. . . . . . . . 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 110	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inl " A ) ) -> ( F ` n ) e. (inl " A ) )
30		imassrn 5093	. . . . . . . . . . . . . 14 |- (inl " A ) C_ ran inl
31	30	sseli 3224	. . . . . . . . . . . . 13 |- ( ( F ` n ) e. (inl " A ) -> ( F ` n ) e. ran inl )
32	31	adantl 277	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inl " A ) ) -> ( F ` n ) e. ran inl )
33		df-rn 4742	. . . . . . . . . . . . 13 |- ran inl = dom `'inl
34	33	eleq2i 2298	. . . . . . . . . . . 12 |- ( ( F ` n ) e. ran inl <-> ( F ` n ) e. dom `'inl )
35	32, 34	sylib 122	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inl " A ) ) -> ( F ` n ) e. dom `'inl )
36	29, 35	2thd 175	. . . . . . . . . 10 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inl " A ) ) -> ( ( F ` n ) e. (inl " A ) <-> ( F ` n ) e. dom `'inl ) )
37		djuin 7323	. . . . . . . . . . . . . 14 |- ( (inl " A ) i^i (inr " 1o ) ) = (/)
38		disjel 3551	. . . . . . . . . . . . . 14 |- ( ( ( (inl " A ) i^i (inr " 1o ) ) = (/) /\ ( F ` n ) e. (inl " A ) ) -> -. ( F ` n ) e. (inr " 1o ) )
39	37, 38	mpan 424	. . . . . . . . . . . . 13 |- ( ( F ` n ) e. (inl " A ) -> -. ( F ` n ) e. (inr " 1o ) )
40	39	con2i 632	. . . . . . . . . . . 12 |- ( ( F ` n ) e. (inr " 1o ) -> -. ( F ` n ) e. (inl " A ) )
41	40	adantl 277	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> -. ( F ` n ) e. (inl " A ) )
42		djuin 7323	. . . . . . . . . . . . . . . 16 |- ( (inl " _V ) i^i (inr " 1o ) ) = (/)
43		disjel 3551	. . . . . . . . . . . . . . . 16 |- ( ( ( (inl " _V ) i^i (inr " 1o ) ) = (/) /\ ( F ` n ) e. (inl " _V ) ) -> -. ( F ` n ) e. (inr " 1o ) )
44	42, 43	mpan 424	. . . . . . . . . . . . . . 15 |- ( ( F ` n ) e. (inl " _V ) -> -. ( F ` n ) e. (inr " 1o ) )
45		dfrn4 5204	. . . . . . . . . . . . . . 15 |- ran inl = (inl " _V )
46	44, 45	eleq2s 2326	. . . . . . . . . . . . . 14 |- ( ( F ` n ) e. ran inl -> -. ( F ` n ) e. (inr " 1o ) )
47	46	con2i 632	. . . . . . . . . . . . 13 |- ( ( F ` n ) e. (inr " 1o ) -> -. ( F ` n ) e. ran inl )
48	47	adantl 277	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> -. ( F ` n ) e. ran inl )
49	48, 34	sylnib 683	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> -. ( F ` n ) e. dom `'inl )
50	41, 49	2falsed 710	. . . . . . . . . 10 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> ( ( F ` n ) e. (inl " A ) <-> ( F ` n ) e. dom `'inl ) )
51	18	ffvelcdmda 5790	. . . . . . . . . . . 12 |- ( ( ph /\ n e. om ) -> ( F ` n ) e. ( A ⊔ 1o ) )
52		djuun 7326	. . . . . . . . . . . . 13 |- ( (inl " A ) u. (inr " 1o ) ) = ( A ⊔ 1o )
53	52	eleq2i 2298	. . . . . . . . . . . 12 |- ( ( F ` n ) e. ( (inl " A ) u. (inr " 1o ) ) <-> ( F ` n ) e. ( A ⊔ 1o ) )
54	51, 53	sylibr 134	. . . . . . . . . . 11 |- ( ( ph /\ n e. om ) -> ( F ` n ) e. ( (inl " A ) u. (inr " 1o ) ) )
55		elun 3350	. . . . . . . . . . 11 |- ( ( F ` n ) e. ( (inl " A ) u. (inr " 1o ) ) <-> ( ( F ` n ) e. (inl " A ) \/ ( F ` n ) e. (inr " 1o ) ) )
56	54, 55	sylib 122	. . . . . . . . . 10 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) \/ ( F ` n ) e. (inr " 1o ) ) )
57	36, 50, 56	mpjaodan 806	. . . . . . . . 9 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) <-> ( F ` n ) e. dom `'inl ) )
58	57	pm5.32da 452	. . . . . . . 8 |- ( ph -> ( ( n e. om /\ ( F ` n ) e. (inl " A ) ) <-> ( n e. om /\ ( F ` n ) e. dom `'inl ) ) )
59	21, 28, 58	3bitr4d 220	. . . . . . 7 |- ( ph -> ( n e. dom ( `'inl o. F ) <-> ( n e. om /\ ( F ` n ) e. (inl " A ) ) ) )
60	13	dmeqi 4938	. . . . . . . 8 |- dom G = dom ( `'inl o. F )
61	60	eleq2i 2298	. . . . . . 7 |- ( n e. dom G <-> n e. dom ( `'inl o. F ) )
62		fveq2 5648	. . . . . . . . 9 |- ( x = n -> ( F ` x ) = ( F ` n ) )
63	62	eleq1d 2300	. . . . . . . 8 |- ( x = n -> ( ( F ` x ) e. (inl " A ) <-> ( F ` n ) e. (inl " A ) ) )
64	63, 1	elrab2 2966	. . . . . . 7 |- ( n e. S <-> ( n e. om /\ ( F ` n ) e. (inl " A ) ) )
65	59, 61, 64	3bitr4g 223	. . . . . 6 |- ( ph -> ( n e. dom G <-> n e. S ) )
66	65	eqrdv 2229	. . . . 5 |- ( ph -> dom G = S )
67		df-fn 5336	. . . . 5 |- ( G Fn S <-> ( Fun G /\ dom G = S ) )
68	16, 66, 67	sylanbrc 417	. . . 4 |- ( ph -> G Fn S )
69	13	fveq1i 5649	. . . . . . 7 |- ( G ` m ) = ( ( `'inl o. F ) ` m )
70	18	adantr 276	. . . . . . . 8 |- ( ( ph /\ m e. S ) -> F : om --> ( A ⊔ 1o ) )
71		fveq2 5648	. . . . . . . . . . . . 13 |- ( x = m -> ( F ` x ) = ( F ` m ) )
72	71	eleq1d 2300	. . . . . . . . . . . 12 |- ( x = m -> ( ( F ` x ) e. (inl " A ) <-> ( F ` m ) e. (inl " A ) ) )
73	72, 1	elrab2 2966	. . . . . . . . . . 11 |- ( m e. S <-> ( m e. om /\ ( F ` m ) e. (inl " A ) ) )
74	73	biimpi 120	. . . . . . . . . 10 |- ( m e. S -> ( m e. om /\ ( F ` m ) e. (inl " A ) ) )
75	74	adantl 277	. . . . . . . . 9 |- ( ( ph /\ m e. S ) -> ( m e. om /\ ( F ` m ) e. (inl " A ) ) )
76	75	simpld 112	. . . . . . . 8 |- ( ( ph /\ m e. S ) -> m e. om )
77		fvco3 5726	. . . . . . . 8 |- ( ( F : om --> ( A ⊔ 1o ) /\ m e. om ) -> ( ( `'inl o. F ) ` m ) = ( `'inl ` ( F ` m ) ) )
78	70, 76, 77	syl2anc 411	. . . . . . 7 |- ( ( ph /\ m e. S ) -> ( ( `'inl o. F ) ` m ) = ( `'inl ` ( F ` m ) ) )
79	69, 78	eqtrid 2276	. . . . . 6 |- ( ( ph /\ m e. S ) -> ( G ` m ) = ( `'inl ` ( F ` m ) ) )
80		f1ofun 5594	. . . . . . . . . 10 |- (inl : _V -1-1-onto-> ( { (/) } X. _V ) -> Fun inl )
81	5, 80	ax-mp 5	. . . . . . . . 9 |- Fun inl
82		fvelima 5706	. . . . . . . . 9 |- ( ( Fun inl /\ ( F ` m ) e. (inl " A ) ) -> E. z e. A (inl ` z ) = ( F ` m ) )
83	81, 82	mpan 424	. . . . . . . 8 |- ( ( F ` m ) e. (inl " A ) -> E. z e. A (inl ` z ) = ( F ` m ) )
84	75, 83	simpl2im 386	. . . . . . 7 |- ( ( ph /\ m e. S ) -> E. z e. A (inl ` z ) = ( F ` m ) )
85		simprr 533	. . . . . . . . 9 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> (inl ` z ) = ( F ` m ) )
86	85	fveq2d 5652	. . . . . . . 8 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` (inl ` z ) ) = ( `'inl ` ( F ` m ) ) )
87		vex 2806	. . . . . . . . . 10 |- z e. _V
88		f1ocnvfv1 5928	. . . . . . . . . 10 |- ( (inl : _V -1-1-onto-> ( { (/) } X. _V ) /\ z e. _V ) -> ( `'inl ` (inl ` z ) ) = z )
89	5, 87, 88	mp2an 426	. . . . . . . . 9 |- ( `'inl ` (inl ` z ) ) = z
90		simprl 531	. . . . . . . . 9 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> z e. A )
91	89, 90	eqeltrid 2318	. . . . . . . 8 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` (inl ` z ) ) e. A )
92	86, 91	eqeltrrd 2309	. . . . . . 7 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` ( F ` m ) ) e. A )
93	84, 92	rexlimddv 2656	. . . . . 6 |- ( ( ph /\ m e. S ) -> ( `'inl ` ( F ` m ) ) e. A )
94	79, 93	eqeltrd 2308	. . . . 5 |- ( ( ph /\ m e. S ) -> ( G ` m ) e. A )
95	94	ralrimiva 2606	. . . 4 |- ( ph -> A. m e. S ( G ` m ) e. A )
96		ffnfv 5813	. . . 4 |- ( G : S --> A <-> ( G Fn S /\ A. m e. S ( G ` m ) e. A ) )
97	68, 95, 96	sylanbrc 417	. . 3 |- ( ph -> G : S --> A )
98		djulcl 7310	. . . . . . . 8 |- ( m e. A -> (inl ` m ) e. ( A ⊔ 1o ) )
99		foelrn 5903	. . . . . . . . . 10 |- ( ( F : om -onto-> ( A ⊔ 1o ) /\ (inl ` m ) e. ( A ⊔ 1o ) ) -> E. y e. om (inl ` m ) = ( F ` y ) )
100	9, 99	sylan 283	. . . . . . . . 9 |- ( ( ph /\ (inl ` m ) e. ( A ⊔ 1o ) ) -> E. y e. om (inl ` m ) = ( F ` y ) )
101		df-rex 2517	. . . . . . . . 9 |- ( E. y e. om (inl ` m ) = ( F ` y ) <-> E. y ( y e. om /\ (inl ` m ) = ( F ` y ) ) )
102	100, 101	sylib 122	. . . . . . . 8 |- ( ( ph /\ (inl ` m ) e. ( A ⊔ 1o ) ) -> E. y ( y e. om /\ (inl ` m ) = ( F ` y ) ) )
103	98, 102	sylan2 286	. . . . . . 7 |- ( ( ph /\ m e. A ) -> E. y ( y e. om /\ (inl ` m ) = ( F ` y ) ) )
104		fveq2 5648	. . . . . . . . . . . . 13 |- ( x = y -> ( F ` x ) = ( F ` y ) )
105	104	eleq1d 2300	. . . . . . . . . . . 12 |- ( x = y -> ( ( F ` x ) e. (inl " A ) <-> ( F ` y ) e. (inl " A ) ) )
106		simprl 531	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> y e. om )
107		simprr 533	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> (inl ` m ) = ( F ` y ) )
108		vex 2806	. . . . . . . . . . . . . . . 16 |- m e. _V
109		f1odm 5596	. . . . . . . . . . . . . . . . 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 2307	. . . . . . . . . . . . . . 15 |- m e. dom inl
112		funfvima 5896	. . . . . . . . . . . . . . 15 |- ( ( Fun inl /\ m e. dom inl ) -> ( m e. A -> (inl ` m ) e. (inl " A ) ) )
113	81, 111, 112	mp2an 426	. . . . . . . . . . . . . 14 |- ( m e. A -> (inl ` m ) e. (inl " A ) )
114	113	ad2antlr 489	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> (inl ` m ) e. (inl " A ) )
115	107, 114	eqeltrrd 2309	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> ( F ` y ) e. (inl " A ) )
116	105, 106, 115	elrabd 2965	. . . . . . . . . . 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 2325	. . . . . . . . . 10 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> y e. S )
118	117, 107	jca 306	. . . . . . . . 9 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> ( y e. S /\ (inl ` m ) = ( F ` y ) ) )
119	118	ex 115	. . . . . . . 8 |- ( ( ph /\ m e. A ) -> ( ( y e. om /\ (inl ` m ) = ( F ` y ) ) -> ( y e. S /\ (inl ` m ) = ( F ` y ) ) ) )
120	119	eximdv 1928	. . . . . . 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 2517	. . . . . 6 |- ( E. y e. S (inl ` m ) = ( F ` y ) <-> E. y ( y e. S /\ (inl ` m ) = ( F ` y ) ) )
123	121, 122	sylibr 134	. . . . 5 |- ( ( ph /\ m e. A ) -> E. y e. S (inl ` m ) = ( F ` y ) )
124		f1ocnvfv1 5928	. . . . . . . . . 10 |- ( (inl : _V -1-1-onto-> ( { (/) } X. _V ) /\ m e. _V ) -> ( `'inl ` (inl ` m ) ) = m )
125	5, 108, 124	mp2an 426	. . . . . . . . 9 |- ( `'inl ` (inl ` m ) ) = m
126		simpr 110	. . . . . . . . . 10 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> (inl ` m ) = ( F ` y ) )
127	126	fveq2d 5652	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> ( `'inl ` (inl ` m ) ) = ( `'inl ` ( F ` y ) ) )
128	125, 127	eqtr3id 2278	. . . . . . . 8 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> m = ( `'inl ` ( F ` y ) ) )
129	13	fveq1i 5649	. . . . . . . . . 10 |- ( G ` y ) = ( ( `'inl o. F ) ` y )
130	18	ad2antrr 488	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> F : om --> ( A ⊔ 1o ) )
131	3	sseli 3224	. . . . . . . . . . . 12 |- ( y e. S -> y e. om )
132	131	adantl 277	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> y e. om )
133		fvco3 5726	. . . . . . . . . . 11 |- ( ( F : om --> ( A ⊔ 1o ) /\ y e. om ) -> ( ( `'inl o. F ) ` y ) = ( `'inl ` ( F ` y ) ) )
134	130, 132, 133	syl2anc 411	. . . . . . . . . 10 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> ( ( `'inl o. F ) ` y ) = ( `'inl ` ( F ` y ) ) )
135	129, 134	eqtrid 2276	. . . . . . . . 9 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> ( G ` y ) = ( `'inl ` ( F ` y ) ) )
136	135	adantr 276	. . . . . . . 8 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> ( G ` y ) = ( `'inl ` ( F ` y ) ) )
137	128, 136	eqtr4d 2267	. . . . . . 7 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> m = ( G ` y ) )
138	137	ex 115	. . . . . 6 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> ( (inl ` m ) = ( F ` y ) -> m = ( G ` y ) ) )
139	138	reximdva 2635	. . . . 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 2606	. . 3 |- ( ph -> A. m e. A E. y e. S m = ( G ` y ) )
142		dffo3 5802	. . 3 |- ( G : S -onto-> A <-> ( G : S --> A /\ A. m e. A E. y e. S m = ( G ` y ) ) )
143	97, 141, 142	sylanbrc 417	. 2 |- ( ph -> G : S -onto-> A )
144	53, 55	bitr3i 186	. . . . . . 7 |- ( ( F ` n ) e. ( A ⊔ 1o ) <-> ( ( F ` n ) e. (inl " A ) \/ ( F ` n ) e. (inr " 1o ) ) )
145	51, 144	sylib 122	. . . . . 6 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) \/ ( F ` n ) e. (inr " 1o ) ) )
146	40	orim2i 769	. . . . . 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 843	. . . . 5 |- (DECID ( F ` n ) e. (inl " A ) <-> ( ( F ` n ) e. (inl " A ) \/ -. ( F ` n ) e. (inl " A ) ) )
149	147, 148	sylibr 134	. . . 4 |- ( ( ph /\ n e. om ) -> DECID ( F ` n ) e. (inl " A ) )
150		ibar 301	. . . . . . 7 |- ( n e. om -> ( ( F ` n ) e. (inl " A ) <-> ( n e. om /\ ( F ` n ) e. (inl " A ) ) ) )
151	150	adantl 277	. . . . . 6 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) <-> ( n e. om /\ ( F ` n ) e. (inl " A ) ) ) )
152	151, 64	bitr4di 198	. . . . 5 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) <-> n e. S ) )
153	152	dcbid 846	. . . 4 |- ( ( ph /\ n e. om ) -> (DECID ( F ` n ) e. (inl " A ) <-> DECID n e. S ) )
154	149, 153	mpbid 147	. . 3 |- ( ( ph /\ n e. om ) -> DECID n e. S )
155	154	ralrimiva 2606	. 2 |- ( ph -> A. n e. om DECID n e. S )
156	4, 143, 155	3jca 1204	1 |- ( ph -> ( S C_ om /\ G : S -onto-> A /\ A. n e. om DECID n e. S ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 716  DECID wdc 842   /\ w3a 1005   = wceq 1398   E.wex 1541   e. wcel 2202   A.wral 2511   E.wrex 2512   {crab 2515   _Vcvv 2803   u. cun 3199   i^i cin 3200   C_ wss 3201   (/)c0 3496   {csn 3673   omcom 4694   X. cxp 4729   `'ccnv 4730   dom cdm 4731   ran crn 4732   "cima 4734   o. ccom 4735   Fun wfun 5327   Fn wfn 5328   -->wf 5329   -onto->wfo 5331   -1-1-onto->wf1o 5332   ` cfv 5333   1oc1o 6618   ⊔ cdju 7296  inlcinl 7304  inrcinr 7305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-nul 4220  ax-pow 4270  ax-pr 4305  ax-un 4536

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-ral 2516  df-rex 2517  df-rab 2520  df-v 2805  df-sbc 3033  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-nul 3497  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-mpt 4157  df-tr 4193  df-id 4396  df-iord 4469  df-on 4471  df-suc 4474  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-res 4743  df-ima 4744  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-f1 5338  df-fo 5339  df-f1o 5340  df-fv 5341  df-1st 6312  df-2nd 6313  df-1o 6625  df-dju 7297  df-inl 7306  df-inr 7307

This theorem is referenced by:  ctssdclemr  7371  ctiunct  13141