infpssrlem4 - Metamath Proof Explorer

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

Theorem infpssrlem4 8736

Description: Lemma for infpssr 8738. (Contributed by Stefan O'Rear, 30-Oct-2014.)

**Hypotheses**
Ref	Expression
infpssrlem.a
infpssrlem.c
infpssrlem.d	$\$
infpssrlem.e

**Assertion**
Ref	Expression
infpssrlem4	$/\$ $/\$

Proof of Theorem infpssrlem4 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5877	. . . . . . . 8
2	1	neeq1d 2701	. . . . . . 7
3	2	raleqbi1dv 3033	. . . . . 6
4	3	imbi2d 317	. . . . 5
5		fveq2 5877	. . . . . . . 8
6	5	neeq1d 2701	. . . . . . 7
7	6	raleqbi1dv 3033	. . . . . 6
8	7	imbi2d 317	. . . . 5
9		fveq2 5877	. . . . . . . 8
10	9	neeq1d 2701	. . . . . . 7
11	10	raleqbi1dv 3033	. . . . . 6
12	11	imbi2d 317	. . . . 5
13		fveq2 5877	. . . . . . . 8
14	13	neeq1d 2701	. . . . . . 7
15	14	raleqbi1dv 3033	. . . . . 6
16	15	imbi2d 317	. . . . 5
17		ral0 3902	. . . . . 6
18	17	a1i 11	. . . . 5
19		infpssrlem.c	. . . . . . . . . . . . . . . . . 18
20		f1ocnv 5839	. . . . . . . . . . . . . . . . . 18
21		f1of 5827	. . . . . . . . . . . . . . . . . 18
22	19, 20, 21	3syl 18	. . . . . . . . . . . . . . . . 17
23	22	adantl 467	. . . . . . . . . . . . . . . 16 $/\$
24		infpssrlem.a	. . . . . . . . . . . . . . . . . . 19
25		infpssrlem.d	. . . . . . . . . . . . . . . . . . 19 $\$
26		infpssrlem.e	. . . . . . . . . . . . . . . . . . 19
27	24, 19, 25, 26	infpssrlem3 8735	. . . . . . . . . . . . . . . . . 18
28	27	ffvelrnda 6033	. . . . . . . . . . . . . . . . 17 $/\$
29	28	ancoms 454	. . . . . . . . . . . . . . . 16 $/\$
30	23, 29	ffvelrnd 6034	. . . . . . . . . . . . . . 15 $/\$
31	25	eldifbd 3449	. . . . . . . . . . . . . . . 16
32	31	adantl 467	. . . . . . . . . . . . . . 15 $/\$
33		nelne2 2754	. . . . . . . . . . . . . . 15 $/\$
34	30, 32, 33	syl2anc 665	. . . . . . . . . . . . . 14 $/\$
35	24, 19, 25, 26	infpssrlem2 8734	. . . . . . . . . . . . . . 15
36	35	adantr 466	. . . . . . . . . . . . . 14 $/\$
37	24, 19, 25, 26	infpssrlem1 8733	. . . . . . . . . . . . . . 15
38	37	adantl 467	. . . . . . . . . . . . . 14 $/\$
39	34, 36, 38	3netr4d 2729	. . . . . . . . . . . . 13 $/\$
40	39	3adant3 1025	. . . . . . . . . . . 12 $/\$ $/\$
41	1	neeq2d 2702	. . . . . . . . . . . 12
42	40, 41	syl5ibr 224	. . . . . . . . . . 11 $/\$ $/\$
43	42	adantrd 469	. . . . . . . . . 10 $/\$ $/\$ $/\$
44		simpr 462	. . . . . . . . . . . . . . . 16 $/\$
45		peano2 6723	. . . . . . . . . . . . . . . . 17
46	45	adantr 466	. . . . . . . . . . . . . . . 16 $/\$
47		elnn 6712	. . . . . . . . . . . . . . . 16 $/\$
48	44, 46, 47	syl2anc 665	. . . . . . . . . . . . . . 15 $/\$
49	48	3ad2antl1 1167	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
50	49	adantl 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
51		simpl 458	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
52		nnsuc 6719	. . . . . . . . . . . . 13 $/\$
53	50, 51, 52	syl2anc 665	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
54		nfv 1751	. . . . . . . . . . . . . . . 16
55		nfv 1751	. . . . . . . . . . . . . . . 16
56		nfra1 2806	. . . . . . . . . . . . . . . 16
57	54, 55, 56	nf3an 1986	. . . . . . . . . . . . . . 15 $/\$ $/\$
58		nfv 1751	. . . . . . . . . . . . . . 15
59	57, 58	nfan 1984	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
60		nfv 1751	. . . . . . . . . . . . . 14
61		simpl3 1010	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
62		simpr 462	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
63		nnord 6710	. . . . . . . . . . . . . . . . . . . . . . . 24
64	63	adantr 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
65		ordsucelsuc 6659	. . . . . . . . . . . . . . . . . . . . . . 23
66	64, 65	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
67	62, 66	mpbird 235	. . . . . . . . . . . . . . . . . . . . 21 $/\$
68	67	3ad2antl1 1167	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
69	68	adantrr 721	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
70		rsp 2791	. . . . . . . . . . . . . . . . . . 19
71	61, 69, 70	sylc 62	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
72		f1of1 5826	. . . . . . . . . . . . . . . . . . . . . . . . . 26
73	19, 20, 72	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25
74	73	ad2antlr 731	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
75	29	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
76	27	ffvelrnda 6033	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
77	76	adantll 718	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
78		f1fveq 6174	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
79	74, 75, 77, 78	syl12anc 1262	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
80	79	necon3bid 2682	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
81	80	biimprd 226	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
82	35	adantr 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
83	24, 19, 25, 26	infpssrlem2 8734	. . . . . . . . . . . . . . . . . . . . . . . 24
84	83	adantl 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
85	82, 84	neeq12d 2703	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
86	85	adantlr 719	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
87	81, 86	sylibrd 237	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
88	87	adantrl 720	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
89	88	3adantl3 1163	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
90	71, 89	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
91	90	expr 618	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
92		eleq1 2494	. . . . . . . . . . . . . . . . . 18
93	92	anbi2d 708	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94		fveq2 5877	. . . . . . . . . . . . . . . . . . 19
95	94	neeq2d 2702	. . . . . . . . . . . . . . . . . 18
96	95	imbi2d 317	. . . . . . . . . . . . . . . . 17
97	93, 96	imbi12d 321	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	91, 97	mpbiri 236	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
99	98	com3l 84	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
100	59, 60, 99	rexlimd 2909	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
101	100	adantl 467	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
102	53, 101	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
103	102	ex 435	. . . . . . . . . 10 $/\$ $/\$ $/\$
104	43, 103	pm2.61ine 2737	. . . . . . . . 9 $/\$ $/\$ $/\$
105	104	ralrimiva 2839	. . . . . . . 8 $/\$ $/\$
106		fveq2 5877	. . . . . . . . . 10
107	106	neeq2d 2702	. . . . . . . . 9
108	107	cbvralv 3055	. . . . . . . 8
109	105, 108	sylib 199	. . . . . . 7 $/\$ $/\$
110	109	3exp 1204	. . . . . 6
111	110	a2d 29	. . . . 5
112	4, 8, 12, 16, 18, 111	finds 6729	. . . 4
113	112	impcom 431	. . 3 $/\$
114		fveq2 5877	. . . . 5
115	114	neeq2d 2702	. . . 4
116	115	rspccv 3179	. . 3
117	113, 116	syl 17	. 2 $/\$
118	117	3impia 1202	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1868

wne 2618

wral 2775

wrex 2776 $\$ cdif 3433

wss 3436

c0 3761

ccnv 4848

cres 4851

word 5437

csuc 5440

wf 5593

wf1 5594

wf1o 5596

cfv 5597

com 6702

crdg 7131

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-sep 4543 ax-nul 4551 ax-pow 4598 ax-pr 4656 ax-un 6593

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-ral 2780 df-rex 2781 df-reu 2782 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-uni 4217 df-iun 4298 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4760 df-id 4764 df-po 4770 df-so 4771 df-fr 4808 df-we 4810 df-xp 4855 df-rel 4856 df-cnv 4857 df-co 4858 df-dm 4859 df-rn 4860 df-res 4861 df-ima 4862 df-pred 5395 df-ord 5441 df-on 5442 df-lim 5443 df-suc 5444 df-iota 5561 df-fun 5599 df-fn 5600 df-f 5601 df-f1 5602 df-fo 5603 df-f1o 5604 df-fv 5605 df-om 6703 df-wrecs 7032 df-recs 7094 df-rdg 7132

This theorem is referenced by: infpssrlem5 8737

W3C validator