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 16110

Description: Lemma for isomninn 16111. 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 7254	. 2 Omni $\/$
2		fveq1 5588	. . . . . . . . 9
3	2	eqeq1d 2215	. . . . . . . 8
4	3	rexbidv 2508	. . . . . . 7
5	2	eqeq1d 2215	. . . . . . . 8
6	5	ralbidv 2507	. . . . . . 7
7	4, 6	orbi12d 795	. . . . . 6 $\/$ $\/$
8		simplr 528	. . . . . 6 $/\$ $\/$ $/\$ $\/$
9		isomninnlem.g	. . . . . . . . 9 frec
10	9	012of 16069	. . . . . . . 8
11		elmapi 6770	. . . . . . . . 9
12	11	adantl 277	. . . . . . . 8 $/\$ $\/$ $/\$
13		fco2 5452	. . . . . . . 8 $/\$
14	10, 12, 13	sylancr 414	. . . . . . 7 $/\$ $\/$ $/\$
15		2onn 6620	. . . . . . . . 9
16	15	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
17		simpll 527	. . . . . . . 8 $/\$ $\/$ $/\$
18	16, 17	elmapd 6762	. . . . . . 7 $/\$ $\/$ $/\$
19	14, 18	mpbird 167	. . . . . 6 $/\$ $\/$ $/\$
20	7, 8, 19	rspcdva 2886	. . . . 5 $/\$ $\/$ $/\$ $\/$
21		nfv 1552	. . . . . . . . 9
22		nfcv 2349	. . . . . . . . . 10
23		nfre1 2550	. . . . . . . . . . 11
24		nfra1 2538	. . . . . . . . . . 11
25	23, 24	nfor 1598	. . . . . . . . . 10 $\/$
26	22, 25	nfralxy 2545	. . . . . . . . 9 $\/$
27	21, 26	nfan 1589	. . . . . . . 8 $/\$ $\/$
28		nfv 1552	. . . . . . . 8
29	27, 28	nfan 1589	. . . . . . 7 $/\$ $\/$ $/\$
30	9	frechashgf1o 10595	. . . . . . . . . . 11
31		0nn0 9330	. . . . . . . . . . . . 13
32		1nn0 9331	. . . . . . . . . . . . 13
33		prssi 3797	. . . . . . . . . . . . 13 $/\$
34	31, 32, 33	mp2an 426	. . . . . . . . . . . 12
35	11	ad2antlr 489	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
36		simpr 110	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
37	35, 36	ffvelcdmd 5729	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
38	34, 37	sselid 3195	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
39		f1ocnvfv2 5860	. . . . . . . . . . 11 $/\$
40	30, 38, 39	sylancr 414	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
41	40	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
42		fvco3 5663	. . . . . . . . . . . . . 14 $/\$
43	35, 42	sylancom 420	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
44	43	eqeq1d 2215	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
45	44	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
46	45	fveq2d 5593	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
47		0zd 9404	. . . . . . . . . . . 12
48	47, 9	frec2uz0d 10566	. . . . . . . . . . 11
49	48	mptru 1382	. . . . . . . . . 10
50	46, 49	eqtrdi 2255	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
51	41, 50	eqtr3d 2241	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
52	51	exp31 364	. . . . . . 7 $/\$ $\/$ $/\$
53	29, 52	reximdai 2605	. . . . . 6 $/\$ $\/$ $/\$
54	40	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
55	43	adantr 276	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
56		simpr 110	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
57	55, 56	eqtr3d 2241	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
58	57	fveq2d 5593	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
59		df-1o 6515	. . . . . . . . . . . 12
60	59	fveq2i 5592	. . . . . . . . . . 11
61		peano1 4650	. . . . . . . . . . . . . 14
62	61	a1i 9	. . . . . . . . . . . . 13
63	47, 9, 62	frec2uzsucd 10568	. . . . . . . . . . . 12
64	63	mptru 1382	. . . . . . . . . . 11
65	49	oveq1i 5967	. . . . . . . . . . . 12
66		0p1e1 9170	. . . . . . . . . . . 12
67	65, 66	eqtri 2227	. . . . . . . . . . 11
68	60, 64, 67	3eqtri 2231	. . . . . . . . . 10
69	58, 68	eqtrdi 2255	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
70	54, 69	eqtr3d 2241	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
71	70	ex 115	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
72	29, 71	ralimdaa 2573	. . . . . 6 $/\$ $\/$ $/\$
73	53, 72	orim12d 788	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
74	20, 73	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
75	74	ralrimiva 2580	. . 3 $/\$ $\/$ $\/$
76		fveq1 5588	. . . . . . . . 9
77	76	eqeq1d 2215	. . . . . . . 8
78	77	rexbidv 2508	. . . . . . 7
79	76	eqeq1d 2215	. . . . . . . 8
80	79	ralbidv 2507	. . . . . . 7
81	78, 80	orbi12d 795	. . . . . 6 $\/$ $\/$
82		simplr 528	. . . . . 6 $/\$ $\/$ $/\$ $\/$
83	9	2o01f 16070	. . . . . . . 8
84		elmapi 6770	. . . . . . . . 9
85	84	adantl 277	. . . . . . . 8 $/\$ $\/$ $/\$
86		fco2 5452	. . . . . . . 8 $/\$
87	83, 85, 86	sylancr 414	. . . . . . 7 $/\$ $\/$ $/\$
88		prexg 4263	. . . . . . . . . 10 $/\$
89	31, 32, 88	mp2an 426	. . . . . . . . 9
90	89	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
91		simpll 527	. . . . . . . 8 $/\$ $\/$ $/\$
92	90, 91	elmapd 6762	. . . . . . 7 $/\$ $\/$ $/\$
93	87, 92	mpbird 167	. . . . . 6 $/\$ $\/$ $/\$
94	81, 82, 93	rspcdva 2886	. . . . 5 $/\$ $\/$ $/\$ $\/$
95		nfcv 2349	. . . . . . . . . 10
96		nfre1 2550	. . . . . . . . . . 11
97		nfra1 2538	. . . . . . . . . . 11
98	96, 97	nfor 1598	. . . . . . . . . 10 $\/$
99	95, 98	nfralxy 2545	. . . . . . . . 9 $\/$
100	21, 99	nfan 1589	. . . . . . . 8 $/\$ $\/$
101		nfv 1552	. . . . . . . 8
102	100, 101	nfan 1589	. . . . . . 7 $/\$ $\/$ $/\$
103	84	ad2antlr 489	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
104		omelon 4665	. . . . . . . . . . . . . . . 16
105	104	onelssi 4484	. . . . . . . . . . . . . . 15
106	15, 105	ax-mp 5	. . . . . . . . . . . . . 14
107	106	a1i 9	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
108	103, 107	fssd 5448	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
109		simpr 110	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
110	108, 109	ffvelcdmd 5729	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
111		f1ocnvfv1 5859	. . . . . . . . . . 11 $/\$
112	30, 110, 111	sylancr 414	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
113	112	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
114		fvco3 5663	. . . . . . . . . . . . . 14 $/\$
115	103, 114	sylancom 420	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
116	115	eqeq1d 2215	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
117	116	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
118	117	fveq2d 5593	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
119		f1ocnvfv 5861	. . . . . . . . . . . 12 $/\$
120	30, 61, 119	mp2an 426	. . . . . . . . . . 11
121	49, 120	ax-mp 5	. . . . . . . . . 10
122	118, 121	eqtrdi 2255	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
123	113, 122	eqtr3d 2241	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
124	123	exp31 364	. . . . . . 7 $/\$ $\/$ $/\$
125	102, 124	reximdai 2605	. . . . . 6 $/\$ $\/$ $/\$
126	112	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
127	115	eqeq1d 2215	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
128	127	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
129	128	fveq2d 5593	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
130		1onn 6619	. . . . . . . . . . . 12
131		f1ocnvfv 5861	. . . . . . . . . . . 12 $/\$
132	30, 130, 131	mp2an 426	. . . . . . . . . . 11
133	68, 132	ax-mp 5	. . . . . . . . . 10
134	129, 133	eqtrdi 2255	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
135	126, 134	eqtr3d 2241	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
136	135	ex 115	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
137	102, 136	ralimdaa 2573	. . . . . 6 $/\$ $\/$ $/\$
138	125, 137	orim12d 788	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
139	94, 138	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
140	139	ralrimiva 2580	. . 3 $/\$ $\/$ $\/$
141	75, 140	impbida 596	. 2 $\/$ $\/$
142	1, 141	bitrd 188	1 Omni $\/$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $\/$ wo 710

wceq 1373

wtru 1374

wcel 2177

wral 2485

wrex 2486

cvv 2773

wss 3170

c0 3464

cpr 3639

cmpt 4113

csuc 4420

com 4646

ccnv 4682

cres 4685

ccom 4687

wf 5276

wf1o 5279

cfv 5280 (class class class)co 5957 freccfrec 6489

c1o 6508

c2o 6509

cmap 6748 Omnicomni 7251

cc0 7945

c1 7946

caddc 7948

cn0 9315

cz 9392

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4167 ax-sep 4170 ax-nul 4178 ax-pow 4226 ax-pr 4261 ax-un 4488 ax-setind 4593 ax-iinf 4644 ax-cnex 8036 ax-resscn 8037 ax-1cn 8038 ax-1re 8039 ax-icn 8040 ax-addcl 8041 ax-addrcl 8042 ax-mulcl 8043 ax-addcom 8045 ax-addass 8047 ax-distr 8049 ax-i2m1 8050 ax-0lt1 8051 ax-0id 8053 ax-rnegex 8054 ax-cnre 8056 ax-pre-ltirr 8057 ax-pre-ltwlin 8058 ax-pre-lttrn 8059 ax-pre-ltadd 8061

This theorem depends on definitions: df-bi 117 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-nul 3465 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3857 df-int 3892 df-iun 3935 df-br 4052 df-opab 4114 df-mpt 4115 df-tr 4151 df-id 4348 df-iord 4421 df-on 4423 df-ilim 4424 df-suc 4426 df-iom 4647 df-xp 4689 df-rel 4690 df-cnv 4691 df-co 4692 df-dm 4693 df-rn 4694 df-res 4695 df-ima 4696 df-iota 5241 df-fun 5282 df-fn 5283 df-f 5284 df-f1 5285 df-fo 5286 df-f1o 5287 df-fv 5288 df-riota 5912 df-ov 5960 df-oprab 5961 df-mpo 5962 df-recs 6404 df-frec 6490 df-1o 6515 df-2o 6516 df-map 6750 df-omni 7252 df-pnf 8129 df-mnf 8130 df-xr 8131 df-ltxr 8132 df-le 8133 df-sub 8265 df-neg 8266 df-inn 9057 df-n0 9316 df-z 9393 df-uz 9669

This theorem is referenced by: isomninn 16111

W3C validator