fin23lem27 - Metamath Proof Explorer

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

Theorem fin23lem27 8758

Description: The mapping constructed in fin23lem22 8757 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 6701	. . . 4
2		ordwe 5436	. . . 4
3		weso 4825	. . . 4
4	1, 2, 3	mp2b 10	. . 3
5	4	a1i 11	. 2 $/\$
6		sopo 4772	. . . . 5
7	4, 6	ax-mp 5	. . . 4
8		poss 4757	. . . 4
9	7, 8	mpi 20	. . 3
10	9	adantr 467	. 2 $/\$
11		fin23lem22.b	. . . 4
12	11	fin23lem22 8757	. . 3 $/\$
13		f1ofo 5821	. . 3
14	12, 13	syl 17	. 2 $/\$
15		nnsdomel 8424	. . . . . . . 8 $/\$
16	15	adantl 468	. . . . . . 7 $/\$ $/\$ $/\$
17	16	biimpd 211	. . . . . 6 $/\$ $/\$ $/\$
18		fin23lem23 8756	. . . . . . . . . . . . 13 $/\$ $/\$
19	18	adantrr 723	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
20		ineq1 3627	. . . . . . . . . . . . . 14
21	20	breq1d 4412	. . . . . . . . . . . . 13
22	21	cbvreuv 3021	. . . . . . . . . . . 12
23	19, 22	sylib 200	. . . . . . . . . . 11 $/\$ $/\$ $/\$
24		nfv 1761	. . . . . . . . . . . 12
25	21	cbvriotav 6263	. . . . . . . . . . . 12
26		ineq1 3627	. . . . . . . . . . . . 13
27	26	breq1d 4412	. . . . . . . . . . . 12
28	24, 25, 27	riotaprop 6275	. . . . . . . . . . 11 $/\$
29	23, 28	syl 17	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
30	29	simprd 465	. . . . . . . . 9 $/\$ $/\$ $/\$
31	30	adantrr 723	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
32		simprr 766	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
33		fin23lem23 8756	. . . . . . . . . . . . . . 15 $/\$ $/\$
34	33	adantrl 722	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
35	20	breq1d 4412	. . . . . . . . . . . . . . 15
36	35	cbvreuv 3021	. . . . . . . . . . . . . 14
37	34, 36	sylib 200	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
38		nfv 1761	. . . . . . . . . . . . . 14
39	35	cbvriotav 6263	. . . . . . . . . . . . . 14
40		ineq1 3627	. . . . . . . . . . . . . . 15
41	40	breq1d 4412	. . . . . . . . . . . . . 14
42	38, 39, 41	riotaprop 6275	. . . . . . . . . . . . 13 $/\$
43	37, 42	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
44	43	simprd 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$
45	44	ensymd 7620	. . . . . . . . . 10 $/\$ $/\$ $/\$
46	45	adantrr 723	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
47		sdomentr 7706	. . . . . . . . 9 $/\$
48	32, 46, 47	syl2anc 667	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
49		ensdomtr 7708	. . . . . . . 8 $/\$
50	31, 48, 49	syl2anc 667	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
51	50	expr 620	. . . . . 6 $/\$ $/\$ $/\$
52		simpll 760	. . . . . . . . 9 $/\$ $/\$ $/\$
53		omsson 6696	. . . . . . . . 9
54	52, 53	syl6ss 3444	. . . . . . . 8 $/\$ $/\$ $/\$
55	29	simpld 461	. . . . . . . 8 $/\$ $/\$ $/\$
56	54, 55	sseldd 3433	. . . . . . 7 $/\$ $/\$ $/\$
57	43	simpld 461	. . . . . . . 8 $/\$ $/\$ $/\$
58	54, 57	sseldd 3433	. . . . . . 7 $/\$ $/\$ $/\$
59		onsdominel 7721	. . . . . . . 8 $/\$ $/\$
60	59	3expia 1210	. . . . . . 7 $/\$
61	56, 58, 60	syl2anc 667	. . . . . 6 $/\$ $/\$ $/\$
62	17, 51, 61	3syld 57	. . . . 5 $/\$ $/\$ $/\$
63		simprl 764	. . . . . . 7 $/\$ $/\$ $/\$
64		breq2 4406	. . . . . . . . 9
65	64	riotabidv 6254	. . . . . . . 8
66	65, 11	fvmptg 5946	. . . . . . 7 $/\$
67	63, 55, 66	syl2anc 667	. . . . . 6 $/\$ $/\$ $/\$
68		simprr 766	. . . . . . 7 $/\$ $/\$ $/\$
69		breq2 4406	. . . . . . . . 9
70	69	riotabidv 6254	. . . . . . . 8
71	70, 11	fvmptg 5946	. . . . . . 7 $/\$
72	68, 57, 71	syl2anc 667	. . . . . 6 $/\$ $/\$ $/\$
73	67, 72	eleq12d 2523	. . . . 5 $/\$ $/\$ $/\$
74	62, 73	sylibrd 238	. . . 4 $/\$ $/\$ $/\$
75		epel 4748	. . . 4
76		fvex 5875	. . . . 5
77	76	epelc 4747	. . . 4
78	74, 75, 77	3imtr4g 274	. . 3 $/\$ $/\$ $/\$
79	78	ralrimivva 2809	. 2 $/\$
80		soisoi 6219	. 2 $/\$ $/\$ $/\$
81	5, 10, 14, 79, 80	syl22anc 1269	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371

wceq 1444

wcel 1887

wral 2737

wreu 2739

cin 3403

wss 3404 class class class wbr 4402

cmpt 4461

cep 4743

wpo 4753

wor 4754

wwe 4792

word 5422

con0 5423

wfo 5580

wf1o 5581

cfv 5582

wiso 5583

crio 6251

com 6692

cen 7566

csdm 7568

cfn 7569

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-om 6693 df-wrecs 7028 df-recs 7090 df-1o 7182 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-card 8373

This theorem is referenced by: (None)

W3C validator