imasaddfnlem - Metamath Proof Explorer

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

Theorem imasaddfnlem 15427

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 4663	. . . . . . . . 9
2		fvex 5873	. . . . . . . . 9
3	1, 2	relsnop 4938	. . . . . . . 8
4	3	rgenw 2748	. . . . . . 7
5		reliun 4953	. . . . . . 7
6	4, 5	mpbir 213	. . . . . 6
7	6	rgenw 2748	. . . . 5
8		reliun 4953	. . . . 5
9	7, 8	mpbir 213	. . . 4
10		imasaddflem.a	. . . . 5
11	10	releqd 4918	. . . 4
12	9, 11	mpbiri 237	. . 3
13		imasaddf.f	. . . . . . . . . . . . . . . . . 18
14		fof 5791	. . . . . . . . . . . . . . . . . 18
15	13, 14	syl 17	. . . . . . . . . . . . . . . . 17
16		ffvelrn 6018	. . . . . . . . . . . . . . . . . 18 $/\$
17		ffvelrn 6018	. . . . . . . . . . . . . . . . . 18 $/\$
18	16, 17	anim12dan 847	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
19	15, 18	sylan 474	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
20		opelxpi 4865	. . . . . . . . . . . . . . . 16 $/\$
21	19, 20	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
22		opelxpi 4865	. . . . . . . . . . . . . . 15 $/\$
23	21, 2, 22	sylancl 667	. . . . . . . . . . . . . 14 $/\$ $/\$
24	23	snssd 4116	. . . . . . . . . . . . 13 $/\$ $/\$
25	24	anassrs 653	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralrimiva 2801	. . . . . . . . . . 11 $/\$
27		iunss 4318	. . . . . . . . . . 11
28	26, 27	sylibr 216	. . . . . . . . . 10 $/\$
29	28	ralrimiva 2801	. . . . . . . . 9
30		iunss 4318	. . . . . . . . 9
31	29, 30	sylibr 216	. . . . . . . 8
32	10, 31	eqsstrd 3465	. . . . . . 7
33		dmss 5033	. . . . . . 7
34	32, 33	syl 17	. . . . . 6
35		vn0 3738	. . . . . . 7
36		dmxp 5052	. . . . . . 7
37	35, 36	ax-mp 5	. . . . . 6
38	34, 37	syl6sseq 3477	. . . . 5
39		forn 5794	. . . . . . 7
40	13, 39	syl 17	. . . . . 6
41	40	sqxpeqd 4859	. . . . 5
42	38, 41	sseqtr4d 3468	. . . 4
43	10	eleq2d 2513	. . . . . . . . . . . . 13
44	43	adantr 467	. . . . . . . . . . . 12 $/\$ $/\$
45		df-br 4402	. . . . . . . . . . . 12
46		eliun 4282	. . . . . . . . . . . . 13
47		eliun 4282	. . . . . . . . . . . . . 14
48	47	rexbii 2888	. . . . . . . . . . . . 13
49	46, 48	bitr2i 254	. . . . . . . . . . . 12
50	44, 45, 49	3bitr4g 292	. . . . . . . . . . 11 $/\$ $/\$
51		opex 4663	. . . . . . . . . . . . . . 15
52	51	elsnc 3991	. . . . . . . . . . . . . 14
53		opex 4663	. . . . . . . . . . . . . . . 16
54		vex 3047	. . . . . . . . . . . . . . . 16
55	53, 54	opth 4675	. . . . . . . . . . . . . . 15 $/\$
56		fvex 5873	. . . . . . . . . . . . . . . . . . 19
57		fvex 5873	. . . . . . . . . . . . . . . . . . 19
58	56, 57	opth 4675	. . . . . . . . . . . . . . . . . 18 $/\$
59		imasaddf.e	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
60	58, 59	syl5bi 221	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
61		eqeq2 2461	. . . . . . . . . . . . . . . . . 18
62	61	biimprd 227	. . . . . . . . . . . . . . . . 17
63	60, 62	syl6 34	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
64	63	impd 433	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
65	55, 64	syl5bi 221	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
66	52, 65	syl5bi 221	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	66	3expa 1207	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
68	67	rexlimdvva 2885	. . . . . . . . . . 11 $/\$ $/\$
69	50, 68	sylbid 219	. . . . . . . . . 10 $/\$ $/\$
70	69	alrimiv 1772	. . . . . . . . 9 $/\$ $/\$
71		mo2icl 3216	. . . . . . . . 9
72	70, 71	syl 17	. . . . . . . 8 $/\$ $/\$
73	72	ralrimivva 2808	. . . . . . 7
74		fofn 5793	. . . . . . . . . 10
75	13, 74	syl 17	. . . . . . . . 9
76		opeq2 4166	. . . . . . . . . . . 12
77	76	breq1d 4411	. . . . . . . . . . 11
78	77	mobidv 2319	. . . . . . . . . 10
79	78	ralrn 6023	. . . . . . . . 9
80	75, 79	syl 17	. . . . . . . 8
81	80	ralbidv 2826	. . . . . . 7
82	73, 81	mpbird 236	. . . . . 6
83		opeq1 4165	. . . . . . . . . . 11
84	83	breq1d 4411	. . . . . . . . . 10
85	84	mobidv 2319	. . . . . . . . 9
86	85	ralbidv 2826	. . . . . . . 8
87	86	ralrn 6023	. . . . . . 7
88	75, 87	syl 17	. . . . . 6
89	82, 88	mpbird 236	. . . . 5
90		breq1 4404	. . . . . . 7
91	90	mobidv 2319	. . . . . 6
92	91	ralxp 4975	. . . . 5
93	89, 92	sylibr 216	. . . 4
94		ssralv 3492	. . . 4
95	42, 93, 94	sylc 62	. . 3
96		dffun7 5607	. . 3 $/\$
97	12, 95, 96	sylanbrc 669	. 2
98		eqimss2 3484	. . . . . . . . . . 11
99	10, 98	syl 17	. . . . . . . . . 10
100		iunss 4318	. . . . . . . . . 10
101	99, 100	sylib 200	. . . . . . . . 9
102		iunss 4318	. . . . . . . . . . 11
103		opex 4663	. . . . . . . . . . . . . 14
104	103	snss 4095	. . . . . . . . . . . . 13
105	1, 2	opeldm 5037	. . . . . . . . . . . . 13
106	104, 105	sylbir 217	. . . . . . . . . . . 12
107	106	ralimi 2780	. . . . . . . . . . 11
108	102, 107	sylbi 199	. . . . . . . . . 10
109	108	ralimi 2780	. . . . . . . . 9
110	101, 109	syl 17	. . . . . . . 8
111		opeq2 4166	. . . . . . . . . . . 12
112	111	eleq1d 2512	. . . . . . . . . . 11
113	112	ralrn 6023	. . . . . . . . . 10
114	75, 113	syl 17	. . . . . . . . 9
115	114	ralbidv 2826	. . . . . . . 8
116	110, 115	mpbird 236	. . . . . . 7
117		opeq1 4165	. . . . . . . . . . 11
118	117	eleq1d 2512	. . . . . . . . . 10
119	118	ralbidv 2826	. . . . . . . . 9
120	119	ralrn 6023	. . . . . . . 8
121	75, 120	syl 17	. . . . . . 7
122	116, 121	mpbird 236	. . . . . 6
123		eleq1 2516	. . . . . . 7
124	123	ralxp 4975	. . . . . 6
125	122, 124	sylibr 216	. . . . 5
126		dfss3 3421	. . . . 5
127	125, 126	sylibr 216	. . . 4
128	41, 127	eqsstr3d 3466	. . 3
129	38, 128	eqssd 3448	. 2
130		df-fn 5584	. 2 $/\$
131	97, 129, 130	sylanbrc 669	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 984

wal 1441

wceq 1443

wcel 1886

wmo 2299

wne 2621

wral 2736

wrex 2737

cvv 3044

wss 3403

c0 3730

csn 3967

cop 3973

ciun 4277 class class class wbr 4401

cxp 4831

cdm 4833

crn 4834

wrel 4838

wfun 5575

wfn 5576

wf 5577

wfo 5579

cfv 5581 (class class class)co 6288

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pr 4638

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-ral 2741 df-rex 2742 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-sn 3968 df-pr 3970 df-op 3974 df-uni 4198 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-id 4748 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-fo 5587 df-fv 5589

This theorem is referenced by: imasaddvallem 15428 imasaddflem 15429 imasaddfn 15430 imasmulfn 15433

W3C validator