Theorem ctssdccl 6996

Description: A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 6998 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 3182	. . . 4 |- { x e. om | ( F ` x ) e. (inl " A ) } C_ om
3	1, 2	eqsstri 3129	. . 3 |- S C_ om
4	3	a1i 9	. 2 |- ( ph -> S C_ om )
5		djulf1o 6943	. . . . . . 7 |- inl : _V -1-1-onto-> ( { (/) } X. _V )
6		f1ocnv 5380	. . . . . . 7 |- (inl : _V -1-1-onto-> ( { (/) } X. _V ) -> `'inl : ( { (/) } X. _V ) -1-1-onto-> _V )
7		f1ofun 5369	. . . . . . 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 5346	. . . . . . 7 |- ( F : om -onto-> ( A ⊔ 1o ) -> Fun F )
11	9, 10	syl 14	. . . . . 6 |- ( ph -> Fun F )
12		funco 5163	. . . . . . 7 |- ( ( Fun `'inl /\ Fun F ) -> Fun ( `'inl o. F ) )
13		ctssdccl.g	. . . . . . . 8 |- G = ( `'inl o. F )
14	13	funeqi 5144	. . . . . . 7 |- ( Fun G <-> Fun ( `'inl o. F ) )
15	12, 14	sylibr 133	. . . . . 6 |- ( ( Fun `'inl /\ Fun F ) -> Fun G )
16	8, 11, 15	sylancr 410	. . . . 5 |- ( ph -> Fun G )
17		fof 5345	. . . . . . . . . . . 12 |- ( F : om -onto-> ( A ⊔ 1o ) -> F : om --> ( A ⊔ 1o ) )
18	9, 17	syl 14	. . . . . . . . . . 11 |- ( ph -> F : om --> ( A ⊔ 1o ) )
19	18	fdmd 5279	. . . . . . . . . 10 |- ( ph -> dom F = om )
20	19	eleq2d 2209	. . . . . . . . 9 |- ( ph -> ( n e. dom F <-> n e. om ) )
21	20	anbi1d 460	. . . . . . . 8 |- ( ph -> ( ( n e. dom F /\ ( F ` n ) e. dom `'inl ) <-> ( n e. om /\ ( F ` n ) e. dom `'inl ) ) )
22		dmcoss 4808	. . . . . . . . . . . 12 |- dom ( `'inl o. F ) C_ dom F
23	22	sseli 3093	. . . . . . . . . . 11 |- ( n e. dom ( `'inl o. F ) -> n e. dom F )
24	23	pm4.71ri 389	. . . . . . . . . 10 |- ( n e. dom ( `'inl o. F ) <-> ( n e. dom F /\ n e. dom ( `'inl o. F ) ) )
25		dmfco 5489	. . . . . . . . . . 11 |- ( ( Fun F /\ n e. dom F ) -> ( n e. dom ( `'inl o. F ) <-> ( F ` n ) e. dom `'inl ) )
26	25	pm5.32da 447	. . . . . . . . . 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 4892	. . . . . . . . . . . . . 14 |- (inl " A ) C_ ran inl
31	30	sseli 3093	. . . . . . . . . . . . 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 4550	. . . . . . . . . . . . 13 |- ran inl = dom `'inl
34	33	eleq2i 2206	. . . . . . . . . . . 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 6949	. . . . . . . . . . . . . 14 |- ( (inl " A ) i^i (inr " 1o ) ) = (/)
38		disjel 3417	. . . . . . . . . . . . . 14 |- ( ( ( (inl " A ) i^i (inr " 1o ) ) = (/) /\ ( F ` n ) e. (inl " A ) ) -> -. ( F ` n ) e. (inr " 1o ) )
39	37, 38	mpan 420	. . . . . . . . . . . . 13 |- ( ( F ` n ) e. (inl " A ) -> -. ( F ` n ) e. (inr " 1o ) )
40	39	con2i 616	. . . . . . . . . . . 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 6949	. . . . . . . . . . . . . . . 16 |- ( (inl " _V ) i^i (inr " 1o ) ) = (/)
43		disjel 3417	. . . . . . . . . . . . . . . 16 |- ( ( ( (inl " _V ) i^i (inr " 1o ) ) = (/) /\ ( F ` n ) e. (inl " _V ) ) -> -. ( F ` n ) e. (inr " 1o ) )
44	42, 43	mpan 420	. . . . . . . . . . . . . . 15 |- ( ( F ` n ) e. (inl " _V ) -> -. ( F ` n ) e. (inr " 1o ) )
45		dfrn4 4999	. . . . . . . . . . . . . . 15 |- ran inl = (inl " _V )
46	44, 45	eleq2s 2234	. . . . . . . . . . . . . 14 |- ( ( F ` n ) e. ran inl -> -. ( F ` n ) e. (inr " 1o ) )
47	46	con2i 616	. . . . . . . . . . . . 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 665	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> -. ( F ` n ) e. dom `'inl )
50	41, 49	2falsed 691	. . . . . . . . . 10 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> ( ( F ` n ) e. (inl " A ) <-> ( F ` n ) e. dom `'inl ) )
51	18	ffvelrnda 5555	. . . . . . . . . . . 12 |- ( ( ph /\ n e. om ) -> ( F ` n ) e. ( A ⊔ 1o ) )
52		djuun 6952	. . . . . . . . . . . . 13 |- ( (inl " A ) u. (inr " 1o ) ) = ( A ⊔ 1o )
53	52	eleq2i 2206	. . . . . . . . . . . 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 3217	. . . . . . . . . . 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 787	. . . . . . . . 9 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) <-> ( F ` n ) e. dom `'inl ) )
58	57	pm5.32da 447	. . . . . . . 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 4740	. . . . . . . 8 |- dom G = dom ( `'inl o. F )
61	60	eleq2i 2206	. . . . . . 7 |- ( n e. dom G <-> n e. dom ( `'inl o. F ) )
62		fveq2 5421	. . . . . . . . 9 |- ( x = n -> ( F ` x ) = ( F ` n ) )
63	62	eleq1d 2208	. . . . . . . 8 |- ( x = n -> ( ( F ` x ) e. (inl " A ) <-> ( F ` n ) e. (inl " A ) ) )
64	63, 1	elrab2 2843	. . . . . . 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 2137	. . . . 5 |- ( ph -> dom G = S )
67		df-fn 5126	. . . . 5 |- ( G Fn S <-> ( Fun G /\ dom G = S ) )
68	16, 66, 67	sylanbrc 413	. . . 4 |- ( ph -> G Fn S )
69	13	fveq1i 5422	. . . . . . 7 |- ( G ` m ) = ( ( `'inl o. F ) ` m )
70	18	adantr 274	. . . . . . . 8 |- ( ( ph /\ m e. S ) -> F : om --> ( A ⊔ 1o ) )
71		fveq2 5421	. . . . . . . . . . . . 13 |- ( x = m -> ( F ` x ) = ( F ` m ) )
72	71	eleq1d 2208	. . . . . . . . . . . 12 |- ( x = m -> ( ( F ` x ) e. (inl " A ) <-> ( F ` m ) e. (inl " A ) ) )
73	72, 1	elrab2 2843	. . . . . . . . . . 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 5492	. . . . . . . 8 |- ( ( F : om --> ( A ⊔ 1o ) /\ m e. om ) -> ( ( `'inl o. F ) ` m ) = ( `'inl ` ( F ` m ) ) )
78	70, 76, 77	syl2anc 408	. . . . . . 7 |- ( ( ph /\ m e. S ) -> ( ( `'inl o. F ) ` m ) = ( `'inl ` ( F ` m ) ) )
79	69, 78	syl5eq 2184	. . . . . 6 |- ( ( ph /\ m e. S ) -> ( G ` m ) = ( `'inl ` ( F ` m ) ) )
80		f1ofun 5369	. . . . . . . . . 10 |- (inl : _V -1-1-onto-> ( { (/) } X. _V ) -> Fun inl )
81	5, 80	ax-mp 5	. . . . . . . . 9 |- Fun inl
82		fvelima 5473	. . . . . . . . 9 |- ( ( Fun inl /\ ( F ` m ) e. (inl " A ) ) -> E. z e. A (inl ` z ) = ( F ` m ) )
83	81, 82	mpan 420	. . . . . . . 8 |- ( ( F ` m ) e. (inl " A ) -> E. z e. A (inl ` z ) = ( F ` m ) )
84	75, 83	simpl2im 383	. . . . . . 7 |- ( ( ph /\ m e. S ) -> E. z e. A (inl ` z ) = ( F ` m ) )
85		simprr 521	. . . . . . . . 9 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> (inl ` z ) = ( F ` m ) )
86	85	fveq2d 5425	. . . . . . . 8 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` (inl ` z ) ) = ( `'inl ` ( F ` m ) ) )
87		vex 2689	. . . . . . . . . 10 |- z e. _V
88		f1ocnvfv1 5678	. . . . . . . . . 10 |- ( (inl : _V -1-1-onto-> ( { (/) } X. _V ) /\ z e. _V ) -> ( `'inl ` (inl ` z ) ) = z )
89	5, 87, 88	mp2an 422	. . . . . . . . 9 |- ( `'inl ` (inl ` z ) ) = z
90		simprl 520	. . . . . . . . 9 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> z e. A )
91	89, 90	eqeltrid 2226	. . . . . . . 8 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` (inl ` z ) ) e. A )
92	86, 91	eqeltrrd 2217	. . . . . . 7 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` ( F ` m ) ) e. A )
93	84, 92	rexlimddv 2554	. . . . . 6 |- ( ( ph /\ m e. S ) -> ( `'inl ` ( F ` m ) ) e. A )
94	79, 93	eqeltrd 2216	. . . . 5 |- ( ( ph /\ m e. S ) -> ( G ` m ) e. A )
95	94	ralrimiva 2505	. . . 4 |- ( ph -> A. m e. S ( G ` m ) e. A )
96		ffnfv 5578	. . . 4 |- ( G : S --> A <-> ( G Fn S /\ A. m e. S ( G ` m ) e. A ) )
97	68, 95, 96	sylanbrc 413	. . 3 |- ( ph -> G : S --> A )
98		djulcl 6936	. . . . . . . 8 |- ( m e. A -> (inl ` m ) e. ( A ⊔ 1o ) )
99		foelrn 5654	. . . . . . . . . 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 2422	. . . . . . . . 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 5421	. . . . . . . . . . . . 13 |- ( x = y -> ( F ` x ) = ( F ` y ) )
105	104	eleq1d 2208	. . . . . . . . . . . 12 |- ( x = y -> ( ( F ` x ) e. (inl " A ) <-> ( F ` y ) e. (inl " A ) ) )
106		simprl 520	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> y e. om )
107		simprr 521	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> (inl ` m ) = ( F ` y ) )
108		vex 2689	. . . . . . . . . . . . . . . 16 |- m e. _V
109		f1odm 5371	. . . . . . . . . . . . . . . . 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 2215	. . . . . . . . . . . . . . 15 |- m e. dom inl
112		funfvima 5649	. . . . . . . . . . . . . . 15 |- ( ( Fun inl /\ m e. dom inl ) -> ( m e. A -> (inl ` m ) e. (inl " A ) ) )
113	81, 111, 112	mp2an 422	. . . . . . . . . . . . . 14 |- ( m e. A -> (inl ` m ) e. (inl " A ) )
114	113	ad2antlr 480	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> (inl ` m ) e. (inl " A ) )
115	107, 114	eqeltrrd 2217	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> ( F ` y ) e. (inl " A ) )
116	105, 106, 115	elrabd 2842	. . . . . . . . . . 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 2233	. . . . . . . . . 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 1852	. . . . . . 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 2422	. . . . . 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 5678	. . . . . . . . . 10 |- ( (inl : _V -1-1-onto-> ( { (/) } X. _V ) /\ m e. _V ) -> ( `'inl ` (inl ` m ) ) = m )
125	5, 108, 124	mp2an 422	. . . . . . . . 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 5425	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> ( `'inl ` (inl ` m ) ) = ( `'inl ` ( F ` y ) ) )
128	125, 127	syl5eqr 2186	. . . . . . . 8 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> m = ( `'inl ` ( F ` y ) ) )
129	13	fveq1i 5422	. . . . . . . . . 10 |- ( G ` y ) = ( ( `'inl o. F ) ` y )
130	18	ad2antrr 479	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> F : om --> ( A ⊔ 1o ) )
131	3	sseli 3093	. . . . . . . . . . . 12 |- ( y e. S -> y e. om )
132	131	adantl 275	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> y e. om )
133		fvco3 5492	. . . . . . . . . . 11 |- ( ( F : om --> ( A ⊔ 1o ) /\ y e. om ) -> ( ( `'inl o. F ) ` y ) = ( `'inl ` ( F ` y ) ) )
134	130, 132, 133	syl2anc 408	. . . . . . . . . 10 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> ( ( `'inl o. F ) ` y ) = ( `'inl ` ( F ` y ) ) )
135	129, 134	syl5eq 2184	. . . . . . . . 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 2175	. . . . . . 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 2534	. . . . 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 2505	. . 3 |- ( ph -> A. m e. A E. y e. S m = ( G ` y ) )
142		dffo3 5567	. . 3 |- ( G : S -onto-> A <-> ( G : S --> A /\ A. m e. A E. y e. S m = ( G ` y ) ) )
143	97, 141, 142	sylanbrc 413	. 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 750	. . . . . 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 820	. . . . 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	syl6bbr 197	. . . . 5 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) <-> n e. S ) )
153	152	dcbid 823	. . . 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 2505	. 2 |- ( ph -> A. n e. om DECID n e. S )
156	4, 143, 155	3jca 1161	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 697  DECID wdc 819   /\ w3a 962   = wceq 1331   E.wex 1468   e. wcel 1480   A.wral 2416   E.wrex 2417   {crab 2420   _Vcvv 2686   u. cun 3069   i^i cin 3070   C_ wss 3071   (/)c0 3363   {csn 3527   omcom 4504   X. cxp 4537   `'ccnv 4538   dom cdm 4539   ran crn 4540   "cima 4542   o. ccom 4543   Fun wfun 5117   Fn wfn 5118   -->wf 5119   -onto->wfo 5121   -1-1-onto->wf1o 5122   ` cfv 5123   1oc1o 6306   ⊔ cdju 6922  inlcinl 6930  inrcinr 6931

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355

This theorem depends on definitions:  df-bi 116  df-dc 820  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-rab 2425  df-v 2688  df-sbc 2910  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-suc 4293  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-1st 6038  df-2nd 6039  df-1o 6313  df-dju 6923  df-inl 6932  df-inr 6933

This theorem is referenced by:  ctssdclemr  6997  ctiunct  11953