imasaddfnlem - Metamath Proof Explorer

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

Theorem imasaddfnlem 14580

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 4659	. . . . . . . . 9
2		fvex 5804	. . . . . . . . 9
3	1, 2	relsnop 5047	. . . . . . . 8
4	3	rgenw 2895	. . . . . . 7
5		reliun 5063	. . . . . . 7
6	4, 5	mpbir 209	. . . . . 6
7	6	rgenw 2895	. . . . 5
8		reliun 5063	. . . . 5
9	7, 8	mpbir 209	. . . 4
10		imasaddflem.a	. . . . 5
11	10	releqd 5027	. . . 4
12	9, 11	mpbiri 233	. . 3
13		imasaddf.f	. . . . . . . . . . . . . . . . . 18
14		fof 5723	. . . . . . . . . . . . . . . . . 18
15	13, 14	syl 16	. . . . . . . . . . . . . . . . 17
16		ffvelrn 5945	. . . . . . . . . . . . . . . . . 18 $/\$
17		ffvelrn 5945	. . . . . . . . . . . . . . . . . 18 $/\$
18	16, 17	anim12dan 833	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
19	15, 18	sylan 471	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
20		opelxpi 4974	. . . . . . . . . . . . . . . 16 $/\$
21	19, 20	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
22		opelxpi 4974	. . . . . . . . . . . . . . 15 $/\$
23	21, 2, 22	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$
24	23	snssd 4121	. . . . . . . . . . . . 13 $/\$ $/\$
25	24	anassrs 648	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralrimiva 2827	. . . . . . . . . . 11 $/\$
27		iunss 4314	. . . . . . . . . . 11
28	26, 27	sylibr 212	. . . . . . . . . 10 $/\$
29	28	ralrimiva 2827	. . . . . . . . 9
30		iunss 4314	. . . . . . . . 9
31	29, 30	sylibr 212	. . . . . . . 8
32	10, 31	eqsstrd 3493	. . . . . . 7
33		dmss 5142	. . . . . . 7
34	32, 33	syl 16	. . . . . 6
35		vn0 3747	. . . . . . 7
36		dmxp 5161	. . . . . . 7
37	35, 36	ax-mp 5	. . . . . 6
38	34, 37	syl6sseq 3505	. . . . 5
39		forn 5726	. . . . . . 7
40	13, 39	syl 16	. . . . . 6
41	40, 40	xpeq12d 4968	. . . . 5
42	38, 41	sseqtr4d 3496	. . . 4
43	10	eleq2d 2522	. . . . . . . . . . . . 13
44	43	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
45		df-br 4396	. . . . . . . . . . . 12
46		eliun 4278	. . . . . . . . . . . . 13
47		eliun 4278	. . . . . . . . . . . . . 14
48	47	rexbii 2861	. . . . . . . . . . . . 13
49	46, 48	bitr2i 250	. . . . . . . . . . . 12
50	44, 45, 49	3bitr4g 288	. . . . . . . . . . 11 $/\$ $/\$
51		opex 4659	. . . . . . . . . . . . . . 15
52	51	elsnc 4004	. . . . . . . . . . . . . 14
53		opex 4659	. . . . . . . . . . . . . . . 16
54		vex 3075	. . . . . . . . . . . . . . . 16
55	53, 54	opth 4669	. . . . . . . . . . . . . . 15 $/\$
56		fvex 5804	. . . . . . . . . . . . . . . . . . 19
57		fvex 5804	. . . . . . . . . . . . . . . . . . 19
58	56, 57	opth 4669	. . . . . . . . . . . . . . . . . 18 $/\$
59		imasaddf.e	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
60	58, 59	syl5bi 217	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
61		eqeq2 2467	. . . . . . . . . . . . . . . . . 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 1188	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
68	67	rexlimdvva 2948	. . . . . . . . . . 11 $/\$ $/\$
69	50, 68	sylbid 215	. . . . . . . . . 10 $/\$ $/\$
70	69	alrimiv 1686	. . . . . . . . 9 $/\$ $/\$
71		mo2icl 3239	. . . . . . . . 9
72	70, 71	syl 16	. . . . . . . 8 $/\$ $/\$
73	72	ralrimivva 2908	. . . . . . 7
74		fofn 5725	. . . . . . . . . 10
75	13, 74	syl 16	. . . . . . . . 9
76		opeq2 4163	. . . . . . . . . . . 12
77	76	breq1d 4405	. . . . . . . . . . 11
78	77	mobidv 2285	. . . . . . . . . 10
79	78	ralrn 5950	. . . . . . . . 9
80	75, 79	syl 16	. . . . . . . 8
81	80	ralbidv 2843	. . . . . . 7
82	73, 81	mpbird 232	. . . . . 6
83		opeq1 4162	. . . . . . . . . . 11
84	83	breq1d 4405	. . . . . . . . . 10
85	84	mobidv 2285	. . . . . . . . 9
86	85	ralbidv 2843	. . . . . . . 8
87	86	ralrn 5950	. . . . . . 7
88	75, 87	syl 16	. . . . . 6
89	82, 88	mpbird 232	. . . . 5
90		breq1 4398	. . . . . . 7
91	90	mobidv 2285	. . . . . 6
92	91	ralxp 5084	. . . . 5
93	89, 92	sylibr 212	. . . 4
94		ssralv 3519	. . . 4
95	42, 93, 94	sylc 60	. . 3
96		dffun7 5547	. . 3 $/\$
97	12, 95, 96	sylanbrc 664	. 2
98		eqimss2 3512	. . . . . . . . . . 11
99	10, 98	syl 16	. . . . . . . . . 10
100		iunss 4314	. . . . . . . . . 10
101	99, 100	sylib 196	. . . . . . . . 9
102		iunss 4314	. . . . . . . . . . 11
103		opex 4659	. . . . . . . . . . . . . 14
104	103	snss 4102	. . . . . . . . . . . . 13
105	1, 2	opeldm 5146	. . . . . . . . . . . . 13
106	104, 105	sylbir 213	. . . . . . . . . . . 12
107	106	ralimi 2816	. . . . . . . . . . 11
108	102, 107	sylbi 195	. . . . . . . . . 10
109	108	ralimi 2816	. . . . . . . . 9
110	101, 109	syl 16	. . . . . . . 8
111		opeq2 4163	. . . . . . . . . . . 12
112	111	eleq1d 2521	. . . . . . . . . . 11
113	112	ralrn 5950	. . . . . . . . . 10
114	75, 113	syl 16	. . . . . . . . 9
115	114	ralbidv 2843	. . . . . . . 8
116	110, 115	mpbird 232	. . . . . . 7
117		opeq1 4162	. . . . . . . . . . 11
118	117	eleq1d 2521	. . . . . . . . . 10
119	118	ralbidv 2843	. . . . . . . . 9
120	119	ralrn 5950	. . . . . . . 8
121	75, 120	syl 16	. . . . . . 7
122	116, 121	mpbird 232	. . . . . 6
123		eleq1 2524	. . . . . . 7
124	123	ralxp 5084	. . . . . 6
125	122, 124	sylibr 212	. . . . 5
126		dfss3 3449	. . . . 5
127	125, 126	sylibr 212	. . . 4
128	41, 127	eqsstr3d 3494	. . 3
129	38, 128	eqssd 3476	. 2
130		df-fn 5524	. 2 $/\$
131	97, 129, 130	sylanbrc 664	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wal 1368

wceq 1370

wcel 1758

wmo 2262

wne 2645

wral 2796

wrex 2797

cvv 3072

wss 3431

c0 3740

csn 3980

cop 3986

ciun 4274 class class class wbr 4395

cxp 4941

cdm 4943

crn 4944

wrel 4948

wfun 5515

wfn 5516

wf 5517

wfo 5519

cfv 5521 (class class class)co 6195

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 ax-sep 4516 ax-nul 4524 ax-pr 4634

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2265 df-mo 2266 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-ne 2647 df-ral 2801 df-rex 2802 df-rab 2805 df-v 3074 df-sbc 3289 df-csb 3391 df-dif 3434 df-un 3436 df-in 3438 df-ss 3445 df-nul 3741 df-if 3895 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4195 df-iun 4276 df-br 4396 df-opab 4454 df-mpt 4455 df-id 4739 df-xp 4949 df-rel 4950 df-cnv 4951 df-co 4952 df-dm 4953 df-rn 4954 df-iota 5484 df-fun 5523 df-fn 5524 df-f 5525 df-fo 5527 df-fv 5529

This theorem is referenced by: imasaddvallem 14581 imasaddflem 14582 imasaddfn 14583 imasmulfn 14586

W3C validator