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 14022

Description: Lemma for isomninn 14023. 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 7109	. 2 Omni $\/$
2		fveq1 5493	. . . . . . . . 9
3	2	eqeq1d 2179	. . . . . . . 8
4	3	rexbidv 2471	. . . . . . 7
5	2	eqeq1d 2179	. . . . . . . 8
6	5	ralbidv 2470	. . . . . . 7
7	4, 6	orbi12d 788	. . . . . 6 $\/$ $\/$
8		simplr 525	. . . . . 6 $/\$ $\/$ $/\$ $\/$
9		isomninnlem.g	. . . . . . . . 9 frec
10	9	012of 13988	. . . . . . . 8
11		elmapi 6644	. . . . . . . . 9
12	11	adantl 275	. . . . . . . 8 $/\$ $\/$ $/\$
13		fco2 5362	. . . . . . . 8 $/\$
14	10, 12, 13	sylancr 412	. . . . . . 7 $/\$ $\/$ $/\$
15		2onn 6497	. . . . . . . . 9
16	15	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
17		simpll 524	. . . . . . . 8 $/\$ $\/$ $/\$
18	16, 17	elmapd 6636	. . . . . . 7 $/\$ $\/$ $/\$
19	14, 18	mpbird 166	. . . . . 6 $/\$ $\/$ $/\$
20	7, 8, 19	rspcdva 2839	. . . . 5 $/\$ $\/$ $/\$ $\/$
21		nfv 1521	. . . . . . . . 9
22		nfcv 2312	. . . . . . . . . 10
23		nfre1 2513	. . . . . . . . . . 11
24		nfra1 2501	. . . . . . . . . . 11
25	23, 24	nfor 1567	. . . . . . . . . 10 $\/$
26	22, 25	nfralxy 2508	. . . . . . . . 9 $\/$
27	21, 26	nfan 1558	. . . . . . . 8 $/\$ $\/$
28		nfv 1521	. . . . . . . 8
29	27, 28	nfan 1558	. . . . . . 7 $/\$ $\/$ $/\$
30	9	frechashgf1o 10371	. . . . . . . . . . 11
31		0nn0 9137	. . . . . . . . . . . . 13
32		1nn0 9138	. . . . . . . . . . . . 13
33		prssi 3736	. . . . . . . . . . . . 13 $/\$
34	31, 32, 33	mp2an 424	. . . . . . . . . . . 12
35	11	ad2antlr 486	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
36		simpr 109	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
37	35, 36	ffvelrnd 5629	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
38	34, 37	sselid 3145	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
39		f1ocnvfv2 5754	. . . . . . . . . . 11 $/\$
40	30, 38, 39	sylancr 412	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
41	40	adantr 274	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
42		fvco3 5565	. . . . . . . . . . . . . 14 $/\$
43	35, 42	sylancom 418	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
44	43	eqeq1d 2179	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
45	44	biimpa 294	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
46	45	fveq2d 5498	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
47		0zd 9211	. . . . . . . . . . . 12
48	47, 9	frec2uz0d 10342	. . . . . . . . . . 11
49	48	mptru 1357	. . . . . . . . . 10
50	46, 49	eqtrdi 2219	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
51	41, 50	eqtr3d 2205	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
52	51	exp31 362	. . . . . . 7 $/\$ $\/$ $/\$
53	29, 52	reximdai 2568	. . . . . 6 $/\$ $\/$ $/\$
54	40	adantr 274	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
55	43	adantr 274	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
56		simpr 109	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
57	55, 56	eqtr3d 2205	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
58	57	fveq2d 5498	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
59		df-1o 6392	. . . . . . . . . . . 12
60	59	fveq2i 5497	. . . . . . . . . . 11
61		peano1 4576	. . . . . . . . . . . . . 14
62	61	a1i 9	. . . . . . . . . . . . 13
63	47, 9, 62	frec2uzsucd 10344	. . . . . . . . . . . 12
64	63	mptru 1357	. . . . . . . . . . 11
65	49	oveq1i 5860	. . . . . . . . . . . 12
66		0p1e1 8979	. . . . . . . . . . . 12
67	65, 66	eqtri 2191	. . . . . . . . . . 11
68	60, 64, 67	3eqtri 2195	. . . . . . . . . 10
69	58, 68	eqtrdi 2219	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
70	54, 69	eqtr3d 2205	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
71	70	ex 114	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
72	29, 71	ralimdaa 2536	. . . . . 6 $/\$ $\/$ $/\$
73	53, 72	orim12d 781	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
74	20, 73	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
75	74	ralrimiva 2543	. . 3 $/\$ $\/$ $\/$
76		fveq1 5493	. . . . . . . . 9
77	76	eqeq1d 2179	. . . . . . . 8
78	77	rexbidv 2471	. . . . . . 7
79	76	eqeq1d 2179	. . . . . . . 8
80	79	ralbidv 2470	. . . . . . 7
81	78, 80	orbi12d 788	. . . . . 6 $\/$ $\/$
82		simplr 525	. . . . . 6 $/\$ $\/$ $/\$ $\/$
83	9	2o01f 13989	. . . . . . . 8
84		elmapi 6644	. . . . . . . . 9
85	84	adantl 275	. . . . . . . 8 $/\$ $\/$ $/\$
86		fco2 5362	. . . . . . . 8 $/\$
87	83, 85, 86	sylancr 412	. . . . . . 7 $/\$ $\/$ $/\$
88		prexg 4194	. . . . . . . . . 10 $/\$
89	31, 32, 88	mp2an 424	. . . . . . . . 9
90	89	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
91		simpll 524	. . . . . . . 8 $/\$ $\/$ $/\$
92	90, 91	elmapd 6636	. . . . . . 7 $/\$ $\/$ $/\$
93	87, 92	mpbird 166	. . . . . 6 $/\$ $\/$ $/\$
94	81, 82, 93	rspcdva 2839	. . . . 5 $/\$ $\/$ $/\$ $\/$
95		nfcv 2312	. . . . . . . . . 10
96		nfre1 2513	. . . . . . . . . . 11
97		nfra1 2501	. . . . . . . . . . 11
98	96, 97	nfor 1567	. . . . . . . . . 10 $\/$
99	95, 98	nfralxy 2508	. . . . . . . . 9 $\/$
100	21, 99	nfan 1558	. . . . . . . 8 $/\$ $\/$
101		nfv 1521	. . . . . . . 8
102	100, 101	nfan 1558	. . . . . . 7 $/\$ $\/$ $/\$
103	84	ad2antlr 486	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
104		omelon 4591	. . . . . . . . . . . . . . . 16
105	104	onelssi 4412	. . . . . . . . . . . . . . 15
106	15, 105	ax-mp 5	. . . . . . . . . . . . . 14
107	106	a1i 9	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
108	103, 107	fssd 5358	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
109		simpr 109	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
110	108, 109	ffvelrnd 5629	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
111		f1ocnvfv1 5753	. . . . . . . . . . 11 $/\$
112	30, 110, 111	sylancr 412	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
113	112	adantr 274	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
114		fvco3 5565	. . . . . . . . . . . . . 14 $/\$
115	103, 114	sylancom 418	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
116	115	eqeq1d 2179	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
117	116	biimpa 294	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
118	117	fveq2d 5498	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
119		f1ocnvfv 5755	. . . . . . . . . . . 12 $/\$
120	30, 61, 119	mp2an 424	. . . . . . . . . . 11
121	49, 120	ax-mp 5	. . . . . . . . . 10
122	118, 121	eqtrdi 2219	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
123	113, 122	eqtr3d 2205	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
124	123	exp31 362	. . . . . . 7 $/\$ $\/$ $/\$
125	102, 124	reximdai 2568	. . . . . 6 $/\$ $\/$ $/\$
126	112	adantr 274	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
127	115	eqeq1d 2179	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
128	127	biimpa 294	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
129	128	fveq2d 5498	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
130		1onn 6496	. . . . . . . . . . . 12
131		f1ocnvfv 5755	. . . . . . . . . . . 12 $/\$
132	30, 130, 131	mp2an 424	. . . . . . . . . . 11
133	68, 132	ax-mp 5	. . . . . . . . . 10
134	129, 133	eqtrdi 2219	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
135	126, 134	eqtr3d 2205	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
136	135	ex 114	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
137	102, 136	ralimdaa 2536	. . . . . 6 $/\$ $\/$ $/\$
138	125, 137	orim12d 781	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
139	94, 138	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
140	139	ralrimiva 2543	. . 3 $/\$ $\/$ $\/$
141	75, 140	impbida 591	. 2 $\/$ $\/$
142	1, 141	bitrd 187	1 Omni $\/$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 703

wceq 1348

wtru 1349

wcel 2141

wral 2448

wrex 2449

cvv 2730

wss 3121

c0 3414

cpr 3582

cmpt 4048

csuc 4348

com 4572

ccnv 4608

cres 4611

ccom 4613

wf 5192

wf1o 5195

cfv 5196 (class class class)co 5850 freccfrec 6366

c1o 6385

c2o 6386

cmap 6622 Omnicomni 7106

cc0 7761

c1 7762

caddc 7764

cn0 9122

cz 9199

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 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4102 ax-sep 4105 ax-nul 4113 ax-pow 4158 ax-pr 4192 ax-un 4416 ax-setind 4519 ax-iinf 4570 ax-cnex 7852 ax-resscn 7853 ax-1cn 7854 ax-1re 7855 ax-icn 7856 ax-addcl 7857 ax-addrcl 7858 ax-mulcl 7859 ax-addcom 7861 ax-addass 7863 ax-distr 7865 ax-i2m1 7866 ax-0lt1 7867 ax-0id 7869 ax-rnegex 7870 ax-cnre 7872 ax-pre-ltirr 7873 ax-pre-ltwlin 7874 ax-pre-lttrn 7875 ax-pre-ltadd 7877

This theorem depends on definitions: df-bi 116 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-pw 3566 df-sn 3587 df-pr 3588 df-op 3590 df-uni 3795 df-int 3830 df-iun 3873 df-br 3988 df-opab 4049 df-mpt 4050 df-tr 4086 df-id 4276 df-iord 4349 df-on 4351 df-ilim 4352 df-suc 4354 df-iom 4573 df-xp 4615 df-rel 4616 df-cnv 4617 df-co 4618 df-dm 4619 df-rn 4620 df-res 4621 df-ima 4622 df-iota 5158 df-fun 5198 df-fn 5199 df-f 5200 df-f1 5201 df-fo 5202 df-f1o 5203 df-fv 5204 df-riota 5806 df-ov 5853 df-oprab 5854 df-mpo 5855 df-recs 6281 df-frec 6367 df-1o 6392 df-2o 6393 df-map 6624 df-omni 7107 df-pnf 7943 df-mnf 7944 df-xr 7945 df-ltxr 7946 df-le 7947 df-sub 8079 df-neg 8080 df-inn 8866 df-n0 9123 df-z 9200 df-uz 9475

This theorem is referenced by: isomninn 14023

W3C validator