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 14434

Description: Lemma for isomninn 14435. 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 7129	. 2 Omni $\/$
2		fveq1 5510	. . . . . . . . 9
3	2	eqeq1d 2186	. . . . . . . 8
4	3	rexbidv 2478	. . . . . . 7
5	2	eqeq1d 2186	. . . . . . . 8
6	5	ralbidv 2477	. . . . . . 7
7	4, 6	orbi12d 793	. . . . . 6 $\/$ $\/$
8		simplr 528	. . . . . 6 $/\$ $\/$ $/\$ $\/$
9		isomninnlem.g	. . . . . . . . 9 frec
10	9	012of 14401	. . . . . . . 8
11		elmapi 6664	. . . . . . . . 9
12	11	adantl 277	. . . . . . . 8 $/\$ $\/$ $/\$
13		fco2 5378	. . . . . . . 8 $/\$
14	10, 12, 13	sylancr 414	. . . . . . 7 $/\$ $\/$ $/\$
15		2onn 6516	. . . . . . . . 9
16	15	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
17		simpll 527	. . . . . . . 8 $/\$ $\/$ $/\$
18	16, 17	elmapd 6656	. . . . . . 7 $/\$ $\/$ $/\$
19	14, 18	mpbird 167	. . . . . 6 $/\$ $\/$ $/\$
20	7, 8, 19	rspcdva 2846	. . . . 5 $/\$ $\/$ $/\$ $\/$
21		nfv 1528	. . . . . . . . 9
22		nfcv 2319	. . . . . . . . . 10
23		nfre1 2520	. . . . . . . . . . 11
24		nfra1 2508	. . . . . . . . . . 11
25	23, 24	nfor 1574	. . . . . . . . . 10 $\/$
26	22, 25	nfralxy 2515	. . . . . . . . 9 $\/$
27	21, 26	nfan 1565	. . . . . . . 8 $/\$ $\/$
28		nfv 1528	. . . . . . . 8
29	27, 28	nfan 1565	. . . . . . 7 $/\$ $\/$ $/\$
30	9	frechashgf1o 10414	. . . . . . . . . . 11
31		0nn0 9180	. . . . . . . . . . . . 13
32		1nn0 9181	. . . . . . . . . . . . 13
33		prssi 3749	. . . . . . . . . . . . 13 $/\$
34	31, 32, 33	mp2an 426	. . . . . . . . . . . 12
35	11	ad2antlr 489	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
36		simpr 110	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
37	35, 36	ffvelcdmd 5648	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
38	34, 37	sselid 3153	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
39		f1ocnvfv2 5773	. . . . . . . . . . 11 $/\$
40	30, 38, 39	sylancr 414	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
41	40	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
42		fvco3 5583	. . . . . . . . . . . . . 14 $/\$
43	35, 42	sylancom 420	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
44	43	eqeq1d 2186	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
45	44	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
46	45	fveq2d 5515	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
47		0zd 9254	. . . . . . . . . . . 12
48	47, 9	frec2uz0d 10385	. . . . . . . . . . 11
49	48	mptru 1362	. . . . . . . . . 10
50	46, 49	eqtrdi 2226	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
51	41, 50	eqtr3d 2212	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
52	51	exp31 364	. . . . . . 7 $/\$ $\/$ $/\$
53	29, 52	reximdai 2575	. . . . . 6 $/\$ $\/$ $/\$
54	40	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
55	43	adantr 276	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
56		simpr 110	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
57	55, 56	eqtr3d 2212	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
58	57	fveq2d 5515	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
59		df-1o 6411	. . . . . . . . . . . 12
60	59	fveq2i 5514	. . . . . . . . . . 11
61		peano1 4590	. . . . . . . . . . . . . 14
62	61	a1i 9	. . . . . . . . . . . . 13
63	47, 9, 62	frec2uzsucd 10387	. . . . . . . . . . . 12
64	63	mptru 1362	. . . . . . . . . . 11
65	49	oveq1i 5879	. . . . . . . . . . . 12
66		0p1e1 9022	. . . . . . . . . . . 12
67	65, 66	eqtri 2198	. . . . . . . . . . 11
68	60, 64, 67	3eqtri 2202	. . . . . . . . . 10
69	58, 68	eqtrdi 2226	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
70	54, 69	eqtr3d 2212	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
71	70	ex 115	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
72	29, 71	ralimdaa 2543	. . . . . 6 $/\$ $\/$ $/\$
73	53, 72	orim12d 786	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
74	20, 73	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
75	74	ralrimiva 2550	. . 3 $/\$ $\/$ $\/$
76		fveq1 5510	. . . . . . . . 9
77	76	eqeq1d 2186	. . . . . . . 8
78	77	rexbidv 2478	. . . . . . 7
79	76	eqeq1d 2186	. . . . . . . 8
80	79	ralbidv 2477	. . . . . . 7
81	78, 80	orbi12d 793	. . . . . 6 $\/$ $\/$
82		simplr 528	. . . . . 6 $/\$ $\/$ $/\$ $\/$
83	9	2o01f 14402	. . . . . . . 8
84		elmapi 6664	. . . . . . . . 9
85	84	adantl 277	. . . . . . . 8 $/\$ $\/$ $/\$
86		fco2 5378	. . . . . . . 8 $/\$
87	83, 85, 86	sylancr 414	. . . . . . 7 $/\$ $\/$ $/\$
88		prexg 4208	. . . . . . . . . 10 $/\$
89	31, 32, 88	mp2an 426	. . . . . . . . 9
90	89	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
91		simpll 527	. . . . . . . 8 $/\$ $\/$ $/\$
92	90, 91	elmapd 6656	. . . . . . 7 $/\$ $\/$ $/\$
93	87, 92	mpbird 167	. . . . . 6 $/\$ $\/$ $/\$
94	81, 82, 93	rspcdva 2846	. . . . 5 $/\$ $\/$ $/\$ $\/$
95		nfcv 2319	. . . . . . . . . 10
96		nfre1 2520	. . . . . . . . . . 11
97		nfra1 2508	. . . . . . . . . . 11
98	96, 97	nfor 1574	. . . . . . . . . 10 $\/$
99	95, 98	nfralxy 2515	. . . . . . . . 9 $\/$
100	21, 99	nfan 1565	. . . . . . . 8 $/\$ $\/$
101		nfv 1528	. . . . . . . 8
102	100, 101	nfan 1565	. . . . . . 7 $/\$ $\/$ $/\$
103	84	ad2antlr 489	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
104		omelon 4605	. . . . . . . . . . . . . . . 16
105	104	onelssi 4426	. . . . . . . . . . . . . . 15
106	15, 105	ax-mp 5	. . . . . . . . . . . . . 14
107	106	a1i 9	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
108	103, 107	fssd 5374	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
109		simpr 110	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
110	108, 109	ffvelcdmd 5648	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
111		f1ocnvfv1 5772	. . . . . . . . . . 11 $/\$
112	30, 110, 111	sylancr 414	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
113	112	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
114		fvco3 5583	. . . . . . . . . . . . . 14 $/\$
115	103, 114	sylancom 420	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
116	115	eqeq1d 2186	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
117	116	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
118	117	fveq2d 5515	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
119		f1ocnvfv 5774	. . . . . . . . . . . 12 $/\$
120	30, 61, 119	mp2an 426	. . . . . . . . . . 11
121	49, 120	ax-mp 5	. . . . . . . . . 10
122	118, 121	eqtrdi 2226	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
123	113, 122	eqtr3d 2212	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
124	123	exp31 364	. . . . . . 7 $/\$ $\/$ $/\$
125	102, 124	reximdai 2575	. . . . . 6 $/\$ $\/$ $/\$
126	112	adantr 276	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
127	115	eqeq1d 2186	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
128	127	biimpa 296	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
129	128	fveq2d 5515	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
130		1onn 6515	. . . . . . . . . . . 12
131		f1ocnvfv 5774	. . . . . . . . . . . 12 $/\$
132	30, 130, 131	mp2an 426	. . . . . . . . . . 11
133	68, 132	ax-mp 5	. . . . . . . . . 10
134	129, 133	eqtrdi 2226	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
135	126, 134	eqtr3d 2212	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
136	135	ex 115	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
137	102, 136	ralimdaa 2543	. . . . . 6 $/\$ $\/$ $/\$
138	125, 137	orim12d 786	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
139	94, 138	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
140	139	ralrimiva 2550	. . 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 708

wceq 1353

wtru 1354

wcel 2148

wral 2455

wrex 2456

cvv 2737

wss 3129

c0 3422

cpr 3592

cmpt 4061

csuc 4362

com 4586

ccnv 4622

cres 4625

ccom 4627

wf 5208

wf1o 5211

cfv 5212 (class class class)co 5869 freccfrec 6385

c1o 6404

c2o 6405

cmap 6642 Omnicomni 7126

cc0 7802

c1 7803

caddc 7805

cn0 9165

cz 9242

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4115 ax-sep 4118 ax-nul 4126 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-setind 4533 ax-iinf 4584 ax-cnex 7893 ax-resscn 7894 ax-1cn 7895 ax-1re 7896 ax-icn 7897 ax-addcl 7898 ax-addrcl 7899 ax-mulcl 7900 ax-addcom 7902 ax-addass 7904 ax-distr 7906 ax-i2m1 7907 ax-0lt1 7908 ax-0id 7910 ax-rnegex 7911 ax-cnre 7913 ax-pre-ltirr 7914 ax-pre-ltwlin 7915 ax-pre-lttrn 7916 ax-pre-ltadd 7918

This theorem depends on definitions: df-bi 117 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-br 4001 df-opab 4062 df-mpt 4063 df-tr 4099 df-id 4290 df-iord 4363 df-on 4365 df-ilim 4366 df-suc 4368 df-iom 4587 df-xp 4629 df-rel 4630 df-cnv 4631 df-co 4632 df-dm 4633 df-rn 4634 df-res 4635 df-ima 4636 df-iota 5174 df-fun 5214 df-fn 5215 df-f 5216 df-f1 5217 df-fo 5218 df-f1o 5219 df-fv 5220 df-riota 5825 df-ov 5872 df-oprab 5873 df-mpo 5874 df-recs 6300 df-frec 6386 df-1o 6411 df-2o 6412 df-map 6644 df-omni 7127 df-pnf 7984 df-mnf 7985 df-xr 7986 df-ltxr 7987 df-le 7988 df-sub 8120 df-neg 8121 df-inn 8909 df-n0 9166 df-z 9243 df-uz 9518

This theorem is referenced by: isomninn 14435

W3C validator