Theorem ctssdccl 7170

Description: A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7172 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 3264	. . . 4 |- { x e. om | ( F ` x ) e. (inl " A ) } C_ om
3	1, 2	eqsstri 3211	. . 3 |- S C_ om
4	3	a1i 9	. 2 |- ( ph -> S C_ om )
5		djulf1o 7117	. . . . . . 7 |- inl : _V -1-1-onto-> ( { (/) } X. _V )
6		f1ocnv 5513	. . . . . . 7 |- (inl : _V -1-1-onto-> ( { (/) } X. _V ) -> `'inl : ( { (/) } X. _V ) -1-1-onto-> _V )
7		f1ofun 5502	. . . . . . 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 5477	. . . . . . 7 |- ( F : om -onto-> ( A ⊔ 1o ) -> Fun F )
11	9, 10	syl 14	. . . . . 6 |- ( ph -> Fun F )
12		funco 5294	. . . . . . 7 |- ( ( Fun `'inl /\ Fun F ) -> Fun ( `'inl o. F ) )
13		ctssdccl.g	. . . . . . . 8 |- G = ( `'inl o. F )
14	13	funeqi 5275	. . . . . . 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 5476	. . . . . . . . . . . 12 |- ( F : om -onto-> ( A ⊔ 1o ) -> F : om --> ( A ⊔ 1o ) )
18	9, 17	syl 14	. . . . . . . . . . 11 |- ( ph -> F : om --> ( A ⊔ 1o ) )
19	18	fdmd 5410	. . . . . . . . . 10 |- ( ph -> dom F = om )
20	19	eleq2d 2263	. . . . . . . . 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 4931	. . . . . . . . . . . 12 |- dom ( `'inl o. F ) C_ dom F
23	22	sseli 3175	. . . . . . . . . . 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 5625	. . . . . . . . . . 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 5016	. . . . . . . . . . . . . 14 |- (inl " A ) C_ ran inl
31	30	sseli 3175	. . . . . . . . . . . . 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 4670	. . . . . . . . . . . . 13 |- ran inl = dom `'inl
34	33	eleq2i 2260	. . . . . . . . . . . 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 7123	. . . . . . . . . . . . . 14 |- ( (inl " A ) i^i (inr " 1o ) ) = (/)
38		disjel 3501	. . . . . . . . . . . . . 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 628	. . . . . . . . . . . 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 7123	. . . . . . . . . . . . . . . 16 |- ( (inl " _V ) i^i (inr " 1o ) ) = (/)
43		disjel 3501	. . . . . . . . . . . . . . . 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 5126	. . . . . . . . . . . . . . 15 |- ran inl = (inl " _V )
46	44, 45	eleq2s 2288	. . . . . . . . . . . . . 14 |- ( ( F ` n ) e. ran inl -> -. ( F ` n ) e. (inr " 1o ) )
47	46	con2i 628	. . . . . . . . . . . . 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 677	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> -. ( F ` n ) e. dom `'inl )
50	41, 49	2falsed 703	. . . . . . . . . 10 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> ( ( F ` n ) e. (inl " A ) <-> ( F ` n ) e. dom `'inl ) )
51	18	ffvelcdmda 5693	. . . . . . . . . . . 12 |- ( ( ph /\ n e. om ) -> ( F ` n ) e. ( A ⊔ 1o ) )
52		djuun 7126	. . . . . . . . . . . . 13 |- ( (inl " A ) u. (inr " 1o ) ) = ( A ⊔ 1o )
53	52	eleq2i 2260	. . . . . . . . . . . 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 3300	. . . . . . . . . . 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 799	. . . . . . . . 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 4863	. . . . . . . 8 |- dom G = dom ( `'inl o. F )
61	60	eleq2i 2260	. . . . . . 7 |- ( n e. dom G <-> n e. dom ( `'inl o. F ) )
62		fveq2 5554	. . . . . . . . 9 |- ( x = n -> ( F ` x ) = ( F ` n ) )
63	62	eleq1d 2262	. . . . . . . 8 |- ( x = n -> ( ( F ` x ) e. (inl " A ) <-> ( F ` n ) e. (inl " A ) ) )
64	63, 1	elrab2 2919	. . . . . . 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 2191	. . . . 5 |- ( ph -> dom G = S )
67		df-fn 5257	. . . . 5 |- ( G Fn S <-> ( Fun G /\ dom G = S ) )
68	16, 66, 67	sylanbrc 417	. . . 4 |- ( ph -> G Fn S )
69	13	fveq1i 5555	. . . . . . 7 |- ( G ` m ) = ( ( `'inl o. F ) ` m )
70	18	adantr 276	. . . . . . . 8 |- ( ( ph /\ m e. S ) -> F : om --> ( A ⊔ 1o ) )
71		fveq2 5554	. . . . . . . . . . . . 13 |- ( x = m -> ( F ` x ) = ( F ` m ) )
72	71	eleq1d 2262	. . . . . . . . . . . 12 |- ( x = m -> ( ( F ` x ) e. (inl " A ) <-> ( F ` m ) e. (inl " A ) ) )
73	72, 1	elrab2 2919	. . . . . . . . . . 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 5628	. . . . . . . 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 2238	. . . . . 6 |- ( ( ph /\ m e. S ) -> ( G ` m ) = ( `'inl ` ( F ` m ) ) )
80		f1ofun 5502	. . . . . . . . . 10 |- (inl : _V -1-1-onto-> ( { (/) } X. _V ) -> Fun inl )
81	5, 80	ax-mp 5	. . . . . . . . 9 |- Fun inl
82		fvelima 5608	. . . . . . . . 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 531	. . . . . . . . 9 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> (inl ` z ) = ( F ` m ) )
86	85	fveq2d 5558	. . . . . . . 8 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` (inl ` z ) ) = ( `'inl ` ( F ` m ) ) )
87		vex 2763	. . . . . . . . . 10 |- z e. _V
88		f1ocnvfv1 5820	. . . . . . . . . 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 529	. . . . . . . . 9 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> z e. A )
91	89, 90	eqeltrid 2280	. . . . . . . 8 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` (inl ` z ) ) e. A )
92	86, 91	eqeltrrd 2271	. . . . . . 7 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` ( F ` m ) ) e. A )
93	84, 92	rexlimddv 2616	. . . . . 6 |- ( ( ph /\ m e. S ) -> ( `'inl ` ( F ` m ) ) e. A )
94	79, 93	eqeltrd 2270	. . . . 5 |- ( ( ph /\ m e. S ) -> ( G ` m ) e. A )
95	94	ralrimiva 2567	. . . 4 |- ( ph -> A. m e. S ( G ` m ) e. A )
96		ffnfv 5716	. . . 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 7110	. . . . . . . 8 |- ( m e. A -> (inl ` m ) e. ( A ⊔ 1o ) )
99		foelrn 5795	. . . . . . . . . 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 2478	. . . . . . . . 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 5554	. . . . . . . . . . . . 13 |- ( x = y -> ( F ` x ) = ( F ` y ) )
105	104	eleq1d 2262	. . . . . . . . . . . 12 |- ( x = y -> ( ( F ` x ) e. (inl " A ) <-> ( F ` y ) e. (inl " A ) ) )
106		simprl 529	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> y e. om )
107		simprr 531	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> (inl ` m ) = ( F ` y ) )
108		vex 2763	. . . . . . . . . . . . . . . 16 |- m e. _V
109		f1odm 5504	. . . . . . . . . . . . . . . . 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 2269	. . . . . . . . . . . . . . 15 |- m e. dom inl
112		funfvima 5790	. . . . . . . . . . . . . . 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 2271	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> ( F ` y ) e. (inl " A ) )
116	105, 106, 115	elrabd 2918	. . . . . . . . . . 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 2287	. . . . . . . . . 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 1891	. . . . . . 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 2478	. . . . . 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 5820	. . . . . . . . . 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 5558	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> ( `'inl ` (inl ` m ) ) = ( `'inl ` ( F ` y ) ) )
128	125, 127	eqtr3id 2240	. . . . . . . 8 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> m = ( `'inl ` ( F ` y ) ) )
129	13	fveq1i 5555	. . . . . . . . . 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 3175	. . . . . . . . . . . 12 |- ( y e. S -> y e. om )
132	131	adantl 277	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> y e. om )
133		fvco3 5628	. . . . . . . . . . 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 2238	. . . . . . . . 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 2229	. . . . . . 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 2596	. . . . 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 2567	. . 3 |- ( ph -> A. m e. A E. y e. S m = ( G ` y ) )
142		dffo3 5705	. . 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 762	. . . . . 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 836	. . . . 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 839	. . . 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 2567	. 2 |- ( ph -> A. n e. om DECID n e. S )
156	4, 143, 155	3jca 1179	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 709  DECID wdc 835   /\ w3a 980   = wceq 1364   E.wex 1503   e. wcel 2164   A.wral 2472   E.wrex 2473   {crab 2476   _Vcvv 2760   u. cun 3151   i^i cin 3152   C_ wss 3153   (/)c0 3446   {csn 3618   omcom 4622   X. cxp 4657   `'ccnv 4658   dom cdm 4659   ran crn 4660   "cima 4662   o. ccom 4663   Fun wfun 5248   Fn wfn 5249   -->wf 5250   -onto->wfo 5252   -1-1-onto->wf1o 5253   ` cfv 5254   1oc1o 6462   ⊔ cdju 7096  inlcinl 7104  inrcinr 7105

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4464

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-sbc 2986  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-mpt 4092  df-tr 4128  df-id 4324  df-iord 4397  df-on 4399  df-suc 4402  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-1st 6193  df-2nd 6194  df-1o 6469  df-dju 7097  df-inl 7106  df-inr 7107

This theorem is referenced by:  ctssdclemr  7171  ctiunct  12597