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 15520

Description: Lemma for isomninn 15521. 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 7196	. 2 Omni $\/$
2		fveq1 5553	. . . . . . . . 9
3	2	eqeq1d 2202	. . . . . . . 8
4	3	rexbidv 2495	. . . . . . 7
5	2	eqeq1d 2202	. . . . . . . 8
6	5	ralbidv 2494	. . . . . . 7
7	4, 6	orbi12d 794	. . . . . 6 $\/$ $\/$
8		simplr 528	. . . . . 6 $/\$ $\/$ $/\$ $\/$
9		isomninnlem.g	. . . . . . . . 9 frec
10	9	012of 15486	. . . . . . . 8
11		elmapi 6724	. . . . . . . . 9
12	11	adantl 277	. . . . . . . 8 $/\$ $\/$ $/\$
13		fco2 5420	. . . . . . . 8 $/\$
14	10, 12, 13	sylancr 414	. . . . . . 7 $/\$ $\/$ $/\$
15		2onn 6574	. . . . . . . . 9
16	15	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
17		simpll 527	. . . . . . . 8 $/\$ $\/$ $/\$
18	16, 17	elmapd 6716	. . . . . . 7 $/\$ $\/$ $/\$
19	14, 18	mpbird 167	. . . . . 6 $/\$ $\/$ $/\$
20	7, 8, 19	rspcdva 2869	. . . . 5 $/\$ $\/$ $/\$ $\/$
21		nfv 1539	. . . . . . . . 9
22		nfcv 2336	. . . . . . . . . 10
23		nfre1 2537	. . . . . . . . . . 11
24		nfra1 2525	. . . . . . . . . . 11
25	23, 24	nfor 1585	. . . . . . . . . 10 $\/$
26	22, 25	nfralxy 2532	. . . . . . . . 9 $\/$
27	21, 26	nfan 1576	. . . . . . . 8 $/\$ $\/$
28		nfv 1539	. . . . . . . 8
29	27, 28	nfan 1576	. . . . . . 7 $/\$ $\/$ $/\$
30	9	frechashgf1o 10499	. . . . . . . . . . 11
31		0nn0 9255	. . . . . . . . . . . . 13
32		1nn0 9256	. . . . . . . . . . . . 13
33		prssi 3776	. . . . . . . . . . . . 13 $/\$
34	31, 32, 33	mp2an 426	. . . . . . . . . . . 12
35	11	ad2antlr 489	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
36		simpr 110	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
37	35, 36	ffvelcdmd 5694	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
38	34, 37	sselid 3177	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
39		f1ocnvfv2 5821	. . . . . . . . . . 11 $/\$
40	30, 38, 39	sylancr 414	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
41	40	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
42		fvco3 5628	. . . . . . . . . . . . . 14 $/\$
43	35, 42	sylancom 420	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
44	43	eqeq1d 2202	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
45	44	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
46	45	fveq2d 5558	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
47		0zd 9329	. . . . . . . . . . . 12
48	47, 9	frec2uz0d 10470	. . . . . . . . . . 11
49	48	mptru 1373	. . . . . . . . . 10
50	46, 49	eqtrdi 2242	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
51	41, 50	eqtr3d 2228	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
52	51	exp31 364	. . . . . . 7 $/\$ $\/$ $/\$
53	29, 52	reximdai 2592	. . . . . 6 $/\$ $\/$ $/\$
54	40	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
55	43	adantr 276	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
56		simpr 110	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
57	55, 56	eqtr3d 2228	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
58	57	fveq2d 5558	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
59		df-1o 6469	. . . . . . . . . . . 12
60	59	fveq2i 5557	. . . . . . . . . . 11
61		peano1 4626	. . . . . . . . . . . . . 14
62	61	a1i 9	. . . . . . . . . . . . 13
63	47, 9, 62	frec2uzsucd 10472	. . . . . . . . . . . 12
64	63	mptru 1373	. . . . . . . . . . 11
65	49	oveq1i 5928	. . . . . . . . . . . 12
66		0p1e1 9096	. . . . . . . . . . . 12
67	65, 66	eqtri 2214	. . . . . . . . . . 11
68	60, 64, 67	3eqtri 2218	. . . . . . . . . 10
69	58, 68	eqtrdi 2242	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
70	54, 69	eqtr3d 2228	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
71	70	ex 115	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
72	29, 71	ralimdaa 2560	. . . . . 6 $/\$ $\/$ $/\$
73	53, 72	orim12d 787	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
74	20, 73	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
75	74	ralrimiva 2567	. . 3 $/\$ $\/$ $\/$
76		fveq1 5553	. . . . . . . . 9
77	76	eqeq1d 2202	. . . . . . . 8
78	77	rexbidv 2495	. . . . . . 7
79	76	eqeq1d 2202	. . . . . . . 8
80	79	ralbidv 2494	. . . . . . 7
81	78, 80	orbi12d 794	. . . . . 6 $\/$ $\/$
82		simplr 528	. . . . . 6 $/\$ $\/$ $/\$ $\/$
83	9	2o01f 15487	. . . . . . . 8
84		elmapi 6724	. . . . . . . . 9
85	84	adantl 277	. . . . . . . 8 $/\$ $\/$ $/\$
86		fco2 5420	. . . . . . . 8 $/\$
87	83, 85, 86	sylancr 414	. . . . . . 7 $/\$ $\/$ $/\$
88		prexg 4240	. . . . . . . . . 10 $/\$
89	31, 32, 88	mp2an 426	. . . . . . . . 9
90	89	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
91		simpll 527	. . . . . . . 8 $/\$ $\/$ $/\$
92	90, 91	elmapd 6716	. . . . . . 7 $/\$ $\/$ $/\$
93	87, 92	mpbird 167	. . . . . 6 $/\$ $\/$ $/\$
94	81, 82, 93	rspcdva 2869	. . . . 5 $/\$ $\/$ $/\$ $\/$
95		nfcv 2336	. . . . . . . . . 10
96		nfre1 2537	. . . . . . . . . . 11
97		nfra1 2525	. . . . . . . . . . 11
98	96, 97	nfor 1585	. . . . . . . . . 10 $\/$
99	95, 98	nfralxy 2532	. . . . . . . . 9 $\/$
100	21, 99	nfan 1576	. . . . . . . 8 $/\$ $\/$
101		nfv 1539	. . . . . . . 8
102	100, 101	nfan 1576	. . . . . . 7 $/\$ $\/$ $/\$
103	84	ad2antlr 489	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
104		omelon 4641	. . . . . . . . . . . . . . . 16
105	104	onelssi 4460	. . . . . . . . . . . . . . 15
106	15, 105	ax-mp 5	. . . . . . . . . . . . . 14
107	106	a1i 9	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
108	103, 107	fssd 5416	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
109		simpr 110	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
110	108, 109	ffvelcdmd 5694	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
111		f1ocnvfv1 5820	. . . . . . . . . . 11 $/\$
112	30, 110, 111	sylancr 414	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
113	112	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
114		fvco3 5628	. . . . . . . . . . . . . 14 $/\$
115	103, 114	sylancom 420	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
116	115	eqeq1d 2202	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
117	116	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
118	117	fveq2d 5558	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
119		f1ocnvfv 5822	. . . . . . . . . . . 12 $/\$
120	30, 61, 119	mp2an 426	. . . . . . . . . . 11
121	49, 120	ax-mp 5	. . . . . . . . . 10
122	118, 121	eqtrdi 2242	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
123	113, 122	eqtr3d 2228	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
124	123	exp31 364	. . . . . . 7 $/\$ $\/$ $/\$
125	102, 124	reximdai 2592	. . . . . 6 $/\$ $\/$ $/\$
126	112	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
127	115	eqeq1d 2202	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
128	127	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
129	128	fveq2d 5558	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
130		1onn 6573	. . . . . . . . . . . 12
131		f1ocnvfv 5822	. . . . . . . . . . . 12 $/\$
132	30, 130, 131	mp2an 426	. . . . . . . . . . 11
133	68, 132	ax-mp 5	. . . . . . . . . 10
134	129, 133	eqtrdi 2242	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
135	126, 134	eqtr3d 2228	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
136	135	ex 115	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
137	102, 136	ralimdaa 2560	. . . . . 6 $/\$ $\/$ $/\$
138	125, 137	orim12d 787	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
139	94, 138	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
140	139	ralrimiva 2567	. . 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 709

wceq 1364

wtru 1365

wcel 2164

wral 2472

wrex 2473

cvv 2760

wss 3153

c0 3446

cpr 3619

cmpt 4090

csuc 4396

com 4622

ccnv 4658

cres 4661

ccom 4663

wf 5250

wf1o 5253

cfv 5254 (class class class)co 5918 freccfrec 6443

c1o 6462

c2o 6463

cmap 6702 Omnicomni 7193

cc0 7872

c1 7873

caddc 7875

cn0 9240

cz 9317

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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4144 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-iinf 4620 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-addcom 7972 ax-addass 7974 ax-distr 7976 ax-i2m1 7977 ax-0lt1 7978 ax-0id 7980 ax-rnegex 7981 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-ltadd 7988

This theorem depends on definitions: df-bi 117 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-iord 4397 df-on 4399 df-ilim 4400 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-f1 5259 df-fo 5260 df-f1o 5261 df-fv 5262 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-recs 6358 df-frec 6444 df-1o 6469 df-2o 6470 df-map 6704 df-omni 7194 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-sub 8192 df-neg 8193 df-inn 8983 df-n0 9241 df-z 9318 df-uz 9593

This theorem is referenced by: isomninn 15521

W3C validator