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 13225

Description: Lemma for isomninn 13226. 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 7009	. 2 Omni $\/$
2		fveq1 5420	. . . . . . . . 9
3	2	eqeq1d 2148	. . . . . . . 8
4	3	rexbidv 2438	. . . . . . 7
5	2	eqeq1d 2148	. . . . . . . 8
6	5	ralbidv 2437	. . . . . . 7
7	4, 6	orbi12d 782	. . . . . 6 $\/$ $\/$
8		simplr 519	. . . . . 6 $/\$ $\/$ $/\$ $\/$
9		isomninnlem.g	. . . . . . . . . . . . 13 frec
10	9	frechashgf1o 10201	. . . . . . . . . . . 12
11		f1ocnv 5380	. . . . . . . . . . . 12
12		f1of 5367	. . . . . . . . . . . 12
13	10, 11, 12	mp2b 8	. . . . . . . . . . 11
14		0nn0 8992	. . . . . . . . . . . 12
15		1nn0 8993	. . . . . . . . . . . 12
16		prssi 3678	. . . . . . . . . . . 12 $/\$
17	14, 15, 16	mp2an 422	. . . . . . . . . . 11
18		fssres 5298	. . . . . . . . . . 11 $/\$
19	13, 17, 18	mp2an 422	. . . . . . . . . 10
20		ffn 5272	. . . . . . . . . 10
21	19, 20	ax-mp 5	. . . . . . . . 9
22		fvres 5445	. . . . . . . . . . 11
23		elpri 3550	. . . . . . . . . . . 12 $\/$
24		fveq2 5421	. . . . . . . . . . . . . 14
25		0zd 9066	. . . . . . . . . . . . . . . . . 18
26	25, 9	frec2uz0d 10172	. . . . . . . . . . . . . . . . 17
27	26	mptru 1340	. . . . . . . . . . . . . . . 16
28		peano1 4508	. . . . . . . . . . . . . . . . 17
29		f1ocnvfv 5680	. . . . . . . . . . . . . . . . 17 $/\$
30	10, 28, 29	mp2an 422	. . . . . . . . . . . . . . . 16
31	27, 30	ax-mp 5	. . . . . . . . . . . . . . 15
32		0lt2o 6338	. . . . . . . . . . . . . . 15
33	31, 32	eqeltri 2212	. . . . . . . . . . . . . 14
34	24, 33	eqeltrdi 2230	. . . . . . . . . . . . 13
35		fveq2 5421	. . . . . . . . . . . . . 14
36		df-1o 6313	. . . . . . . . . . . . . . . . . 18
37	36	fveq2i 5424	. . . . . . . . . . . . . . . . 17
38	28	a1i 9	. . . . . . . . . . . . . . . . . . 19
39	25, 9, 38	frec2uzsucd 10174	. . . . . . . . . . . . . . . . . 18
40	39	mptru 1340	. . . . . . . . . . . . . . . . 17
41	27	oveq1i 5784	. . . . . . . . . . . . . . . . . 18
42		0p1e1 8834	. . . . . . . . . . . . . . . . . 18
43	41, 42	eqtri 2160	. . . . . . . . . . . . . . . . 17
44	37, 40, 43	3eqtri 2164	. . . . . . . . . . . . . . . 16
45		1onn 6416	. . . . . . . . . . . . . . . . 17
46		f1ocnvfv 5680	. . . . . . . . . . . . . . . . 17 $/\$
47	10, 45, 46	mp2an 422	. . . . . . . . . . . . . . . 16
48	44, 47	ax-mp 5	. . . . . . . . . . . . . . 15
49		1lt2o 6339	. . . . . . . . . . . . . . 15
50	48, 49	eqeltri 2212	. . . . . . . . . . . . . 14
51	35, 50	eqeltrdi 2230	. . . . . . . . . . . . 13
52	34, 51	jaoi 705	. . . . . . . . . . . 12 $\/$
53	23, 52	syl 14	. . . . . . . . . . 11
54	22, 53	eqeltrd 2216	. . . . . . . . . 10
55	54	rgen 2485	. . . . . . . . 9
56		ffnfv 5578	. . . . . . . . 9 $/\$
57	21, 55, 56	mpbir2an 926	. . . . . . . 8
58		elmapi 6564	. . . . . . . . 9
59	58	adantl 275	. . . . . . . 8 $/\$ $\/$ $/\$
60		fco2 5289	. . . . . . . 8 $/\$
61	57, 59, 60	sylancr 410	. . . . . . 7 $/\$ $\/$ $/\$
62		2onn 6417	. . . . . . . . 9
63	62	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
64		simpll 518	. . . . . . . 8 $/\$ $\/$ $/\$
65	63, 64	elmapd 6556	. . . . . . 7 $/\$ $\/$ $/\$
66	61, 65	mpbird 166	. . . . . 6 $/\$ $\/$ $/\$
67	7, 8, 66	rspcdva 2794	. . . . 5 $/\$ $\/$ $/\$ $\/$
68		nfv 1508	. . . . . . . . 9
69		nfcv 2281	. . . . . . . . . 10
70		nfre1 2476	. . . . . . . . . . 11
71		nfra1 2466	. . . . . . . . . . 11
72	70, 71	nfor 1553	. . . . . . . . . 10 $\/$
73	69, 72	nfralxy 2471	. . . . . . . . 9 $\/$
74	68, 73	nfan 1544	. . . . . . . 8 $/\$ $\/$
75		nfv 1508	. . . . . . . 8
76	74, 75	nfan 1544	. . . . . . 7 $/\$ $\/$ $/\$
77		simplr 519	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$
78	77, 58	syl 14	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
79		simpr 109	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
80	78, 79	ffvelrnd 5556	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
81	17, 80	sseldi 3095	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
82		f1ocnvfv2 5679	. . . . . . . . . . 11 $/\$
83	10, 81, 82	sylancr 410	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
84	83	adantr 274	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
85		fvco3 5492	. . . . . . . . . . . . . 14 $/\$
86	78, 85	sylancom 416	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
87	86	eqeq1d 2148	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
88	87	biimpa 294	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
89	88	fveq2d 5425	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
90	89, 27	syl6eq 2188	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
91	84, 90	eqtr3d 2174	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
92	91	exp31 361	. . . . . . 7 $/\$ $\/$ $/\$
93	76, 92	reximdai 2530	. . . . . 6 $/\$ $\/$ $/\$
94	83	adantr 274	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
95	86	adantr 274	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
96		simpr 109	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
97	95, 96	eqtr3d 2174	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
98	97	fveq2d 5425	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
99	98, 44	syl6eq 2188	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
100	94, 99	eqtr3d 2174	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
101	100	ex 114	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
102	76, 101	ralimdaa 2498	. . . . . 6 $/\$ $\/$ $/\$
103	93, 102	orim12d 775	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
104	67, 103	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
105	104	ralrimiva 2505	. . 3 $/\$ $\/$ $\/$
106		fveq1 5420	. . . . . . . . 9
107	106	eqeq1d 2148	. . . . . . . 8
108	107	rexbidv 2438	. . . . . . 7
109	106	eqeq1d 2148	. . . . . . . 8
110	109	ralbidv 2437	. . . . . . 7
111	108, 110	orbi12d 782	. . . . . 6 $\/$ $\/$
112		simplr 519	. . . . . 6 $/\$ $\/$ $/\$ $\/$
113		f1of 5367	. . . . . . . . . . . 12
114	10, 113	ax-mp 5	. . . . . . . . . . 11
115		omelon 4522	. . . . . . . . . . . . 13
116	115	onelssi 4351	. . . . . . . . . . . 12
117	62, 116	ax-mp 5	. . . . . . . . . . 11
118		fssres 5298	. . . . . . . . . . 11 $/\$
119	114, 117, 118	mp2an 422	. . . . . . . . . 10
120		ffn 5272	. . . . . . . . . 10
121	119, 120	ax-mp 5	. . . . . . . . 9
122		fvres 5445	. . . . . . . . . . 11
123		elpri 3550	. . . . . . . . . . . . 13 $\/$
124		df2o3 6327	. . . . . . . . . . . . 13
125	123, 124	eleq2s 2234	. . . . . . . . . . . 12 $\/$
126		fveq2 5421	. . . . . . . . . . . . . 14
127		c0ex 7760	. . . . . . . . . . . . . . . 16
128	127	prid1 3629	. . . . . . . . . . . . . . 15
129	27, 128	eqeltri 2212	. . . . . . . . . . . . . 14
130	126, 129	eqeltrdi 2230	. . . . . . . . . . . . 13
131		fveq2 5421	. . . . . . . . . . . . . 14
132		1ex 7761	. . . . . . . . . . . . . . . 16
133	132	prid2 3630	. . . . . . . . . . . . . . 15
134	44, 133	eqeltri 2212	. . . . . . . . . . . . . 14
135	131, 134	eqeltrdi 2230	. . . . . . . . . . . . 13
136	130, 135	jaoi 705	. . . . . . . . . . . 12 $\/$
137	125, 136	syl 14	. . . . . . . . . . 11
138	122, 137	eqeltrd 2216	. . . . . . . . . 10
139	138	rgen 2485	. . . . . . . . 9
140		ffnfv 5578	. . . . . . . . 9 $/\$
141	121, 139, 140	mpbir2an 926	. . . . . . . 8
142		elmapi 6564	. . . . . . . . 9
143	142	adantl 275	. . . . . . . 8 $/\$ $\/$ $/\$
144		fco2 5289	. . . . . . . 8 $/\$
145	141, 143, 144	sylancr 410	. . . . . . 7 $/\$ $\/$ $/\$
146		prexg 4133	. . . . . . . . . 10 $/\$
147	14, 15, 146	mp2an 422	. . . . . . . . 9
148	147	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
149		simpll 518	. . . . . . . 8 $/\$ $\/$ $/\$
150	148, 149	elmapd 6556	. . . . . . 7 $/\$ $\/$ $/\$
151	145, 150	mpbird 166	. . . . . 6 $/\$ $\/$ $/\$
152	111, 112, 151	rspcdva 2794	. . . . 5 $/\$ $\/$ $/\$ $\/$
153		nfcv 2281	. . . . . . . . . 10
154		nfre1 2476	. . . . . . . . . . 11
155		nfra1 2466	. . . . . . . . . . 11
156	154, 155	nfor 1553	. . . . . . . . . 10 $\/$
157	153, 156	nfralxy 2471	. . . . . . . . 9 $\/$
158	68, 157	nfan 1544	. . . . . . . 8 $/\$ $\/$
159		nfv 1508	. . . . . . . 8
160	158, 159	nfan 1544	. . . . . . 7 $/\$ $\/$ $/\$
161	143	adantr 274	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
162	117	a1i 9	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
163	161, 162	fssd 5285	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
164		simpr 109	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
165	163, 164	ffvelrnd 5556	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
166		f1ocnvfv1 5678	. . . . . . . . . . 11 $/\$
167	10, 165, 166	sylancr 410	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
168	167	adantr 274	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
169		fvco3 5492	. . . . . . . . . . . . . 14 $/\$
170	161, 169	sylancom 416	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
171	170	eqeq1d 2148	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
172	171	biimpa 294	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
173	172	fveq2d 5425	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
174	173, 31	syl6eq 2188	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
175	168, 174	eqtr3d 2174	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
176	175	exp31 361	. . . . . . 7 $/\$ $\/$ $/\$
177	160, 176	reximdai 2530	. . . . . 6 $/\$ $\/$ $/\$
178	167	adantr 274	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
179	170	eqeq1d 2148	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
180	179	biimpa 294	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
181	180	fveq2d 5425	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
182	181, 48	syl6eq 2188	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
183	178, 182	eqtr3d 2174	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
184	183	ex 114	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
185	160, 184	ralimdaa 2498	. . . . . 6 $/\$ $\/$ $/\$
186	177, 185	orim12d 775	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
187	152, 186	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
188	187	ralrimiva 2505	. . 3 $/\$ $\/$ $\/$
189	105, 188	impbida 585	. 2 $\/$ $\/$
190	1, 189	bitrd 187	1 Omni $\/$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 697

wceq 1331

wtru 1332

wcel 1480

wral 2416

wrex 2417

cvv 2686

wss 3071

c0 3363

cpr 3528

cmpt 3989

csuc 4287

com 4504

ccnv 4538

cres 4541

ccom 4543

wfn 5118

wf 5119

wf1o 5122

cfv 5123 (class class class)co 5774 freccfrec 6287

c1o 6306

c2o 6307

cmap 6542 Omnicomni 7004

cc0 7620

c1 7621

caddc 7623

cn0 8977

cz 9054

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-coll 4043 ax-sep 4046 ax-nul 4054 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452 ax-iinf 4502 ax-cnex 7711 ax-resscn 7712 ax-1cn 7713 ax-1re 7714 ax-icn 7715 ax-addcl 7716 ax-addrcl 7717 ax-mulcl 7718 ax-addcom 7720 ax-addass 7722 ax-distr 7724 ax-i2m1 7725 ax-0lt1 7726 ax-0id 7728 ax-rnegex 7729 ax-cnre 7731 ax-pre-ltirr 7732 ax-pre-ltwlin 7733 ax-pre-lttrn 7734 ax-pre-ltadd 7736

This theorem depends on definitions: df-bi 116 df-3or 963 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-nel 2404 df-ral 2421 df-rex 2422 df-reu 2423 df-rab 2425 df-v 2688 df-sbc 2910 df-csb 3004 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-int 3772 df-iun 3815 df-br 3930 df-opab 3990 df-mpt 3991 df-tr 4027 df-id 4215 df-iord 4288 df-on 4290 df-ilim 4291 df-suc 4293 df-iom 4505 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-riota 5730 df-ov 5777 df-oprab 5778 df-mpo 5779 df-recs 6202 df-frec 6288 df-1o 6313 df-2o 6314 df-map 6544 df-omni 7006 df-pnf 7802 df-mnf 7803 df-xr 7804 df-ltxr 7805 df-le 7806 df-sub 7935 df-neg 7936 df-inn 8721 df-n0 8978 df-z 9055 df-uz 9327

This theorem is referenced by: isomninn 13226

W3C validator