Theorem ctssdccl 7444

Description: A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7446 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 3333	. . . 4 |- { x e. om | ( F ` x ) e. (inl " A ) } C_ om
3	1, 2	eqsstri 3280	. . 3 |- S C_ om
4	3	a1i 9	. 2 |- ( ph -> S C_ om )
5		djulf1o 7391	. . . . . . 7 |- inl : _V -1-1-onto-> ( { (/) } X. _V )
6		f1ocnv 5650	. . . . . . 7 |- (inl : _V -1-1-onto-> ( { (/) } X. _V ) -> `'inl : ( { (/) } X. _V ) -1-1-onto-> _V )
7		f1ofun 5639	. . . . . . 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 5614	. . . . . . 7 |- ( F : om -onto-> ( A ⊔ 1o ) -> Fun F )
11	9, 10	syl 14	. . . . . 6 |- ( ph -> Fun F )
12		funco 5415	. . . . . . 7 |- ( ( Fun `'inl /\ Fun F ) -> Fun ( `'inl o. F ) )
13		ctssdccl.g	. . . . . . . 8 |- G = ( `'inl o. F )
14	13	funeqi 5396	. . . . . . 7 |- ( Fun G <-> Fun ( `'inl o. F ) )
15	12, 14	sylibr 134	. . . . . 6 |- ( ( Fun `'inl /\ Fun F ) -> Fun G )
16	8, 11, 15	sylancr 418	. . . . 5 |- ( ph -> Fun G )
17		fof 5613	. . . . . . . . . . . 12 |- ( F : om -onto-> ( A ⊔ 1o ) -> F : om --> ( A ⊔ 1o ) )
18	9, 17	syl 14	. . . . . . . . . . 11 |- ( ph -> F : om --> ( A ⊔ 1o ) )
19	18	fdmd 5538	. . . . . . . . . 10 |- ( ph -> dom F = om )
20	19	eleq2d 2308	. . . . . . . . 9 |- ( ph -> ( n e. dom F <-> n e. om ) )
21	20	anbi1d 469	. . . . . . . 8 |- ( ph -> ( ( n e. dom F /\ ( F ` n ) e. dom `'inl ) <-> ( n e. om /\ ( F ` n ) e. dom `'inl ) ) )
22		dmcoss 5050	. . . . . . . . . . . 12 |- dom ( `'inl o. F ) C_ dom F
23	22	sseli 3244	. . . . . . . . . . 11 |- ( n e. dom ( `'inl o. F ) -> n e. dom F )
24	23	pm4.71ri 396	. . . . . . . . . 10 |- ( n e. dom ( `'inl o. F ) <-> ( n e. dom F /\ n e. dom ( `'inl o. F ) ) )
25		dmfco 5770	. . . . . . . . . . 11 |- ( ( Fun F /\ n e. dom F ) -> ( n e. dom ( `'inl o. F ) <-> ( F ` n ) e. dom `'inl ) )
26	25	pm5.32da 456	. . . . . . . . . 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 5135	. . . . . . . . . . . . . 14 |- (inl " A ) C_ ran inl
31	30	sseli 3244	. . . . . . . . . . . . 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 4783	. . . . . . . . . . . . 13 |- ran inl = dom `'inl
34	33	eleq2i 2305	. . . . . . . . . . . 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 7397	. . . . . . . . . . . . . 14 |- ( (inl " A ) i^i (inr " 1o ) ) = (/)
38		disjel 3579	. . . . . . . . . . . . . 14 |- ( ( ( (inl " A ) i^i (inr " 1o ) ) = (/) /\ ( F ` n ) e. (inl " A ) ) -> -. ( F ` n ) e. (inr " 1o ) )
39	37, 38	mpan 428	. . . . . . . . . . . . 13 |- ( ( F ` n ) e. (inl " A ) -> -. ( F ` n ) e. (inr " 1o ) )
40	39	con2i 636	. . . . . . . . . . . 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 7397	. . . . . . . . . . . . . . . 16 |- ( (inl " _V ) i^i (inr " 1o ) ) = (/)
43		disjel 3579	. . . . . . . . . . . . . . . 16 |- ( ( ( (inl " _V ) i^i (inr " 1o ) ) = (/) /\ ( F ` n ) e. (inl " _V ) ) -> -. ( F ` n ) e. (inr " 1o ) )
44	42, 43	mpan 428	. . . . . . . . . . . . . . 15 |- ( ( F ` n ) e. (inl " _V ) -> -. ( F ` n ) e. (inr " 1o ) )
45		dfrn4 5246	. . . . . . . . . . . . . . 15 |- ran inl = (inl " _V )
46	44, 45	eleq2s 2333	. . . . . . . . . . . . . 14 |- ( ( F ` n ) e. ran inl -> -. ( F ` n ) e. (inr " 1o ) )
47	46	con2i 636	. . . . . . . . . . . . 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 687	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> -. ( F ` n ) e. dom `'inl )
50	41, 49	2falsed 714	. . . . . . . . . 10 |- ( ( ( ph /\ n e. om ) /\ ( F ` n ) e. (inr " 1o ) ) -> ( ( F ` n ) e. (inl " A ) <-> ( F ` n ) e. dom `'inl ) )
51	18	ffvelcdmda 5837	. . . . . . . . . . . 12 |- ( ( ph /\ n e. om ) -> ( F ` n ) e. ( A ⊔ 1o ) )
52		djuun 7400	. . . . . . . . . . . . 13 |- ( (inl " A ) u. (inr " 1o ) ) = ( A ⊔ 1o )
53	52	eleq2i 2305	. . . . . . . . . . . 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 3370	. . . . . . . . . . 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 810	. . . . . . . . 9 |- ( ( ph /\ n e. om ) -> ( ( F ` n ) e. (inl " A ) <-> ( F ` n ) e. dom `'inl ) )
58	57	pm5.32da 456	. . . . . . . 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 4980	. . . . . . . 8 |- dom G = dom ( `'inl o. F )
61	60	eleq2i 2305	. . . . . . 7 |- ( n e. dom G <-> n e. dom ( `'inl o. F ) )
62		fveq2 5693	. . . . . . . . 9 |- ( x = n -> ( F ` x ) = ( F ` n ) )
63	62	eleq1d 2307	. . . . . . . 8 |- ( x = n -> ( ( F ` x ) e. (inl " A ) <-> ( F ` n ) e. (inl " A ) ) )
64	63, 1	elrab2 2985	. . . . . . 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 2236	. . . . 5 |- ( ph -> dom G = S )
67		df-fn 5378	. . . . 5 |- ( G Fn S <-> ( Fun G /\ dom G = S ) )
68	16, 66, 67	sylanbrc 421	. . . 4 |- ( ph -> G Fn S )
69	13	fveq1i 5694	. . . . . . 7 |- ( G ` m ) = ( ( `'inl o. F ) ` m )
70	18	adantr 276	. . . . . . . 8 |- ( ( ph /\ m e. S ) -> F : om --> ( A ⊔ 1o ) )
71		fveq2 5693	. . . . . . . . . . . . 13 |- ( x = m -> ( F ` x ) = ( F ` m ) )
72	71	eleq1d 2307	. . . . . . . . . . . 12 |- ( x = m -> ( ( F ` x ) e. (inl " A ) <-> ( F ` m ) e. (inl " A ) ) )
73	72, 1	elrab2 2985	. . . . . . . . . . 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 5773	. . . . . . . 8 |- ( ( F : om --> ( A ⊔ 1o ) /\ m e. om ) -> ( ( `'inl o. F ) ` m ) = ( `'inl ` ( F ` m ) ) )
78	70, 76, 77	syl2anc 415	. . . . . . 7 |- ( ( ph /\ m e. S ) -> ( ( `'inl o. F ) ` m ) = ( `'inl ` ( F ` m ) ) )
79	69, 78	eqtrid 2283	. . . . . 6 |- ( ( ph /\ m e. S ) -> ( G ` m ) = ( `'inl ` ( F ` m ) ) )
80		f1ofun 5639	. . . . . . . . . 10 |- (inl : _V -1-1-onto-> ( { (/) } X. _V ) -> Fun inl )
81	5, 80	ax-mp 5	. . . . . . . . 9 |- Fun inl
82		fvelima 5751	. . . . . . . . 9 |- ( ( Fun inl /\ ( F ` m ) e. (inl " A ) ) -> E. z e. A (inl ` z ) = ( F ` m ) )
83	81, 82	mpan 428	. . . . . . . 8 |- ( ( F ` m ) e. (inl " A ) -> E. z e. A (inl ` z ) = ( F ` m ) )
84	75, 83	simpl2im 390	. . . . . . 7 |- ( ( ph /\ m e. S ) -> E. z e. A (inl ` z ) = ( F ` m ) )
85		simprr 537	. . . . . . . . 9 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> (inl ` z ) = ( F ` m ) )
86	85	fveq2d 5697	. . . . . . . 8 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` (inl ` z ) ) = ( `'inl ` ( F ` m ) ) )
87		vex 2824	. . . . . . . . . 10 |- z e. _V
88		f1ocnvfv1 5976	. . . . . . . . . 10 |- ( (inl : _V -1-1-onto-> ( { (/) } X. _V ) /\ z e. _V ) -> ( `'inl ` (inl ` z ) ) = z )
89	5, 87, 88	mp2an 430	. . . . . . . . 9 |- ( `'inl ` (inl ` z ) ) = z
90		simprl 535	. . . . . . . . 9 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> z e. A )
91	89, 90	eqeltrid 2325	. . . . . . . 8 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` (inl ` z ) ) e. A )
92	86, 91	eqeltrrd 2316	. . . . . . 7 |- ( ( ( ph /\ m e. S ) /\ ( z e. A /\ (inl ` z ) = ( F ` m ) ) ) -> ( `'inl ` ( F ` m ) ) e. A )
93	84, 92	rexlimddv 2673	. . . . . 6 |- ( ( ph /\ m e. S ) -> ( `'inl ` ( F ` m ) ) e. A )
94	79, 93	eqeltrd 2315	. . . . 5 |- ( ( ph /\ m e. S ) -> ( G ` m ) e. A )
95	94	ralrimiva 2623	. . . 4 |- ( ph -> A. m e. S ( G ` m ) e. A )
96		ffnfv 5860	. . . 4 |- ( G : S --> A <-> ( G Fn S /\ A. m e. S ( G ` m ) e. A ) )
97	68, 95, 96	sylanbrc 421	. . 3 |- ( ph -> G : S --> A )
98		djulcl 7384	. . . . . . . 8 |- ( m e. A -> (inl ` m ) e. ( A ⊔ 1o ) )
99		foelrn 5951	. . . . . . . . . 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 2534	. . . . . . . . 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 5693	. . . . . . . . . . . . 13 |- ( x = y -> ( F ` x ) = ( F ` y ) )
105	104	eleq1d 2307	. . . . . . . . . . . 12 |- ( x = y -> ( ( F ` x ) e. (inl " A ) <-> ( F ` y ) e. (inl " A ) ) )
106		simprl 535	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> y e. om )
107		simprr 537	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> (inl ` m ) = ( F ` y ) )
108		vex 2824	. . . . . . . . . . . . . . . 16 |- m e. _V
109		f1odm 5641	. . . . . . . . . . . . . . . . 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 2314	. . . . . . . . . . . . . . 15 |- m e. dom inl
112		funfvima 5943	. . . . . . . . . . . . . . 15 |- ( ( Fun inl /\ m e. dom inl ) -> ( m e. A -> (inl ` m ) e. (inl " A ) ) )
113	81, 111, 112	mp2an 430	. . . . . . . . . . . . . 14 |- ( m e. A -> (inl ` m ) e. (inl " A ) )
114	113	ad2antlr 493	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> (inl ` m ) e. (inl " A ) )
115	107, 114	eqeltrrd 2316	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. A ) /\ ( y e. om /\ (inl ` m ) = ( F ` y ) ) ) -> ( F ` y ) e. (inl " A ) )
116	105, 106, 115	elrabd 2984	. . . . . . . . . . 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 2332	. . . . . . . . . 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 1933	. . . . . . 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 2534	. . . . . 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 5976	. . . . . . . . . 10 |- ( (inl : _V -1-1-onto-> ( { (/) } X. _V ) /\ m e. _V ) -> ( `'inl ` (inl ` m ) ) = m )
125	5, 108, 124	mp2an 430	. . . . . . . . 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 5697	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> ( `'inl ` (inl ` m ) ) = ( `'inl ` ( F ` y ) ) )
128	125, 127	eqtr3id 2285	. . . . . . . 8 |- ( ( ( ( ph /\ m e. A ) /\ y e. S ) /\ (inl ` m ) = ( F ` y ) ) -> m = ( `'inl ` ( F ` y ) ) )
129	13	fveq1i 5694	. . . . . . . . . 10 |- ( G ` y ) = ( ( `'inl o. F ) ` y )
130	18	ad2antrr 492	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> F : om --> ( A ⊔ 1o ) )
131	3	sseli 3244	. . . . . . . . . . . 12 |- ( y e. S -> y e. om )
132	131	adantl 277	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> y e. om )
133		fvco3 5773	. . . . . . . . . . 11 |- ( ( F : om --> ( A ⊔ 1o ) /\ y e. om ) -> ( ( `'inl o. F ) ` y ) = ( `'inl ` ( F ` y ) ) )
134	130, 132, 133	syl2anc 415	. . . . . . . . . 10 |- ( ( ( ph /\ m e. A ) /\ y e. S ) -> ( ( `'inl o. F ) ` y ) = ( `'inl ` ( F ` y ) ) )
135	129, 134	eqtrid 2283	. . . . . . . . 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 2274	. . . . . . 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 2652	. . . . 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 2623	. . 3 |- ( ph -> A. m e. A E. y e. S m = ( G ` y ) )
142		dffo3 5849	. . 3 |- ( G : S -onto-> A <-> ( G : S --> A /\ A. m e. A E. y e. S m = ( G ` y ) ) )
143	97, 141, 142	sylanbrc 421	. 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 773	. . . . . 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 847	. . . . 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 850	. . . 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 2623	. 2 |- ( ph -> A. n e. om DECID n e. S )
156	4, 143, 155	3jca 1208	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 720  DECID wdc 846   /\ w3a 1009   = wceq 1402   E.wex 1545   e. wcel 2209   A.wral 2528   E.wrex 2529   {crab 2532   _Vcvv 2821   u. cun 3218   i^i cin 3219   C_ wss 3220   (/)c0 3520   {csn 3708   omcom 4735   X. cxp 4770   `'ccnv 4771   dom cdm 4772   ran crn 4773   "cima 4775   o. ccom 4776   Fun wfun 5369   Fn wfn 5370   -->wf 5371   -onto->wfo 5373   -1-1-onto->wf1o 5374   ` cfv 5375   1oc1o 6673   ⊔ cdju 7370  inlcinl 7378  inrcinr 7379

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-nul 4257  ax-pow 4309  ax-pr 4344  ax-un 4576

This theorem depends on definitions:  df-bi 117  df-dc 847  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-opab 4191  df-mpt 4192  df-tr 4228  df-id 4436  df-iord 4509  df-on 4511  df-suc 4514  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-rn 4783  df-res 4784  df-ima 4785  df-iota 5335  df-fun 5377  df-fn 5378  df-f 5379  df-f1 5380  df-fo 5381  df-f1o 5382  df-fv 5383  df-1st 6367  df-2nd 6368  df-1o 6680  df-dju 7371  df-inl 7380  df-inr 7381

This theorem is referenced by:  ctssdclemr  7445  ctiunct  13312