isomninnlem - Mathbox for Jim Kingdon

	Mathbox for Jim Kingdon		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > Mathboxes > isomninnlem		Unicode version

Theorem isomninnlem 12906

Description: Lemma for isomninn 12907. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.)

**Hypothesis**
Ref	Expression
isomninnlem.g	frec

**Assertion**
Ref	Expression
isomninnlem	Omni $\/$

Distinct variable groups:

Proof of Theorem isomninnlem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isomnimap 6957	. 2 Omni $\/$
2		fveq1 5372	. . . . . . . . 9
3	2	eqeq1d 2121	. . . . . . . 8
4	3	rexbidv 2410	. . . . . . 7
5	2	eqeq1d 2121	. . . . . . . 8
6	5	ralbidv 2409	. . . . . . 7
7	4, 6	orbi12d 765	. . . . . 6 $\/$ $\/$
8		simplr 502	. . . . . 6 $/\$ $\/$ $/\$ $\/$
9		isomninnlem.g	. . . . . . . . . . . . 13 frec
10	9	frechashgf1o 10088	. . . . . . . . . . . 12
11		f1ocnv 5334	. . . . . . . . . . . 12
12		f1of 5321	. . . . . . . . . . . 12
13	10, 11, 12	mp2b 8	. . . . . . . . . . 11
14		0nn0 8890	. . . . . . . . . . . 12
15		1nn0 8891	. . . . . . . . . . . 12
16		prssi 3642	. . . . . . . . . . . 12 $/\$
17	14, 15, 16	mp2an 420	. . . . . . . . . . 11
18		fssres 5254	. . . . . . . . . . 11 $/\$
19	13, 17, 18	mp2an 420	. . . . . . . . . 10
20		ffn 5228	. . . . . . . . . 10
21	19, 20	ax-mp 7	. . . . . . . . 9
22		fvres 5397	. . . . . . . . . . 11
23		elpri 3514	. . . . . . . . . . . 12 $\/$
24		fveq2 5373	. . . . . . . . . . . . . 14
25		0zd 8964	. . . . . . . . . . . . . . . . . 18
26	25, 9	frec2uz0d 10059	. . . . . . . . . . . . . . . . 17
27	26	mptru 1321	. . . . . . . . . . . . . . . 16
28		peano1 4466	. . . . . . . . . . . . . . . . 17
29		f1ocnvfv 5632	. . . . . . . . . . . . . . . . 17 $/\$
30	10, 28, 29	mp2an 420	. . . . . . . . . . . . . . . 16
31	27, 30	ax-mp 7	. . . . . . . . . . . . . . 15
32		0lt2o 6290	. . . . . . . . . . . . . . 15
33	31, 32	eqeltri 2185	. . . . . . . . . . . . . 14
34	24, 33	syl6eqel 2203	. . . . . . . . . . . . 13
35		fveq2 5373	. . . . . . . . . . . . . 14
36		df-1o 6265	. . . . . . . . . . . . . . . . . 18
37	36	fveq2i 5376	. . . . . . . . . . . . . . . . 17
38	28	a1i 9	. . . . . . . . . . . . . . . . . . 19
39	25, 9, 38	frec2uzsucd 10061	. . . . . . . . . . . . . . . . . 18
40	39	mptru 1321	. . . . . . . . . . . . . . . . 17
41	27	oveq1i 5736	. . . . . . . . . . . . . . . . . 18
42		0p1e1 8738	. . . . . . . . . . . . . . . . . 18
43	41, 42	eqtri 2133	. . . . . . . . . . . . . . . . 17
44	37, 40, 43	3eqtri 2137	. . . . . . . . . . . . . . . 16
45		1onn 6368	. . . . . . . . . . . . . . . . 17
46		f1ocnvfv 5632	. . . . . . . . . . . . . . . . 17 $/\$
47	10, 45, 46	mp2an 420	. . . . . . . . . . . . . . . 16
48	44, 47	ax-mp 7	. . . . . . . . . . . . . . 15
49		1lt2o 6291	. . . . . . . . . . . . . . 15
50	48, 49	eqeltri 2185	. . . . . . . . . . . . . 14
51	35, 50	syl6eqel 2203	. . . . . . . . . . . . 13
52	34, 51	jaoi 688	. . . . . . . . . . . 12 $\/$
53	23, 52	syl 14	. . . . . . . . . . 11
54	22, 53	eqeltrd 2189	. . . . . . . . . 10
55	54	rgen 2457	. . . . . . . . 9
56		ffnfv 5530	. . . . . . . . 9 $/\$
57	21, 55, 56	mpbir2an 907	. . . . . . . 8
58		elmapi 6516	. . . . . . . . 9
59	58	adantl 273	. . . . . . . 8 $/\$ $\/$ $/\$
60		fco2 5245	. . . . . . . 8 $/\$
61	57, 59, 60	sylancr 408	. . . . . . 7 $/\$ $\/$ $/\$
62		2onn 6369	. . . . . . . . 9
63	62	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
64		simpll 501	. . . . . . . 8 $/\$ $\/$ $/\$
65	63, 64	elmapd 6508	. . . . . . 7 $/\$ $\/$ $/\$
66	61, 65	mpbird 166	. . . . . 6 $/\$ $\/$ $/\$
67	7, 8, 66	rspcdva 2763	. . . . 5 $/\$ $\/$ $/\$ $\/$
68		nfv 1489	. . . . . . . . 9
69		nfcv 2253	. . . . . . . . . 10
70		nfre1 2448	. . . . . . . . . . 11
71		nfra1 2438	. . . . . . . . . . 11
72	70, 71	nfor 1534	. . . . . . . . . 10 $\/$
73	69, 72	nfralxy 2443	. . . . . . . . 9 $\/$
74	68, 73	nfan 1525	. . . . . . . 8 $/\$ $\/$
75		nfv 1489	. . . . . . . 8
76	74, 75	nfan 1525	. . . . . . 7 $/\$ $\/$ $/\$
77		simplr 502	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$
78	77, 58	syl 14	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
79		simpr 109	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
80	78, 79	ffvelrnd 5508	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
81	17, 80	sseldi 3059	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
82		f1ocnvfv2 5631	. . . . . . . . . . 11 $/\$
83	10, 81, 82	sylancr 408	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
84	83	adantr 272	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
85		fvco3 5444	. . . . . . . . . . . . . 14 $/\$
86	78, 85	sylancom 414	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
87	86	eqeq1d 2121	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
88	87	biimpa 292	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
89	88	fveq2d 5377	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
90	89, 27	syl6eq 2161	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
91	84, 90	eqtr3d 2147	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
92	91	exp31 359	. . . . . . 7 $/\$ $\/$ $/\$
93	76, 92	reximdai 2502	. . . . . 6 $/\$ $\/$ $/\$
94	83	adantr 272	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
95	86	adantr 272	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
96		simpr 109	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
97	95, 96	eqtr3d 2147	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
98	97	fveq2d 5377	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
99	98, 44	syl6eq 2161	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
100	94, 99	eqtr3d 2147	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
101	100	ex 114	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
102	76, 101	ralimdaa 2470	. . . . . 6 $/\$ $\/$ $/\$
103	93, 102	orim12d 758	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
104	67, 103	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
105	104	ralrimiva 2477	. . 3 $/\$ $\/$ $\/$
106		fveq1 5372	. . . . . . . . 9
107	106	eqeq1d 2121	. . . . . . . 8
108	107	rexbidv 2410	. . . . . . 7
109	106	eqeq1d 2121	. . . . . . . 8
110	109	ralbidv 2409	. . . . . . 7
111	108, 110	orbi12d 765	. . . . . 6 $\/$ $\/$
112		simplr 502	. . . . . 6 $/\$ $\/$ $/\$ $\/$
113		f1of 5321	. . . . . . . . . . . 12
114	10, 113	ax-mp 7	. . . . . . . . . . 11
115		omelon 4480	. . . . . . . . . . . . 13
116	115	onelssi 4309	. . . . . . . . . . . 12
117	62, 116	ax-mp 7	. . . . . . . . . . 11
118		fssres 5254	. . . . . . . . . . 11 $/\$
119	114, 117, 118	mp2an 420	. . . . . . . . . 10
120		ffn 5228	. . . . . . . . . 10
121	119, 120	ax-mp 7	. . . . . . . . 9
122		fvres 5397	. . . . . . . . . . 11
123		elpri 3514	. . . . . . . . . . . . 13 $\/$
124		df2o3 6279	. . . . . . . . . . . . 13
125	123, 124	eleq2s 2207	. . . . . . . . . . . 12 $\/$
126		fveq2 5373	. . . . . . . . . . . . . 14
127		c0ex 7678	. . . . . . . . . . . . . . . 16
128	127	prid1 3593	. . . . . . . . . . . . . . 15
129	27, 128	eqeltri 2185	. . . . . . . . . . . . . 14
130	126, 129	syl6eqel 2203	. . . . . . . . . . . . 13
131		fveq2 5373	. . . . . . . . . . . . . 14
132		1ex 7679	. . . . . . . . . . . . . . . 16
133	132	prid2 3594	. . . . . . . . . . . . . . 15
134	44, 133	eqeltri 2185	. . . . . . . . . . . . . 14
135	131, 134	syl6eqel 2203	. . . . . . . . . . . . 13
136	130, 135	jaoi 688	. . . . . . . . . . . 12 $\/$
137	125, 136	syl 14	. . . . . . . . . . 11
138	122, 137	eqeltrd 2189	. . . . . . . . . 10
139	138	rgen 2457	. . . . . . . . 9
140		ffnfv 5530	. . . . . . . . 9 $/\$
141	121, 139, 140	mpbir2an 907	. . . . . . . 8
142		elmapi 6516	. . . . . . . . 9
143	142	adantl 273	. . . . . . . 8 $/\$ $\/$ $/\$
144		fco2 5245	. . . . . . . 8 $/\$
145	141, 143, 144	sylancr 408	. . . . . . 7 $/\$ $\/$ $/\$
146		prexg 4091	. . . . . . . . . 10 $/\$
147	14, 15, 146	mp2an 420	. . . . . . . . 9
148	147	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
149		simpll 501	. . . . . . . 8 $/\$ $\/$ $/\$
150	148, 149	elmapd 6508	. . . . . . 7 $/\$ $\/$ $/\$
151	145, 150	mpbird 166	. . . . . 6 $/\$ $\/$ $/\$
152	111, 112, 151	rspcdva 2763	. . . . 5 $/\$ $\/$ $/\$ $\/$
153		nfcv 2253	. . . . . . . . . 10
154		nfre1 2448	. . . . . . . . . . 11
155		nfra1 2438	. . . . . . . . . . 11
156	154, 155	nfor 1534	. . . . . . . . . 10 $\/$
157	153, 156	nfralxy 2443	. . . . . . . . 9 $\/$
158	68, 157	nfan 1525	. . . . . . . 8 $/\$ $\/$
159		nfv 1489	. . . . . . . 8
160	158, 159	nfan 1525	. . . . . . 7 $/\$ $\/$ $/\$
161	143	adantr 272	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
162	117	a1i 9	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
163	161, 162	fssd 5241	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
164		simpr 109	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
165	163, 164	ffvelrnd 5508	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
166		f1ocnvfv1 5630	. . . . . . . . . . 11 $/\$
167	10, 165, 166	sylancr 408	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
168	167	adantr 272	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
169		fvco3 5444	. . . . . . . . . . . . . 14 $/\$
170	161, 169	sylancom 414	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
171	170	eqeq1d 2121	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
172	171	biimpa 292	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
173	172	fveq2d 5377	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
174	173, 31	syl6eq 2161	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
175	168, 174	eqtr3d 2147	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
176	175	exp31 359	. . . . . . 7 $/\$ $\/$ $/\$
177	160, 176	reximdai 2502	. . . . . 6 $/\$ $\/$ $/\$
178	167	adantr 272	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
179	170	eqeq1d 2121	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
180	179	biimpa 292	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
181	180	fveq2d 5377	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
182	181, 48	syl6eq 2161	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
183	178, 182	eqtr3d 2147	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
184	183	ex 114	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
185	160, 184	ralimdaa 2470	. . . . . 6 $/\$ $\/$ $/\$
186	177, 185	orim12d 758	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
187	152, 186	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
188	187	ralrimiva 2477	. . 3 $/\$ $\/$ $\/$
189	105, 188	impbida 568	. 2 $\/$ $\/$
190	1, 189	bitrd 187	1 Omni $\/$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 680

wceq 1312

wtru 1313

wcel 1461

wral 2388

wrex 2389

cvv 2655

wss 3035

c0 3327

cpr 3492

cmpt 3947

csuc 4245

com 4462

ccnv 4496

cres 4499

ccom 4501

wfn 5074

wf 5075

wf1o 5078

cfv 5079 (class class class)co 5726 freccfrec 6239

c1o 6258

c2o 6259

cmap 6494 Omnicomni 6952

cc0 7541

c1 7542

caddc 7544

cn0 8875

cz 8952

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-io 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-13 1472 ax-14 1473 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 ax-coll 4001 ax-sep 4004 ax-nul 4012 ax-pow 4056 ax-pr 4089 ax-un 4313 ax-setind 4410 ax-iinf 4460 ax-cnex 7630 ax-resscn 7631 ax-1cn 7632 ax-1re 7633 ax-icn 7634 ax-addcl 7635 ax-addrcl 7636 ax-mulcl 7637 ax-addcom 7639 ax-addass 7641 ax-distr 7643 ax-i2m1 7644 ax-0lt1 7645 ax-0id 7647 ax-rnegex 7648 ax-cnre 7650 ax-pre-ltirr 7651 ax-pre-ltwlin 7652 ax-pre-lttrn 7653 ax-pre-ltadd 7655

This theorem depends on definitions: df-bi 116 df-3or 944 df-3an 945 df-tru 1315 df-fal 1318 df-nf 1418 df-sb 1717 df-eu 1976 df-mo 1977 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-ne 2281 df-nel 2376 df-ral 2393 df-rex 2394 df-reu 2395 df-rab 2397 df-v 2657 df-sbc 2877 df-csb 2970 df-dif 3037 df-un 3039 df-in 3041 df-ss 3048 df-nul 3328 df-pw 3476 df-sn 3497 df-pr 3498 df-op 3500 df-uni 3701 df-int 3736 df-iun 3779 df-br 3894 df-opab 3948 df-mpt 3949 df-tr 3985 df-id 4173 df-iord 4246 df-on 4248 df-ilim 4249 df-suc 4251 df-iom 4463 df-xp 4503 df-rel 4504 df-cnv 4505 df-co 4506 df-dm 4507 df-rn 4508 df-res 4509 df-ima 4510 df-iota 5044 df-fun 5081 df-fn 5082 df-f 5083 df-f1 5084 df-fo 5085 df-f1o 5086 df-fv 5087 df-riota 5682 df-ov 5729 df-oprab 5730 df-mpo 5731 df-recs 6154 df-frec 6240 df-1o 6265 df-2o 6266 df-map 6496 df-omni 6954 df-pnf 7720 df-mnf 7721 df-xr 7722 df-ltxr 7723 df-le 7724 df-sub 7852 df-neg 7853 df-inn 8625 df-n0 8876 df-z 8953 df-uz 9223

This theorem is referenced by: isomninn 12907

W3C validator