imasaddfnlem - Metamath Proof Explorer

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

Theorem imasaddfnlem 14783

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 4711	. . . . . . . . 9
2		fvex 5876	. . . . . . . . 9
3	1, 2	relsnop 5107	. . . . . . . 8
4	3	rgenw 2825	. . . . . . 7
5		reliun 5123	. . . . . . 7
6	4, 5	mpbir 209	. . . . . 6
7	6	rgenw 2825	. . . . 5
8		reliun 5123	. . . . 5
9	7, 8	mpbir 209	. . . 4
10		imasaddflem.a	. . . . 5
11	10	releqd 5087	. . . 4
12	9, 11	mpbiri 233	. . 3
13		imasaddf.f	. . . . . . . . . . . . . . . . . 18
14		fof 5795	. . . . . . . . . . . . . . . . . 18
15	13, 14	syl 16	. . . . . . . . . . . . . . . . 17
16		ffvelrn 6019	. . . . . . . . . . . . . . . . . 18 $/\$
17		ffvelrn 6019	. . . . . . . . . . . . . . . . . 18 $/\$
18	16, 17	anim12dan 835	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
19	15, 18	sylan 471	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
20		opelxpi 5031	. . . . . . . . . . . . . . . 16 $/\$
21	19, 20	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
22		opelxpi 5031	. . . . . . . . . . . . . . 15 $/\$
23	21, 2, 22	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$
24	23	snssd 4172	. . . . . . . . . . . . 13 $/\$ $/\$
25	24	anassrs 648	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralrimiva 2878	. . . . . . . . . . 11 $/\$
27		iunss 4366	. . . . . . . . . . 11
28	26, 27	sylibr 212	. . . . . . . . . 10 $/\$
29	28	ralrimiva 2878	. . . . . . . . 9
30		iunss 4366	. . . . . . . . 9
31	29, 30	sylibr 212	. . . . . . . 8
32	10, 31	eqsstrd 3538	. . . . . . 7
33		dmss 5202	. . . . . . 7
34	32, 33	syl 16	. . . . . 6
35		vn0 3792	. . . . . . 7
36		dmxp 5221	. . . . . . 7
37	35, 36	ax-mp 5	. . . . . 6
38	34, 37	syl6sseq 3550	. . . . 5
39		forn 5798	. . . . . . 7
40	13, 39	syl 16	. . . . . 6
41	40, 40	xpeq12d 5024	. . . . 5
42	38, 41	sseqtr4d 3541	. . . 4
43	10	eleq2d 2537	. . . . . . . . . . . . 13
44	43	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
45		df-br 4448	. . . . . . . . . . . 12
46		eliun 4330	. . . . . . . . . . . . 13
47		eliun 4330	. . . . . . . . . . . . . 14
48	47	rexbii 2965	. . . . . . . . . . . . 13
49	46, 48	bitr2i 250	. . . . . . . . . . . 12
50	44, 45, 49	3bitr4g 288	. . . . . . . . . . 11 $/\$ $/\$
51		opex 4711	. . . . . . . . . . . . . . 15
52	51	elsnc 4051	. . . . . . . . . . . . . 14
53		opex 4711	. . . . . . . . . . . . . . . 16
54		vex 3116	. . . . . . . . . . . . . . . 16
55	53, 54	opth 4721	. . . . . . . . . . . . . . 15 $/\$
56		fvex 5876	. . . . . . . . . . . . . . . . . . 19
57		fvex 5876	. . . . . . . . . . . . . . . . . . 19
58	56, 57	opth 4721	. . . . . . . . . . . . . . . . . 18 $/\$
59		imasaddf.e	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
60	58, 59	syl5bi 217	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
61		eqeq2 2482	. . . . . . . . . . . . . . . . . 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 1196	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
68	67	rexlimdvva 2962	. . . . . . . . . . 11 $/\$ $/\$
69	50, 68	sylbid 215	. . . . . . . . . 10 $/\$ $/\$
70	69	alrimiv 1695	. . . . . . . . 9 $/\$ $/\$
71		mo2icl 3282	. . . . . . . . 9
72	70, 71	syl 16	. . . . . . . 8 $/\$ $/\$
73	72	ralrimivva 2885	. . . . . . 7
74		fofn 5797	. . . . . . . . . 10
75	13, 74	syl 16	. . . . . . . . 9
76		opeq2 4214	. . . . . . . . . . . 12
77	76	breq1d 4457	. . . . . . . . . . 11
78	77	mobidv 2299	. . . . . . . . . 10
79	78	ralrn 6024	. . . . . . . . 9
80	75, 79	syl 16	. . . . . . . 8
81	80	ralbidv 2903	. . . . . . 7
82	73, 81	mpbird 232	. . . . . 6
83		opeq1 4213	. . . . . . . . . . 11
84	83	breq1d 4457	. . . . . . . . . 10
85	84	mobidv 2299	. . . . . . . . 9
86	85	ralbidv 2903	. . . . . . . 8
87	86	ralrn 6024	. . . . . . 7
88	75, 87	syl 16	. . . . . 6
89	82, 88	mpbird 232	. . . . 5
90		breq1 4450	. . . . . . 7
91	90	mobidv 2299	. . . . . 6
92	91	ralxp 5144	. . . . 5
93	89, 92	sylibr 212	. . . 4
94		ssralv 3564	. . . 4
95	42, 93, 94	sylc 60	. . 3
96		dffun7 5614	. . 3 $/\$
97	12, 95, 96	sylanbrc 664	. 2
98		eqimss2 3557	. . . . . . . . . . 11
99	10, 98	syl 16	. . . . . . . . . 10
100		iunss 4366	. . . . . . . . . 10
101	99, 100	sylib 196	. . . . . . . . 9
102		iunss 4366	. . . . . . . . . . 11
103		opex 4711	. . . . . . . . . . . . . 14
104	103	snss 4151	. . . . . . . . . . . . 13
105	1, 2	opeldm 5206	. . . . . . . . . . . . 13
106	104, 105	sylbir 213	. . . . . . . . . . . 12
107	106	ralimi 2857	. . . . . . . . . . 11
108	102, 107	sylbi 195	. . . . . . . . . 10
109	108	ralimi 2857	. . . . . . . . 9
110	101, 109	syl 16	. . . . . . . 8
111		opeq2 4214	. . . . . . . . . . . 12
112	111	eleq1d 2536	. . . . . . . . . . 11
113	112	ralrn 6024	. . . . . . . . . 10
114	75, 113	syl 16	. . . . . . . . 9
115	114	ralbidv 2903	. . . . . . . 8
116	110, 115	mpbird 232	. . . . . . 7
117		opeq1 4213	. . . . . . . . . . 11
118	117	eleq1d 2536	. . . . . . . . . 10
119	118	ralbidv 2903	. . . . . . . . 9
120	119	ralrn 6024	. . . . . . . 8
121	75, 120	syl 16	. . . . . . 7
122	116, 121	mpbird 232	. . . . . 6
123		eleq1 2539	. . . . . . 7
124	123	ralxp 5144	. . . . . 6
125	122, 124	sylibr 212	. . . . 5
126		dfss3 3494	. . . . 5
127	125, 126	sylibr 212	. . . 4
128	41, 127	eqsstr3d 3539	. . 3
129	38, 128	eqssd 3521	. 2
130		df-fn 5591	. 2 $/\$
131	97, 129, 130	sylanbrc 664	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wal 1377

wceq 1379

wcel 1767

wmo 2276

wne 2662

wral 2814

wrex 2815

cvv 3113

wss 3476

c0 3785

csn 4027

cop 4033

ciun 4325 class class class wbr 4447

cxp 4997

cdm 4999

crn 5000

wrel 5004

wfun 5582

wfn 5583

wf 5584

wfo 5586

cfv 5588 (class class class)co 6284

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pr 4686

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-if 3940 df-sn 4028 df-pr 4030 df-op 4034 df-uni 4246 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-id 4795 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-fo 5594 df-fv 5596

This theorem is referenced by: imasaddvallem 14784 imasaddflem 14785 imasaddfn 14786 imasmulfn 14789

W3C validator