fin23lem27 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fin23lem27		Structured version Unicode version

Theorem fin23lem27 8707

Description: The mapping constructed in fin23lem22 8706 is in fact an isomorphism. (Contributed by Stefan O'Rear, 2-Nov-2014.)

**Hypothesis**
Ref	Expression
fin23lem22.b

**Assertion**
Ref	Expression
fin23lem27	$/\$

Distinct variable group:

Allowed substitution hints:

(

)

Proof of Theorem fin23lem27 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ordom 6688	. . . 4
2		ordwe 4891	. . . 4
3		weso 4870	. . . 4
4	1, 2, 3	mp2b 10	. . 3
5	4	a1i 11	. 2 $/\$
6		sopo 4817	. . . . 5
7	4, 6	ax-mp 5	. . . 4
8		poss 4802	. . . 4
9	7, 8	mpi 17	. . 3
10	9	adantr 465	. 2 $/\$
11		fin23lem22.b	. . . 4
12	11	fin23lem22 8706	. . 3 $/\$
13		f1ofo 5822	. . 3
14	12, 13	syl 16	. 2 $/\$
15		nnsdomel 8370	. . . . . . . 8 $/\$
16	15	adantl 466	. . . . . . 7 $/\$ $/\$ $/\$
17	16	biimpd 207	. . . . . 6 $/\$ $/\$ $/\$
18		fin23lem23 8705	. . . . . . . . . . . . 13 $/\$ $/\$
19	18	adantrr 716	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
20		ineq1 3693	. . . . . . . . . . . . . 14
21	20	breq1d 4457	. . . . . . . . . . . . 13
22	21	cbvreuv 3090	. . . . . . . . . . . 12
23	19, 22	sylib 196	. . . . . . . . . . 11 $/\$ $/\$ $/\$
24		nfv 1683	. . . . . . . . . . . 12
25	21	cbvriotav 6255	. . . . . . . . . . . 12
26		ineq1 3693	. . . . . . . . . . . . 13
27	26	breq1d 4457	. . . . . . . . . . . 12
28	24, 25, 27	riotaprop 6268	. . . . . . . . . . 11 $/\$
29	23, 28	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
30	29	simprd 463	. . . . . . . . 9 $/\$ $/\$ $/\$
31	30	adantrr 716	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
32		simprr 756	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
33		fin23lem23 8705	. . . . . . . . . . . . . . 15 $/\$ $/\$
34	33	adantrl 715	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
35	20	breq1d 4457	. . . . . . . . . . . . . . 15
36	35	cbvreuv 3090	. . . . . . . . . . . . . 14
37	34, 36	sylib 196	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
38		nfv 1683	. . . . . . . . . . . . . 14
39	35	cbvriotav 6255	. . . . . . . . . . . . . 14
40		ineq1 3693	. . . . . . . . . . . . . . 15
41	40	breq1d 4457	. . . . . . . . . . . . . 14
42	38, 39, 41	riotaprop 6268	. . . . . . . . . . . . 13 $/\$
43	37, 42	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
44	43	simprd 463	. . . . . . . . . . 11 $/\$ $/\$ $/\$
45	44	ensymd 7566	. . . . . . . . . 10 $/\$ $/\$ $/\$
46	45	adantrr 716	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
47		sdomentr 7651	. . . . . . . . 9 $/\$
48	32, 46, 47	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
49		ensdomtr 7653	. . . . . . . 8 $/\$
50	31, 48, 49	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
51	50	expr 615	. . . . . 6 $/\$ $/\$ $/\$
52		simpll 753	. . . . . . . . 9 $/\$ $/\$ $/\$
53		omsson 6683	. . . . . . . . 9
54	52, 53	syl6ss 3516	. . . . . . . 8 $/\$ $/\$ $/\$
55	29	simpld 459	. . . . . . . 8 $/\$ $/\$ $/\$
56	54, 55	sseldd 3505	. . . . . . 7 $/\$ $/\$ $/\$
57	43	simpld 459	. . . . . . . 8 $/\$ $/\$ $/\$
58	54, 57	sseldd 3505	. . . . . . 7 $/\$ $/\$ $/\$
59		onsdominel 7666	. . . . . . . 8 $/\$ $/\$
60	59	3expia 1198	. . . . . . 7 $/\$
61	56, 58, 60	syl2anc 661	. . . . . 6 $/\$ $/\$ $/\$
62	17, 51, 61	3syld 55	. . . . 5 $/\$ $/\$ $/\$
63		simprl 755	. . . . . . 7 $/\$ $/\$ $/\$
64		breq2 4451	. . . . . . . . 9
65	64	riotabidv 6246	. . . . . . . 8
66	65, 11	fvmptg 5947	. . . . . . 7 $/\$
67	63, 55, 66	syl2anc 661	. . . . . 6 $/\$ $/\$ $/\$
68		simprr 756	. . . . . . 7 $/\$ $/\$ $/\$
69		breq2 4451	. . . . . . . . 9
70	69	riotabidv 6246	. . . . . . . 8
71	70, 11	fvmptg 5947	. . . . . . 7 $/\$
72	68, 57, 71	syl2anc 661	. . . . . 6 $/\$ $/\$ $/\$
73	67, 72	eleq12d 2549	. . . . 5 $/\$ $/\$ $/\$
74	62, 73	sylibrd 234	. . . 4 $/\$ $/\$ $/\$
75		epel 4794	. . . 4
76		fvex 5875	. . . . 5
77	76	epelc 4793	. . . 4
78	74, 75, 77	3imtr4g 270	. . 3 $/\$ $/\$ $/\$
79	78	ralrimivva 2885	. 2 $/\$
80		soisoi 6211	. 2 $/\$ $/\$ $/\$
81	5, 10, 14, 79, 80	syl22anc 1229	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1379

wcel 1767

wral 2814

wreu 2816

cin 3475

wss 3476 class class class wbr 4447

cmpt 4505

cep 4789

wpo 4798

wor 4799

wwe 4837

word 4877

con0 4878

wfo 5585

wf1o 5586

cfv 5587

wiso 5588

crio 6243

com 6679

cen 7513

csdm 7515

cfn 7516

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6575

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5550 df-fun 5589 df-fn 5590 df-f 5591 df-f1 5592 df-fo 5593 df-f1o 5594 df-fv 5595 df-isom 5596 df-riota 6244 df-om 6680 df-recs 7042 df-1o 7130 df-er 7311 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-card 8319

This theorem is referenced by: (None)

W3C validator