Theorem fnwelem 6915

Description: Lemma for fnwe 6916. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.)

Hypotheses

Ref	Expression
fnwe.1
fnwe.2
fnwe.3
fnwe.4
fnwe.5
fnwelem.6
fnwelem.7

Assertion

Ref	Expression
fnwelem

Distinct variable groups:   ,,,,,,   ,,,,,,   ,,,   ,,,   ,,,,,,   ,Q,,   ,,,,,   ,S,,,,   ,

Proof of Theorem fnwelem

Step	Hyp	Ref	Expression
1		fnwe.2	. . . 4
2		ffvelrn 6029	. . . . . 6
3		simpr 461	. . . . . 6
4		opelxp 5034	. . . . . 6
5	2, 3, 4	sylanbrc 664	. . . . 5
6		fnwelem.7	. . . . 5
7	5, 6	fmptd 6055	. . . 4
8		frn 5742	. . . 4
9	1, 7, 8	3syl 20	. . 3
10		fnwe.3	. . . 4
11		fnwe.4	. . . 4
12		fnwelem.6	. . . . 5
13	12	wexp 6914	. . . 4
14	10, 11, 13	syl2anc 661	. . 3
15		wess 4871	. . 3
16	9, 14, 15	sylc 60	. 2
17		fveq2 5871	. . . . . . . . . . . . 13
18		id 22	. . . . . . . . . . . . 13
19	17, 18	opeq12d 4225	. . . . . . . . . . . 12
20		opex 4716	. . . . . . . . . . . 12
21	19, 6, 20	fvmpt 5956	. . . . . . . . . . 11
22		fveq2 5871	. . . . . . . . . . . . 13
23		id 22	. . . . . . . . . . . . 13
24	22, 23	opeq12d 4225	. . . . . . . . . . . 12
25		opex 4716	. . . . . . . . . . . 12
26	24, 6, 25	fvmpt 5956	. . . . . . . . . . 11
27	21, 26	eqeqan12d 2480	. . . . . . . . . 10
28		fvex 5881	. . . . . . . . . . . 12
29		vex 3112	. . . . . . . . . . . 12
30	28, 29	opth 4726	. . . . . . . . . . 11
31	30	simprbi 464	. . . . . . . . . 10
32	27, 31	syl6bi 228	. . . . . . . . 9
33	32	rgen2a 2884	. . . . . . . 8
34	33	a1i 11	. . . . . . 7
35		dff13 6166	. . . . . . 7
36	7, 34, 35	sylanbrc 664	. . . . . 6
37		f1f1orn 5832	. . . . . 6
38		f1ocnv 5833	. . . . . 6
39	1, 36, 37, 38	4syl 21	. . . . 5
40		eqid 2457	. . . . . . 7
41	40	f1oiso2 6248	. . . . . 6
42		fnwe.1	. . . . . . . 8
43		frel 5739	. . . . . . . . . . . . . . . 16
44		dfrel2 5462	. . . . . . . . . . . . . . . 16
45	43, 44	sylib 196	. . . . . . . . . . . . . . 15
46	45	fveq1d 5873	. . . . . . . . . . . . . 14
47	45	fveq1d 5873	. . . . . . . . . . . . . 14
48	46, 47	breq12d 4465	. . . . . . . . . . . . 13
49	7, 48	syl 16	. . . . . . . . . . . 12
50	49	adantr 465	. . . . . . . . . . 11
51	21, 26	breqan12d 4467	. . . . . . . . . . . 12
52	51	adantl 466	. . . . . . . . . . 11
53		ffvelrn 6029	. . . . . . . . . . . . . . 15
54		simpr 461	. . . . . . . . . . . . . . 15
55	53, 54	jca 532	. . . . . . . . . . . . . 14
56		ffvelrn 6029	. . . . . . . . . . . . . . 15
57		simpr 461	. . . . . . . . . . . . . . 15
58	56, 57	jca 532	. . . . . . . . . . . . . 14
59	55, 58	anim12dan 837	. . . . . . . . . . . . 13
60	59	biantrurd 508	. . . . . . . . . . . 12
61		eleq1 2529	. . . . . . . . . . . . . . . 16
62		opelxp 5034	. . . . . . . . . . . . . . . 16
63	61, 62	syl6bb 261	. . . . . . . . . . . . . . 15
64	63	anbi1d 704	. . . . . . . . . . . . . 14
65	28, 29	op1std 6810	. . . . . . . . . . . . . . . 16
66	65	breq1d 4462	. . . . . . . . . . . . . . 15
67	65	eqeq1d 2459	. . . . . . . . . . . . . . . 16
68	28, 29	op2ndd 6811	. . . . . . . . . . . . . . . . 17
69	68	breq1d 4462	. . . . . . . . . . . . . . . 16
70	67, 69	anbi12d 710	. . . . . . . . . . . . . . 15
71	66, 70	orbi12d 709	. . . . . . . . . . . . . 14
72	64, 71	anbi12d 710	. . . . . . . . . . . . 13
73		eleq1 2529	. . . . . . . . . . . . . . . 16
74		opelxp 5034	. . . . . . . . . . . . . . . 16
75	73, 74	syl6bb 261	. . . . . . . . . . . . . . 15
76	75	anbi2d 703	. . . . . . . . . . . . . 14
77		fvex 5881	. . . . . . . . . . . . . . . . 17
78		vex 3112	. . . . . . . . . . . . . . . . 17
79	77, 78	op1std 6810	. . . . . . . . . . . . . . . 16
80	79	breq2d 4464	. . . . . . . . . . . . . . 15
81	79	eqeq2d 2471	. . . . . . . . . . . . . . . 16
82	77, 78	op2ndd 6811	. . . . . . . . . . . . . . . . 17
83	82	breq2d 4464	. . . . . . . . . . . . . . . 16
84	81, 83	anbi12d 710	. . . . . . . . . . . . . . 15
85	80, 84	orbi12d 709	. . . . . . . . . . . . . 14
86	76, 85	anbi12d 710	. . . . . . . . . . . . 13
87	20, 25, 72, 86, 12	brab 4775	. . . . . . . . . . . 12
88	60, 87	syl6rbbr 264	. . . . . . . . . . 11
89	50, 52, 88	3bitrrd 280	. . . . . . . . . 10
90	89	pm5.32da 641	. . . . . . . . 9
91	90	opabbidv 4515	. . . . . . . 8
92	42, 91	syl5eq 2510	. . . . . . 7
93		isoeq3 6217	. . . . . . 7
94	92, 93	syl 16	. . . . . 6
95	41, 94	syl5ibr 221	. . . . 5
96	1, 39, 95	sylc 60	. . . 4
97		isocnv 6226	. . . 4
98	96, 97	syl 16	. . 3
99		imacnvcnv 5477	. . . . 5
100		fnwe.5	. . . . . . 7
101		vex 3112	. . . . . . 7
102		xpexg 6602	. . . . . . 7
103	100, 101, 102	sylancl 662	. . . . . 6
104		imadmres 5504	. . . . . . 7
105		dmres 5299	. . . . . . . . . . 11
106	105	elin2 3688	. . . . . . . . . 10
107		simprr 757	. . . . . . . . . . . . 13
108		f1dm 5790	. . . . . . . . . . . . . . 15
109	1, 36, 108	3syl 20	. . . . . . . . . . . . . 14
110	109	adantr 465	. . . . . . . . . . . . 13
111	107, 110	eleqtrd 2547	. . . . . . . . . . . 12
112	111, 21	syl 16	. . . . . . . . . . 11
113		ffn 5736	. . . . . . . . . . . . . . . 16
114	1, 113	syl 16	. . . . . . . . . . . . . . 15
115	114	adantr 465	. . . . . . . . . . . . . 14
116		dmres 5299	. . . . . . . . . . . . . . 15
117		inss2 3718	. . . . . . . . . . . . . . . 16
118		fndm 5685	. . . . . . . . . . . . . . . . 17
119	115, 118	syl 16	. . . . . . . . . . . . . . . 16
120	117, 119	syl5sseq 3551	. . . . . . . . . . . . . . 15
121	116, 120	syl5eqss 3547	. . . . . . . . . . . . . 14
122		simprl 756	. . . . . . . . . . . . . . 15
123	111, 119	eleqtrrd 2548	. . . . . . . . . . . . . . 15
124	116	elin2 3688	. . . . . . . . . . . . . . 15
125	122, 123, 124	sylanbrc 664	. . . . . . . . . . . . . 14
126		fnfvima 6150	. . . . . . . . . . . . . 14
127	115, 121, 125, 126	syl3anc 1228	. . . . . . . . . . . . 13
128		imadmres 5504	. . . . . . . . . . . . 13
129	127, 128	syl6eleq 2555	. . . . . . . . . . . 12
130		opelxpi 5036	. . . . . . . . . . . 12
131	129, 122, 130	syl2anc 661	. . . . . . . . . . 11
132	112, 131	eqeltrd 2545	. . . . . . . . . 10
133	106, 132	sylan2b 475	. . . . . . . . 9
134	133	ralrimiva 2871	. . . . . . . 8
135		f1fun 5788	. . . . . . . . . 10
136	1, 36, 135	3syl 20	. . . . . . . . 9
137		resss 5302	. . . . . . . . . 10
138		dmss 5207	. . . . . . . . . 10
139	137, 138	ax-mp 5	. . . . . . . . 9
140		funimass4 5924	. . . . . . . . 9
141	136, 139, 140	sylancl 662	. . . . . . . 8
142	134, 141	mpbird 232	. . . . . . 7
143	104, 142	syl5eqssr 3548	. . . . . 6
144	103, 143	ssexd 4599	. . . . 5
145	99, 144	syl5eqel 2549	. . . 4
146	145	alrimiv 1719	. . 3
147		isowe2 6246	. . 3
148	98, 146, 147	syl2anc 661	. 2
149	16, 148	mpd 15	1

Syntax hints:  ->wi 4  <->wb 184  \/wo 368  /\wa 369  A.wal 1393  =wceq 1395  e.wcel 1818  A.wral 2807  cvv 3109  i^icin 3474  C_wss 3475  <.cop 4035   class class class wbr 4452  {copab 4509  e.cmpt 4510  Wewwe 4842  X.cxp 5002  `'ccnv 5003  domcdm 5004  rancrn 5005  |`cres 5006  "cima 5007  Relwrel 5009  Funwfun 5587  Fnwfn 5588  -->wf 5589  -1-1->wf1 5590  -1-1-onto->wf1o 5592  `cfv 5593  Isomwiso 5594  c1st 6798  c2nd 6799

This theorem is referenced by:  fnwe  6916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-int 4287  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602  df-1st 6800  df-2nd 6801