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 15176

Description: Lemma for isomninn 15177. 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 7153	. 2 Omni $\/$
2		fveq1 5529	. . . . . . . . 9
3	2	eqeq1d 2198	. . . . . . . 8
4	3	rexbidv 2491	. . . . . . 7
5	2	eqeq1d 2198	. . . . . . . 8
6	5	ralbidv 2490	. . . . . . 7
7	4, 6	orbi12d 794	. . . . . 6 $\/$ $\/$
8		simplr 528	. . . . . 6 $/\$ $\/$ $/\$ $\/$
9		isomninnlem.g	. . . . . . . . 9 frec
10	9	012of 15143	. . . . . . . 8
11		elmapi 6688	. . . . . . . . 9
12	11	adantl 277	. . . . . . . 8 $/\$ $\/$ $/\$
13		fco2 5397	. . . . . . . 8 $/\$
14	10, 12, 13	sylancr 414	. . . . . . 7 $/\$ $\/$ $/\$
15		2onn 6540	. . . . . . . . 9
16	15	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
17		simpll 527	. . . . . . . 8 $/\$ $\/$ $/\$
18	16, 17	elmapd 6680	. . . . . . 7 $/\$ $\/$ $/\$
19	14, 18	mpbird 167	. . . . . 6 $/\$ $\/$ $/\$
20	7, 8, 19	rspcdva 2861	. . . . 5 $/\$ $\/$ $/\$ $\/$
21		nfv 1539	. . . . . . . . 9
22		nfcv 2332	. . . . . . . . . 10
23		nfre1 2533	. . . . . . . . . . 11
24		nfra1 2521	. . . . . . . . . . 11
25	23, 24	nfor 1585	. . . . . . . . . 10 $\/$
26	22, 25	nfralxy 2528	. . . . . . . . 9 $\/$
27	21, 26	nfan 1576	. . . . . . . 8 $/\$ $\/$
28		nfv 1539	. . . . . . . 8
29	27, 28	nfan 1576	. . . . . . 7 $/\$ $\/$ $/\$
30	9	frechashgf1o 10446	. . . . . . . . . . 11
31		0nn0 9209	. . . . . . . . . . . . 13
32		1nn0 9210	. . . . . . . . . . . . 13
33		prssi 3765	. . . . . . . . . . . . 13 $/\$
34	31, 32, 33	mp2an 426	. . . . . . . . . . . 12
35	11	ad2antlr 489	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
36		simpr 110	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
37	35, 36	ffvelcdmd 5668	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
38	34, 37	sselid 3168	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
39		f1ocnvfv2 5795	. . . . . . . . . . 11 $/\$
40	30, 38, 39	sylancr 414	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
41	40	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
42		fvco3 5603	. . . . . . . . . . . . . 14 $/\$
43	35, 42	sylancom 420	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
44	43	eqeq1d 2198	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
45	44	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
46	45	fveq2d 5534	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
47		0zd 9283	. . . . . . . . . . . 12
48	47, 9	frec2uz0d 10417	. . . . . . . . . . 11
49	48	mptru 1373	. . . . . . . . . 10
50	46, 49	eqtrdi 2238	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
51	41, 50	eqtr3d 2224	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
52	51	exp31 364	. . . . . . 7 $/\$ $\/$ $/\$
53	29, 52	reximdai 2588	. . . . . 6 $/\$ $\/$ $/\$
54	40	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
55	43	adantr 276	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
56		simpr 110	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
57	55, 56	eqtr3d 2224	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
58	57	fveq2d 5534	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
59		df-1o 6435	. . . . . . . . . . . 12
60	59	fveq2i 5533	. . . . . . . . . . 11
61		peano1 4608	. . . . . . . . . . . . . 14
62	61	a1i 9	. . . . . . . . . . . . 13
63	47, 9, 62	frec2uzsucd 10419	. . . . . . . . . . . 12
64	63	mptru 1373	. . . . . . . . . . 11
65	49	oveq1i 5901	. . . . . . . . . . . 12
66		0p1e1 9051	. . . . . . . . . . . 12
67	65, 66	eqtri 2210	. . . . . . . . . . 11
68	60, 64, 67	3eqtri 2214	. . . . . . . . . 10
69	58, 68	eqtrdi 2238	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
70	54, 69	eqtr3d 2224	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
71	70	ex 115	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
72	29, 71	ralimdaa 2556	. . . . . 6 $/\$ $\/$ $/\$
73	53, 72	orim12d 787	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
74	20, 73	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
75	74	ralrimiva 2563	. . 3 $/\$ $\/$ $\/$
76		fveq1 5529	. . . . . . . . 9
77	76	eqeq1d 2198	. . . . . . . 8
78	77	rexbidv 2491	. . . . . . 7
79	76	eqeq1d 2198	. . . . . . . 8
80	79	ralbidv 2490	. . . . . . 7
81	78, 80	orbi12d 794	. . . . . 6 $\/$ $\/$
82		simplr 528	. . . . . 6 $/\$ $\/$ $/\$ $\/$
83	9	2o01f 15144	. . . . . . . 8
84		elmapi 6688	. . . . . . . . 9
85	84	adantl 277	. . . . . . . 8 $/\$ $\/$ $/\$
86		fco2 5397	. . . . . . . 8 $/\$
87	83, 85, 86	sylancr 414	. . . . . . 7 $/\$ $\/$ $/\$
88		prexg 4226	. . . . . . . . . 10 $/\$
89	31, 32, 88	mp2an 426	. . . . . . . . 9
90	89	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
91		simpll 527	. . . . . . . 8 $/\$ $\/$ $/\$
92	90, 91	elmapd 6680	. . . . . . 7 $/\$ $\/$ $/\$
93	87, 92	mpbird 167	. . . . . 6 $/\$ $\/$ $/\$
94	81, 82, 93	rspcdva 2861	. . . . 5 $/\$ $\/$ $/\$ $\/$
95		nfcv 2332	. . . . . . . . . 10
96		nfre1 2533	. . . . . . . . . . 11
97		nfra1 2521	. . . . . . . . . . 11
98	96, 97	nfor 1585	. . . . . . . . . 10 $\/$
99	95, 98	nfralxy 2528	. . . . . . . . 9 $\/$
100	21, 99	nfan 1576	. . . . . . . 8 $/\$ $\/$
101		nfv 1539	. . . . . . . 8
102	100, 101	nfan 1576	. . . . . . 7 $/\$ $\/$ $/\$
103	84	ad2antlr 489	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
104		omelon 4623	. . . . . . . . . . . . . . . 16
105	104	onelssi 4444	. . . . . . . . . . . . . . 15
106	15, 105	ax-mp 5	. . . . . . . . . . . . . 14
107	106	a1i 9	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
108	103, 107	fssd 5393	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
109		simpr 110	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
110	108, 109	ffvelcdmd 5668	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
111		f1ocnvfv1 5794	. . . . . . . . . . 11 $/\$
112	30, 110, 111	sylancr 414	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
113	112	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
114		fvco3 5603	. . . . . . . . . . . . . 14 $/\$
115	103, 114	sylancom 420	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
116	115	eqeq1d 2198	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
117	116	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
118	117	fveq2d 5534	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
119		f1ocnvfv 5796	. . . . . . . . . . . 12 $/\$
120	30, 61, 119	mp2an 426	. . . . . . . . . . 11
121	49, 120	ax-mp 5	. . . . . . . . . 10
122	118, 121	eqtrdi 2238	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
123	113, 122	eqtr3d 2224	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
124	123	exp31 364	. . . . . . 7 $/\$ $\/$ $/\$
125	102, 124	reximdai 2588	. . . . . 6 $/\$ $\/$ $/\$
126	112	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
127	115	eqeq1d 2198	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
128	127	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
129	128	fveq2d 5534	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
130		1onn 6539	. . . . . . . . . . . 12
131		f1ocnvfv 5796	. . . . . . . . . . . 12 $/\$
132	30, 130, 131	mp2an 426	. . . . . . . . . . 11
133	68, 132	ax-mp 5	. . . . . . . . . 10
134	129, 133	eqtrdi 2238	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
135	126, 134	eqtr3d 2224	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
136	135	ex 115	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
137	102, 136	ralimdaa 2556	. . . . . 6 $/\$ $\/$ $/\$
138	125, 137	orim12d 787	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
139	94, 138	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
140	139	ralrimiva 2563	. . 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 2160

wral 2468

wrex 2469

cvv 2752

wss 3144

c0 3437

cpr 3608

cmpt 4079

csuc 4380

com 4604

ccnv 4640

cres 4643

ccom 4645

wf 5227

wf1o 5230

cfv 5231 (class class class)co 5891 freccfrec 6409

c1o 6428

c2o 6429

cmap 6666 Omnicomni 7150

cc0 7829

c1 7830

caddc 7832

cn0 9194

cz 9271

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 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4189 ax-pr 4224 ax-un 4448 ax-setind 4551 ax-iinf 4602 ax-cnex 7920 ax-resscn 7921 ax-1cn 7922 ax-1re 7923 ax-icn 7924 ax-addcl 7925 ax-addrcl 7926 ax-mulcl 7927 ax-addcom 7929 ax-addass 7931 ax-distr 7933 ax-i2m1 7934 ax-0lt1 7935 ax-0id 7937 ax-rnegex 7938 ax-cnre 7940 ax-pre-ltirr 7941 ax-pre-ltwlin 7942 ax-pre-lttrn 7943 ax-pre-ltadd 7945

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 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4308 df-iord 4381 df-on 4383 df-ilim 4384 df-suc 4386 df-iom 4605 df-xp 4647 df-rel 4648 df-cnv 4649 df-co 4650 df-dm 4651 df-rn 4652 df-res 4653 df-ima 4654 df-iota 5193 df-fun 5233 df-fn 5234 df-f 5235 df-f1 5236 df-fo 5237 df-f1o 5238 df-fv 5239 df-riota 5847 df-ov 5894 df-oprab 5895 df-mpo 5896 df-recs 6324 df-frec 6410 df-1o 6435 df-2o 6436 df-map 6668 df-omni 7151 df-pnf 8012 df-mnf 8013 df-xr 8014 df-ltxr 8015 df-le 8016 df-sub 8148 df-neg 8149 df-inn 8938 df-n0 9195 df-z 9272 df-uz 9547

This theorem is referenced by: isomninn 15177

W3C validator