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 13909

Description: Lemma for isomninn 13910. 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 7101	. 2 Omni $\/$
2		fveq1 5485	. . . . . . . . 9
3	2	eqeq1d 2174	. . . . . . . 8
4	3	rexbidv 2467	. . . . . . 7
5	2	eqeq1d 2174	. . . . . . . 8
6	5	ralbidv 2466	. . . . . . 7
7	4, 6	orbi12d 783	. . . . . 6 $\/$ $\/$
8		simplr 520	. . . . . 6 $/\$ $\/$ $/\$ $\/$
9		isomninnlem.g	. . . . . . . . 9 frec
10	9	012of 13875	. . . . . . . 8
11		elmapi 6636	. . . . . . . . 9
12	11	adantl 275	. . . . . . . 8 $/\$ $\/$ $/\$
13		fco2 5354	. . . . . . . 8 $/\$
14	10, 12, 13	sylancr 411	. . . . . . 7 $/\$ $\/$ $/\$
15		2onn 6489	. . . . . . . . 9
16	15	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
17		simpll 519	. . . . . . . 8 $/\$ $\/$ $/\$
18	16, 17	elmapd 6628	. . . . . . 7 $/\$ $\/$ $/\$
19	14, 18	mpbird 166	. . . . . 6 $/\$ $\/$ $/\$
20	7, 8, 19	rspcdva 2835	. . . . 5 $/\$ $\/$ $/\$ $\/$
21		nfv 1516	. . . . . . . . 9
22		nfcv 2308	. . . . . . . . . 10
23		nfre1 2509	. . . . . . . . . . 11
24		nfra1 2497	. . . . . . . . . . 11
25	23, 24	nfor 1562	. . . . . . . . . 10 $\/$
26	22, 25	nfralxy 2504	. . . . . . . . 9 $\/$
27	21, 26	nfan 1553	. . . . . . . 8 $/\$ $\/$
28		nfv 1516	. . . . . . . 8
29	27, 28	nfan 1553	. . . . . . 7 $/\$ $\/$ $/\$
30	9	frechashgf1o 10363	. . . . . . . . . . 11
31		0nn0 9129	. . . . . . . . . . . . 13
32		1nn0 9130	. . . . . . . . . . . . 13
33		prssi 3731	. . . . . . . . . . . . 13 $/\$
34	31, 32, 33	mp2an 423	. . . . . . . . . . . 12
35	11	ad2antlr 481	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
36		simpr 109	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
37	35, 36	ffvelrnd 5621	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
38	34, 37	sselid 3140	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
39		f1ocnvfv2 5746	. . . . . . . . . . 11 $/\$
40	30, 38, 39	sylancr 411	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
41	40	adantr 274	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
42		fvco3 5557	. . . . . . . . . . . . . 14 $/\$
43	35, 42	sylancom 417	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
44	43	eqeq1d 2174	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
45	44	biimpa 294	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
46	45	fveq2d 5490	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
47		0zd 9203	. . . . . . . . . . . 12
48	47, 9	frec2uz0d 10334	. . . . . . . . . . 11
49	48	mptru 1352	. . . . . . . . . 10
50	46, 49	eqtrdi 2215	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
51	41, 50	eqtr3d 2200	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
52	51	exp31 362	. . . . . . 7 $/\$ $\/$ $/\$
53	29, 52	reximdai 2564	. . . . . 6 $/\$ $\/$ $/\$
54	40	adantr 274	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
55	43	adantr 274	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
56		simpr 109	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
57	55, 56	eqtr3d 2200	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
58	57	fveq2d 5490	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
59		df-1o 6384	. . . . . . . . . . . 12
60	59	fveq2i 5489	. . . . . . . . . . 11
61		peano1 4571	. . . . . . . . . . . . . 14
62	61	a1i 9	. . . . . . . . . . . . 13
63	47, 9, 62	frec2uzsucd 10336	. . . . . . . . . . . 12
64	63	mptru 1352	. . . . . . . . . . 11
65	49	oveq1i 5852	. . . . . . . . . . . 12
66		0p1e1 8971	. . . . . . . . . . . 12
67	65, 66	eqtri 2186	. . . . . . . . . . 11
68	60, 64, 67	3eqtri 2190	. . . . . . . . . 10
69	58, 68	eqtrdi 2215	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
70	54, 69	eqtr3d 2200	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
71	70	ex 114	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
72	29, 71	ralimdaa 2532	. . . . . 6 $/\$ $\/$ $/\$
73	53, 72	orim12d 776	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
74	20, 73	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
75	74	ralrimiva 2539	. . 3 $/\$ $\/$ $\/$
76		fveq1 5485	. . . . . . . . 9
77	76	eqeq1d 2174	. . . . . . . 8
78	77	rexbidv 2467	. . . . . . 7
79	76	eqeq1d 2174	. . . . . . . 8
80	79	ralbidv 2466	. . . . . . 7
81	78, 80	orbi12d 783	. . . . . 6 $\/$ $\/$
82		simplr 520	. . . . . 6 $/\$ $\/$ $/\$ $\/$
83	9	2o01f 13876	. . . . . . . 8
84		elmapi 6636	. . . . . . . . 9
85	84	adantl 275	. . . . . . . 8 $/\$ $\/$ $/\$
86		fco2 5354	. . . . . . . 8 $/\$
87	83, 85, 86	sylancr 411	. . . . . . 7 $/\$ $\/$ $/\$
88		prexg 4189	. . . . . . . . . 10 $/\$
89	31, 32, 88	mp2an 423	. . . . . . . . 9
90	89	a1i 9	. . . . . . . 8 $/\$ $\/$ $/\$
91		simpll 519	. . . . . . . 8 $/\$ $\/$ $/\$
92	90, 91	elmapd 6628	. . . . . . 7 $/\$ $\/$ $/\$
93	87, 92	mpbird 166	. . . . . 6 $/\$ $\/$ $/\$
94	81, 82, 93	rspcdva 2835	. . . . 5 $/\$ $\/$ $/\$ $\/$
95		nfcv 2308	. . . . . . . . . 10
96		nfre1 2509	. . . . . . . . . . 11
97		nfra1 2497	. . . . . . . . . . 11
98	96, 97	nfor 1562	. . . . . . . . . 10 $\/$
99	95, 98	nfralxy 2504	. . . . . . . . 9 $\/$
100	21, 99	nfan 1553	. . . . . . . 8 $/\$ $\/$
101		nfv 1516	. . . . . . . 8
102	100, 101	nfan 1553	. . . . . . 7 $/\$ $\/$ $/\$
103	84	ad2antlr 481	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
104		omelon 4586	. . . . . . . . . . . . . . . 16
105	104	onelssi 4407	. . . . . . . . . . . . . . 15
106	15, 105	ax-mp 5	. . . . . . . . . . . . . 14
107	106	a1i 9	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
108	103, 107	fssd 5350	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
109		simpr 109	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
110	108, 109	ffvelrnd 5621	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
111		f1ocnvfv1 5745	. . . . . . . . . . 11 $/\$
112	30, 110, 111	sylancr 411	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
113	112	adantr 274	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
114		fvco3 5557	. . . . . . . . . . . . . 14 $/\$
115	103, 114	sylancom 417	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
116	115	eqeq1d 2174	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
117	116	biimpa 294	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
118	117	fveq2d 5490	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
119		f1ocnvfv 5747	. . . . . . . . . . . 12 $/\$
120	30, 61, 119	mp2an 423	. . . . . . . . . . 11
121	49, 120	ax-mp 5	. . . . . . . . . 10
122	118, 121	eqtrdi 2215	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
123	113, 122	eqtr3d 2200	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
124	123	exp31 362	. . . . . . 7 $/\$ $\/$ $/\$
125	102, 124	reximdai 2564	. . . . . 6 $/\$ $\/$ $/\$
126	112	adantr 274	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
127	115	eqeq1d 2174	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
128	127	biimpa 294	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
129	128	fveq2d 5490	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
130		1onn 6488	. . . . . . . . . . . 12
131		f1ocnvfv 5747	. . . . . . . . . . . 12 $/\$
132	30, 130, 131	mp2an 423	. . . . . . . . . . 11
133	68, 132	ax-mp 5	. . . . . . . . . 10
134	129, 133	eqtrdi 2215	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
135	126, 134	eqtr3d 2200	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
136	135	ex 114	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
137	102, 136	ralimdaa 2532	. . . . . 6 $/\$ $\/$ $/\$
138	125, 137	orim12d 776	. . . . 5 $/\$ $\/$ $/\$ $\/$ $\/$
139	94, 138	mpd 13	. . . 4 $/\$ $\/$ $/\$ $\/$
140	139	ralrimiva 2539	. . 3 $/\$ $\/$ $\/$
141	75, 140	impbida 586	. 2 $\/$ $\/$
142	1, 141	bitrd 187	1 Omni $\/$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 698

wceq 1343

wtru 1344

wcel 2136

wral 2444

wrex 2445

cvv 2726

wss 3116

c0 3409

cpr 3577

cmpt 4043

csuc 4343

com 4567

ccnv 4603

cres 4606

ccom 4608

wf 5184

wf1o 5187

cfv 5188 (class class class)co 5842 freccfrec 6358

c1o 6377

c2o 6378

cmap 6614 Omnicomni 7098

cc0 7753

c1 7754

caddc 7756

cn0 9114

cz 9191

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 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-addcom 7853 ax-addass 7855 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-0id 7861 ax-rnegex 7862 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-ltadd 7869

This theorem depends on definitions: df-bi 116 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-recs 6273 df-frec 6359 df-1o 6384 df-2o 6385 df-map 6616 df-omni 7099 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-inn 8858 df-n0 9115 df-z 9192 df-uz 9467

This theorem is referenced by: isomninn 13910

W3C validator