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 16984

Description: Lemma for isomninn 16985. 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 variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		isomnimap 7467	. 2 Omni $\/$
2		fveq1 5689	. . . . . . . . 9
3	2	eqeq1d 2247	. . . . . . . 8
4	3	rexbidv 2551	. . . . . . 7
5	2	eqeq1d 2247	. . . . . . . 8
6	5	ralbidv 2550	. . . . . . 7
7	4, 6	orbi12d 805	. . . . . 6 $\/$ $\/$
8		simplr 533	. . . . . 6 $/\$ $\/$ $/\$ $\/$
9		isomninnlem.g	. . . . . . . . 9 frec
10	9	012of 16937	. . . . . . . 8
11		elmapi 6934	. . . . . . . . 9
12	11	adantl 277	. . . . . . . 8 $/\$ $\/$ $/\$
13		fco2 5549	. . . . . . . 8 $/\$
14	10, 12, 13	sylancr 418	. . . . . . 7 $/\$ $\/$ $/\$
15		2onn 6784	. . . . . . . . 9
16	15	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
17		simpll 531	. . . . . . . 8 $/\$ $\/$ $/\$
18	16, 17	elmapd 6926	. . . . . . 7 $/\$ $\/$ $/\$
19	14, 18	mpbird 167	. . . . . 6 $/\$ $\/$ $/\$
20	7, 8, 19	rspcdva 2934	. . . . 5 $/\$ $\/$ $/\$ $\/$
21		nfv 1581	. . . . . . . . 9
22		nfcv 2392	. . . . . . . . . 10
23		nfre1 2593	. . . . . . . . . . 11
24		nfra1 2581	. . . . . . . . . . 11
25	23, 24	nfor 1627	. . . . . . . . . 10 $\/$
26	22, 25	nfralxy 2588	. . . . . . . . 9 $\/$
27	21, 26	nfan 1618	. . . . . . . 8 $/\$ $\/$
28		nfv 1581	. . . . . . . 8
29	27, 28	nfan 1618	. . . . . . 7 $/\$ $\/$ $/\$
30	9	frechashgf1o 10843	. . . . . . . . . . 11
31		0nn0 9557	. . . . . . . . . . . . 13
32		1nn0 9558	. . . . . . . . . . . . 13
33		prssi 3868	. . . . . . . . . . . . 13 $/\$
34	31, 32, 33	mp2an 430	. . . . . . . . . . . 12
35	11	ad2antlr 493	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
36		simpr 110	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
37	35, 36	ffvelcdmd 5835	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
38	34, 37	sselid 3246	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
39		f1ocnvfv2 5974	. . . . . . . . . . 11 $/\$
40	30, 38, 39	sylancr 418	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
41	40	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
42		fvco3 5770	. . . . . . . . . . . . . 14 $/\$
43	35, 42	sylancom 424	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
44	43	eqeq1d 2247	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
45	44	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
46	45	fveq2d 5694	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
47		0zd 9635	. . . . . . . . . . . 12
48	47, 9	frec2uz0d 10814	. . . . . . . . . . 11
49	48	mptru 1411	. . . . . . . . . 10
50	46, 49	eqtrdi 2287	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
51	41, 50	eqtr3d 2273	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
52	51	exp31 364	. . . . . . 7 $/\$ $\/$ $/\$
53	29, 52	reximdai 2648	. . . . . 6 $/\$ $\/$ $/\$
54	40	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
55	43	adantr 276	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
56		simpr 110	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
57	55, 56	eqtr3d 2273	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
58	57	fveq2d 5694	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
59		df-1o 6677	. . . . . . . . . . . 12
60	59	fveq2i 5693	. . . . . . . . . . 11
61		peano1 4736	. . . . . . . . . . . . . 14
62	61	a1i 9	. . . . . . . . . . . . 13
63	47, 9, 62	frec2uzsucd 10816	. . . . . . . . . . . 12
64	63	mptru 1411	. . . . . . . . . . 11
65	49	oveq1i 6085	. . . . . . . . . . . 12
66		0p1e1 9397	. . . . . . . . . . . 12
67	65, 66	eqtri 2259	. . . . . . . . . . 11
68	60, 64, 67	3eqtri 2263	. . . . . . . . . 10
69	58, 68	eqtrdi 2287	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
70	54, 69	eqtr3d 2273	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
71	70	ex 115	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
72	29, 71	ralimdaa 2616	. . . . . 6 $/\$ $\/$ $/\$
73	53, 72	orim12d 798	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
74	20, 73	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
75	74	ralrimiva 2623	. . 3 $/\$ $\/$ $\/$
76		fveq1 5689	. . . . . . . . 9
77	76	eqeq1d 2247	. . . . . . . 8
78	77	rexbidv 2551	. . . . . . 7
79	76	eqeq1d 2247	. . . . . . . 8
80	79	ralbidv 2550	. . . . . . 7
81	78, 80	orbi12d 805	. . . . . 6 $\/$ $\/$
82		simplr 533	. . . . . 6 $/\$ $\/$ $/\$ $\/$
83	9	2o01f 16938	. . . . . . . 8
84		elmapi 6934	. . . . . . . . 9
85	84	adantl 277	. . . . . . . 8 $/\$ $\/$ $/\$
86		fco2 5549	. . . . . . . 8 $/\$
87	83, 85, 86	sylancr 418	. . . . . . 7 $/\$ $\/$ $/\$
88		prexg 4344	. . . . . . . . . 10 $/\$
89	31, 32, 88	mp2an 430	. . . . . . . . 9
90	89	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
91		simpll 531	. . . . . . . 8 $/\$ $\/$ $/\$
92	90, 91	elmapd 6926	. . . . . . 7 $/\$ $\/$ $/\$
93	87, 92	mpbird 167	. . . . . 6 $/\$ $\/$ $/\$
94	81, 82, 93	rspcdva 2934	. . . . 5 $/\$ $\/$ $/\$ $\/$
95		nfcv 2392	. . . . . . . . . 10
96		nfre1 2593	. . . . . . . . . . 11
97		nfra1 2581	. . . . . . . . . . 11
98	96, 97	nfor 1627	. . . . . . . . . 10 $\/$
99	95, 98	nfralxy 2588	. . . . . . . . 9 $\/$
100	21, 99	nfan 1618	. . . . . . . 8 $/\$ $\/$
101		nfv 1581	. . . . . . . 8
102	100, 101	nfan 1618	. . . . . . 7 $/\$ $\/$ $/\$
103	84	ad2antlr 493	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
104		omelon 4751	. . . . . . . . . . . . . . . 16
105	104	onelssi 4569	. . . . . . . . . . . . . . 15
106	15, 105	ax-mp 5	. . . . . . . . . . . . . 14
107	106	a1i 9	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
108	103, 107	fssd 5542	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
109		simpr 110	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
110	108, 109	ffvelcdmd 5835	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
111		f1ocnvfv1 5973	. . . . . . . . . . 11 $/\$
112	30, 110, 111	sylancr 418	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
113	112	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
114		fvco3 5770	. . . . . . . . . . . . . 14 $/\$
115	103, 114	sylancom 424	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
116	115	eqeq1d 2247	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
117	116	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
118	117	fveq2d 5694	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
119		f1ocnvfv 5975	. . . . . . . . . . . 12 $/\$
120	30, 61, 119	mp2an 430	. . . . . . . . . . 11
121	49, 120	ax-mp 5	. . . . . . . . . 10
122	118, 121	eqtrdi 2287	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
123	113, 122	eqtr3d 2273	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
124	123	exp31 364	. . . . . . 7 $/\$ $\/$ $/\$
125	102, 124	reximdai 2648	. . . . . 6 $/\$ $\/$ $/\$
126	112	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
127	115	eqeq1d 2247	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
128	127	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
129	128	fveq2d 5694	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
130		1onn 6783	. . . . . . . . . . . 12
131		f1ocnvfv 5975	. . . . . . . . . . . 12 $/\$
132	30, 130, 131	mp2an 430	. . . . . . . . . . 11
133	68, 132	ax-mp 5	. . . . . . . . . 10
134	129, 133	eqtrdi 2287	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
135	126, 134	eqtr3d 2273	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
136	135	ex 115	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
137	102, 136	ralimdaa 2616	. . . . . 6 $/\$ $\/$ $/\$
138	125, 137	orim12d 798	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
139	94, 138	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
140	139	ralrimiva 2623	. . 3 $/\$ $\/$ $\/$
141	75, 140	impbida 604	. 2 $\/$ $\/$
142	1, 141	bitrd 188	1 Omni $\/$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $\/$ wo 720

wceq 1402

wtru 1403

wcel 2209

wral 2528

wrex 2529

cvv 2821

wss 3220

c0 3520

cpr 3706

cmpt 4187

csuc 4505

com 4732

ccnv 4768

cres 4771

ccom 4773

wf 5368

wf1o 5371

cfv 5372 (class class class)co 6075 freccfrec 6651

c1o 6670

c2o 6671

cmap 6912 Omnicomni 7464

cc0 8169

c1 8170

caddc 8172

cn0 9542

cz 9623

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-coll 4241 ax-sep 4244 ax-nul 4254 ax-pow 4306 ax-pr 4341 ax-un 4573 ax-setind 4679 ax-iinf 4730 ax-cnex 8260 ax-resscn 8261 ax-1cn 8262 ax-1re 8263 ax-icn 8264 ax-addcl 8265 ax-addrcl 8266 ax-mulcl 8267 ax-addcom 8269 ax-addass 8271 ax-distr 8273 ax-i2m1 8274 ax-0lt1 8275 ax-0id 8277 ax-rnegex 8278 ax-cnre 8280 ax-pre-ltirr 8281 ax-pre-ltwlin 8282 ax-pre-lttrn 8283 ax-pre-ltadd 8285

This theorem depends on definitions: df-bi 117 df-3or 1010 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-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-pw 3687 df-sn 3711 df-pr 3712 df-op 3714 df-uni 3931 df-int 3966 df-iun 4009 df-br 4126 df-opab 4188 df-mpt 4189 df-tr 4225 df-id 4433 df-iord 4506 df-on 4508 df-ilim 4509 df-suc 4511 df-iom 4733 df-xp 4775 df-rel 4776 df-cnv 4777 df-co 4778 df-dm 4779 df-rn 4780 df-res 4781 df-ima 4782 df-iota 5332 df-fun 5374 df-fn 5375 df-f 5376 df-f1 5377 df-fo 5378 df-f1o 5379 df-fv 5380 df-riota 6028 df-ov 6078 df-oprab 6079 df-mpo 6080 df-recs 6566 df-frec 6652 df-1o 6677 df-2o 6678 df-map 6914 df-omni 7465 df-pnf 8352 df-mnf 8353 df-xr 8354 df-ltxr 8355 df-le 8356 df-sub 8489 df-neg 8490 df-inn 9284 df-n0 9543 df-z 9624 df-uz 9901

This theorem is referenced by: isomninn 16985

W3C validator