fin23lem27 - Metamath Proof Explorer

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

Theorem fin23lem27 8699

Description: The mapping constructed in fin23lem22 8698 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 6682	. . . 4
2		ordwe 4880	. . . 4
3		weso 4859	. . . 4
4	1, 2, 3	mp2b 10	. . 3
5	4	a1i 11	. 2 $/\$
6		sopo 4806	. . . . 5
7	4, 6	ax-mp 5	. . . 4
8		poss 4791	. . . 4
9	7, 8	mpi 17	. . 3
10	9	adantr 463	. 2 $/\$
11		fin23lem22.b	. . . 4
12	11	fin23lem22 8698	. . 3 $/\$
13		f1ofo 5805	. . 3
14	12, 13	syl 16	. 2 $/\$
15		nnsdomel 8362	. . . . . . . 8 $/\$
16	15	adantl 464	. . . . . . 7 $/\$ $/\$ $/\$
17	16	biimpd 207	. . . . . 6 $/\$ $/\$ $/\$
18		fin23lem23 8697	. . . . . . . . . . . . 13 $/\$ $/\$
19	18	adantrr 714	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
20		ineq1 3679	. . . . . . . . . . . . . 14
21	20	breq1d 4449	. . . . . . . . . . . . 13
22	21	cbvreuv 3083	. . . . . . . . . . . 12
23	19, 22	sylib 196	. . . . . . . . . . 11 $/\$ $/\$ $/\$
24		nfv 1712	. . . . . . . . . . . 12
25	21	cbvriotav 6243	. . . . . . . . . . . 12
26		ineq1 3679	. . . . . . . . . . . . 13
27	26	breq1d 4449	. . . . . . . . . . . 12
28	24, 25, 27	riotaprop 6255	. . . . . . . . . . 11 $/\$
29	23, 28	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
30	29	simprd 461	. . . . . . . . 9 $/\$ $/\$ $/\$
31	30	adantrr 714	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
32		simprr 755	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
33		fin23lem23 8697	. . . . . . . . . . . . . . 15 $/\$ $/\$
34	33	adantrl 713	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
35	20	breq1d 4449	. . . . . . . . . . . . . . 15
36	35	cbvreuv 3083	. . . . . . . . . . . . . 14
37	34, 36	sylib 196	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
38		nfv 1712	. . . . . . . . . . . . . 14
39	35	cbvriotav 6243	. . . . . . . . . . . . . 14
40		ineq1 3679	. . . . . . . . . . . . . . 15
41	40	breq1d 4449	. . . . . . . . . . . . . 14
42	38, 39, 41	riotaprop 6255	. . . . . . . . . . . . 13 $/\$
43	37, 42	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
44	43	simprd 461	. . . . . . . . . . 11 $/\$ $/\$ $/\$
45	44	ensymd 7559	. . . . . . . . . 10 $/\$ $/\$ $/\$
46	45	adantrr 714	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
47		sdomentr 7644	. . . . . . . . 9 $/\$
48	32, 46, 47	syl2anc 659	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
49		ensdomtr 7646	. . . . . . . 8 $/\$
50	31, 48, 49	syl2anc 659	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
51	50	expr 613	. . . . . 6 $/\$ $/\$ $/\$
52		simpll 751	. . . . . . . . 9 $/\$ $/\$ $/\$
53		omsson 6677	. . . . . . . . 9
54	52, 53	syl6ss 3501	. . . . . . . 8 $/\$ $/\$ $/\$
55	29	simpld 457	. . . . . . . 8 $/\$ $/\$ $/\$
56	54, 55	sseldd 3490	. . . . . . 7 $/\$ $/\$ $/\$
57	43	simpld 457	. . . . . . . 8 $/\$ $/\$ $/\$
58	54, 57	sseldd 3490	. . . . . . 7 $/\$ $/\$ $/\$
59		onsdominel 7659	. . . . . . . 8 $/\$ $/\$
60	59	3expia 1196	. . . . . . 7 $/\$
61	56, 58, 60	syl2anc 659	. . . . . 6 $/\$ $/\$ $/\$
62	17, 51, 61	3syld 55	. . . . 5 $/\$ $/\$ $/\$
63		simprl 754	. . . . . . 7 $/\$ $/\$ $/\$
64		breq2 4443	. . . . . . . . 9
65	64	riotabidv 6234	. . . . . . . 8
66	65, 11	fvmptg 5929	. . . . . . 7 $/\$
67	63, 55, 66	syl2anc 659	. . . . . 6 $/\$ $/\$ $/\$
68		simprr 755	. . . . . . 7 $/\$ $/\$ $/\$
69		breq2 4443	. . . . . . . . 9
70	69	riotabidv 6234	. . . . . . . 8
71	70, 11	fvmptg 5929	. . . . . . 7 $/\$
72	68, 57, 71	syl2anc 659	. . . . . 6 $/\$ $/\$ $/\$
73	67, 72	eleq12d 2536	. . . . 5 $/\$ $/\$ $/\$
74	62, 73	sylibrd 234	. . . 4 $/\$ $/\$ $/\$
75		epel 4783	. . . 4
76		fvex 5858	. . . . 5
77	76	epelc 4782	. . . 4
78	74, 75, 77	3imtr4g 270	. . 3 $/\$ $/\$ $/\$
79	78	ralrimivva 2875	. 2 $/\$
80		soisoi 6199	. 2 $/\$ $/\$ $/\$
81	5, 10, 14, 79, 80	syl22anc 1227	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367

wceq 1398

wcel 1823

wral 2804

wreu 2806

cin 3460

wss 3461 class class class wbr 4439

cmpt 4497

cep 4778

wpo 4787

wor 4788

wwe 4826

word 4866

con0 4867

wfo 5568

wf1o 5569

cfv 5570

wiso 5571

crio 6231

com 6673

cen 7506

csdm 7508

cfn 7509

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-int 4272 df-iun 4317 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-se 4828 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-isom 5579 df-riota 6232 df-om 6674 df-recs 7034 df-1o 7122 df-er 7303 df-en 7510 df-dom 7511 df-sdom 7512 df-fin 7513 df-card 8311

This theorem is referenced by: (None)

W3C validator