imasaddfnlem - Metamath Proof Explorer

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

Theorem imasaddfnlem 14907

Description: The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015.)

**Hypotheses**
Ref	Expression
imasaddf.f
imasaddf.e	$/\$ $/\$ $/\$ $/\$ $/\$
imasaddflem.a

**Assertion**
Ref	Expression
imasaddfnlem

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem imasaddfnlem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opex 4701	. . . . . . . . 9
2		fvex 5866	. . . . . . . . 9
3	1, 2	relsnop 5097	. . . . . . . 8
4	3	rgenw 2804	. . . . . . 7
5		reliun 5113	. . . . . . 7
6	4, 5	mpbir 209	. . . . . 6
7	6	rgenw 2804	. . . . 5
8		reliun 5113	. . . . 5
9	7, 8	mpbir 209	. . . 4
10		imasaddflem.a	. . . . 5
11	10	releqd 5077	. . . 4
12	9, 11	mpbiri 233	. . 3
13		imasaddf.f	. . . . . . . . . . . . . . . . . 18
14		fof 5785	. . . . . . . . . . . . . . . . . 18
15	13, 14	syl 16	. . . . . . . . . . . . . . . . 17
16		ffvelrn 6014	. . . . . . . . . . . . . . . . . 18 $/\$
17		ffvelrn 6014	. . . . . . . . . . . . . . . . . 18 $/\$
18	16, 17	anim12dan 837	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
19	15, 18	sylan 471	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
20		opelxpi 5021	. . . . . . . . . . . . . . . 16 $/\$
21	19, 20	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
22		opelxpi 5021	. . . . . . . . . . . . . . 15 $/\$
23	21, 2, 22	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$
24	23	snssd 4160	. . . . . . . . . . . . 13 $/\$ $/\$
25	24	anassrs 648	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralrimiva 2857	. . . . . . . . . . 11 $/\$
27		iunss 4356	. . . . . . . . . . 11
28	26, 27	sylibr 212	. . . . . . . . . 10 $/\$
29	28	ralrimiva 2857	. . . . . . . . 9
30		iunss 4356	. . . . . . . . 9
31	29, 30	sylibr 212	. . . . . . . 8
32	10, 31	eqsstrd 3523	. . . . . . 7
33		dmss 5192	. . . . . . 7
34	32, 33	syl 16	. . . . . 6
35		vn0 3778	. . . . . . 7
36		dmxp 5211	. . . . . . 7
37	35, 36	ax-mp 5	. . . . . 6
38	34, 37	syl6sseq 3535	. . . . 5
39		forn 5788	. . . . . . 7
40	13, 39	syl 16	. . . . . 6
41	40	sqxpeqd 5015	. . . . 5
42	38, 41	sseqtr4d 3526	. . . 4
43	10	eleq2d 2513	. . . . . . . . . . . . 13
44	43	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
45		df-br 4438	. . . . . . . . . . . 12
46		eliun 4320	. . . . . . . . . . . . 13
47		eliun 4320	. . . . . . . . . . . . . 14
48	47	rexbii 2945	. . . . . . . . . . . . 13
49	46, 48	bitr2i 250	. . . . . . . . . . . 12
50	44, 45, 49	3bitr4g 288	. . . . . . . . . . 11 $/\$ $/\$
51		opex 4701	. . . . . . . . . . . . . . 15
52	51	elsnc 4038	. . . . . . . . . . . . . 14
53		opex 4701	. . . . . . . . . . . . . . . 16
54		vex 3098	. . . . . . . . . . . . . . . 16
55	53, 54	opth 4711	. . . . . . . . . . . . . . 15 $/\$
56		fvex 5866	. . . . . . . . . . . . . . . . . . 19
57		fvex 5866	. . . . . . . . . . . . . . . . . . 19
58	56, 57	opth 4711	. . . . . . . . . . . . . . . . . 18 $/\$
59		imasaddf.e	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
60	58, 59	syl5bi 217	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
61		eqeq2 2458	. . . . . . . . . . . . . . . . . 18
62	61	biimprd 223	. . . . . . . . . . . . . . . . 17
63	60, 62	syl6 33	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
64	63	impd 431	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
65	55, 64	syl5bi 217	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
66	52, 65	syl5bi 217	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	66	3expa 1197	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
68	67	rexlimdvva 2942	. . . . . . . . . . 11 $/\$ $/\$
69	50, 68	sylbid 215	. . . . . . . . . 10 $/\$ $/\$
70	69	alrimiv 1706	. . . . . . . . 9 $/\$ $/\$
71		mo2icl 3264	. . . . . . . . 9
72	70, 71	syl 16	. . . . . . . 8 $/\$ $/\$
73	72	ralrimivva 2864	. . . . . . 7
74		fofn 5787	. . . . . . . . . 10
75	13, 74	syl 16	. . . . . . . . 9
76		opeq2 4203	. . . . . . . . . . . 12
77	76	breq1d 4447	. . . . . . . . . . 11
78	77	mobidv 2291	. . . . . . . . . 10
79	78	ralrn 6019	. . . . . . . . 9
80	75, 79	syl 16	. . . . . . . 8
81	80	ralbidv 2882	. . . . . . 7
82	73, 81	mpbird 232	. . . . . 6
83		opeq1 4202	. . . . . . . . . . 11
84	83	breq1d 4447	. . . . . . . . . 10
85	84	mobidv 2291	. . . . . . . . 9
86	85	ralbidv 2882	. . . . . . . 8
87	86	ralrn 6019	. . . . . . 7
88	75, 87	syl 16	. . . . . 6
89	82, 88	mpbird 232	. . . . 5
90		breq1 4440	. . . . . . 7
91	90	mobidv 2291	. . . . . 6
92	91	ralxp 5134	. . . . 5
93	89, 92	sylibr 212	. . . 4
94		ssralv 3549	. . . 4
95	42, 93, 94	sylc 60	. . 3
96		dffun7 5604	. . 3 $/\$
97	12, 95, 96	sylanbrc 664	. 2
98		eqimss2 3542	. . . . . . . . . . 11
99	10, 98	syl 16	. . . . . . . . . 10
100		iunss 4356	. . . . . . . . . 10
101	99, 100	sylib 196	. . . . . . . . 9
102		iunss 4356	. . . . . . . . . . 11
103		opex 4701	. . . . . . . . . . . . . 14
104	103	snss 4139	. . . . . . . . . . . . 13
105	1, 2	opeldm 5196	. . . . . . . . . . . . 13
106	104, 105	sylbir 213	. . . . . . . . . . . 12
107	106	ralimi 2836	. . . . . . . . . . 11
108	102, 107	sylbi 195	. . . . . . . . . 10
109	108	ralimi 2836	. . . . . . . . 9
110	101, 109	syl 16	. . . . . . . 8
111		opeq2 4203	. . . . . . . . . . . 12
112	111	eleq1d 2512	. . . . . . . . . . 11
113	112	ralrn 6019	. . . . . . . . . 10
114	75, 113	syl 16	. . . . . . . . 9
115	114	ralbidv 2882	. . . . . . . 8
116	110, 115	mpbird 232	. . . . . . 7
117		opeq1 4202	. . . . . . . . . . 11
118	117	eleq1d 2512	. . . . . . . . . 10
119	118	ralbidv 2882	. . . . . . . . 9
120	119	ralrn 6019	. . . . . . . 8
121	75, 120	syl 16	. . . . . . 7
122	116, 121	mpbird 232	. . . . . 6
123		eleq1 2515	. . . . . . 7
124	123	ralxp 5134	. . . . . 6
125	122, 124	sylibr 212	. . . . 5
126		dfss3 3479	. . . . 5
127	125, 126	sylibr 212	. . . 4
128	41, 127	eqsstr3d 3524	. . 3
129	38, 128	eqssd 3506	. 2
130		df-fn 5581	. 2 $/\$
131	97, 129, 130	sylanbrc 664	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 974

wal 1381

wceq 1383

wcel 1804

wmo 2269

wne 2638

wral 2793

wrex 2794

cvv 3095

wss 3461

c0 3770

csn 4014

cop 4020

ciun 4315 class class class wbr 4437

cxp 4987

cdm 4989

crn 4990

wrel 4994

wfun 5572

wfn 5573

wf 5574

wfo 5576

cfv 5578 (class class class)co 6281

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-sep 4558 ax-nul 4566 ax-pr 4676

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-ral 2798 df-rex 2799 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-nul 3771 df-if 3927 df-sn 4015 df-pr 4017 df-op 4021 df-uni 4235 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-id 4785 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-fo 5584 df-fv 5586

This theorem is referenced by: imasaddvallem 14908 imasaddflem 14909 imasaddfn 14910 imasmulfn 14913

W3C validator