imasaddfnlem - Metamath Proof Explorer

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

Theorem imasaddfnlem 14462

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 4553	. . . . . . . . 9
2		fvex 5698	. . . . . . . . 9
3	1, 2	relsnop 4940	. . . . . . . 8
4	3	rgenw 2781	. . . . . . 7
5		reliun 4956	. . . . . . 7
6	4, 5	mpbir 209	. . . . . 6
7	6	rgenw 2781	. . . . 5
8		reliun 4956	. . . . 5
9	7, 8	mpbir 209	. . . 4
10		imasaddflem.a	. . . . 5
11	10	releqd 4920	. . . 4
12	9, 11	mpbiri 233	. . 3
13		imasaddf.f	. . . . . . . . . . . . . . . . . 18
14		fof 5617	. . . . . . . . . . . . . . . . . 18
15	13, 14	syl 16	. . . . . . . . . . . . . . . . 17
16		ffvelrn 5838	. . . . . . . . . . . . . . . . . 18 $/\$
17		ffvelrn 5838	. . . . . . . . . . . . . . . . . 18 $/\$
18	16, 17	anim12dan 828	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
19	15, 18	sylan 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
20		opelxpi 4867	. . . . . . . . . . . . . . . 16 $/\$
21	19, 20	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
22		opelxpi 4867	. . . . . . . . . . . . . . 15 $/\$
23	21, 2, 22	sylancl 657	. . . . . . . . . . . . . 14 $/\$ $/\$
24	23	snssd 4015	. . . . . . . . . . . . 13 $/\$ $/\$
25	24	anassrs 643	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralrimiva 2797	. . . . . . . . . . 11 $/\$
27		iunss 4208	. . . . . . . . . . 11
28	26, 27	sylibr 212	. . . . . . . . . 10 $/\$
29	28	ralrimiva 2797	. . . . . . . . 9
30		iunss 4208	. . . . . . . . 9
31	29, 30	sylibr 212	. . . . . . . 8
32	10, 31	eqsstrd 3387	. . . . . . 7
33		dmss 5035	. . . . . . 7
34	32, 33	syl 16	. . . . . 6
35		vn0 3641	. . . . . . 7
36		dmxp 5054	. . . . . . 7
37	35, 36	ax-mp 5	. . . . . 6
38	34, 37	syl6sseq 3399	. . . . 5
39		forn 5620	. . . . . . 7
40	13, 39	syl 16	. . . . . 6
41	40, 40	xpeq12d 4861	. . . . 5
42	38, 41	sseqtr4d 3390	. . . 4
43	10	eleq2d 2508	. . . . . . . . . . . . 13
44	43	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$
45		df-br 4290	. . . . . . . . . . . 12
46		eliun 4172	. . . . . . . . . . . . 13
47		eliun 4172	. . . . . . . . . . . . . 14
48	47	rexbii 2738	. . . . . . . . . . . . 13
49	46, 48	bitr2i 250	. . . . . . . . . . . 12
50	44, 45, 49	3bitr4g 288	. . . . . . . . . . 11 $/\$ $/\$
51		opex 4553	. . . . . . . . . . . . . . 15
52	51	elsnc 3898	. . . . . . . . . . . . . 14
53		opex 4553	. . . . . . . . . . . . . . . 16
54		vex 2973	. . . . . . . . . . . . . . . 16
55	53, 54	opth 4563	. . . . . . . . . . . . . . 15 $/\$
56		fvex 5698	. . . . . . . . . . . . . . . . . . 19
57		fvex 5698	. . . . . . . . . . . . . . . . . . 19
58	56, 57	opth 4563	. . . . . . . . . . . . . . . . . 18 $/\$
59		imasaddf.e	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
60	58, 59	syl5bi 217	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
61		eqeq2 2450	. . . . . . . . . . . . . . . . . 18
62	61	biimprd 223	. . . . . . . . . . . . . . . . 17
63	60, 62	syl6 33	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
64	63	imp3a 431	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
65	55, 64	syl5bi 217	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
66	52, 65	syl5bi 217	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	66	3expa 1182	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
68	67	rexlimdvva 2846	. . . . . . . . . . 11 $/\$ $/\$
69	50, 68	sylbid 215	. . . . . . . . . 10 $/\$ $/\$
70	69	alrimiv 1690	. . . . . . . . 9 $/\$ $/\$
71		mo2icl 3135	. . . . . . . . 9
72	70, 71	syl 16	. . . . . . . 8 $/\$ $/\$
73	72	ralrimivva 2806	. . . . . . 7
74		fofn 5619	. . . . . . . . . 10
75	13, 74	syl 16	. . . . . . . . 9
76		opeq2 4057	. . . . . . . . . . . 12
77	76	breq1d 4299	. . . . . . . . . . 11
78	77	mobidv 2280	. . . . . . . . . 10
79	78	ralrn 5843	. . . . . . . . 9
80	75, 79	syl 16	. . . . . . . 8
81	80	ralbidv 2733	. . . . . . 7
82	73, 81	mpbird 232	. . . . . 6
83		opeq1 4056	. . . . . . . . . . 11
84	83	breq1d 4299	. . . . . . . . . 10
85	84	mobidv 2280	. . . . . . . . 9
86	85	ralbidv 2733	. . . . . . . 8
87	86	ralrn 5843	. . . . . . 7
88	75, 87	syl 16	. . . . . 6
89	82, 88	mpbird 232	. . . . 5
90		breq1 4292	. . . . . . 7
91	90	mobidv 2280	. . . . . 6
92	91	ralxp 4977	. . . . 5
93	89, 92	sylibr 212	. . . 4
94		ssralv 3413	. . . 4
95	42, 93, 94	sylc 60	. . 3
96		dffun7 5441	. . 3 $/\$
97	12, 95, 96	sylanbrc 659	. 2
98		eqimss2 3406	. . . . . . . . . . 11
99	10, 98	syl 16	. . . . . . . . . 10
100		iunss 4208	. . . . . . . . . 10
101	99, 100	sylib 196	. . . . . . . . 9
102		iunss 4208	. . . . . . . . . . 11
103		opex 4553	. . . . . . . . . . . . . 14
104	103	snss 3996	. . . . . . . . . . . . 13
105	1, 2	opeldm 5039	. . . . . . . . . . . . 13
106	104, 105	sylbir 213	. . . . . . . . . . . 12
107	106	ralimi 2789	. . . . . . . . . . 11
108	102, 107	sylbi 195	. . . . . . . . . 10
109	108	ralimi 2789	. . . . . . . . 9
110	101, 109	syl 16	. . . . . . . 8
111		opeq2 4057	. . . . . . . . . . . 12
112	111	eleq1d 2507	. . . . . . . . . . 11
113	112	ralrn 5843	. . . . . . . . . 10
114	75, 113	syl 16	. . . . . . . . 9
115	114	ralbidv 2733	. . . . . . . 8
116	110, 115	mpbird 232	. . . . . . 7
117		opeq1 4056	. . . . . . . . . . 11
118	117	eleq1d 2507	. . . . . . . . . 10
119	118	ralbidv 2733	. . . . . . . . 9
120	119	ralrn 5843	. . . . . . . 8
121	75, 120	syl 16	. . . . . . 7
122	116, 121	mpbird 232	. . . . . 6
123		eleq1 2501	. . . . . . 7
124	123	ralxp 4977	. . . . . 6
125	122, 124	sylibr 212	. . . . 5
126		dfss3 3343	. . . . 5
127	125, 126	sylibr 212	. . . 4
128	41, 127	eqsstr3d 3388	. . 3
129	38, 128	eqssd 3370	. 2
130		df-fn 5418	. 2 $/\$
131	97, 129, 130	sylanbrc 659	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wal 1362

wceq 1364

wcel 1761

wmo 2258

wne 2604

wral 2713

wrex 2714

cvv 2970

wss 3325

c0 3634

csn 3874

cop 3880

ciun 4168 class class class wbr 4289

cxp 4834

cdm 4836

crn 4837

wrel 4841

wfun 5409

wfn 5410

wf 5411

wfo 5413

cfv 5415 (class class class)co 6090

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-sep 4410 ax-nul 4418 ax-pr 4528

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-ral 2718 df-rex 2719 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-nul 3635 df-if 3789 df-sn 3875 df-pr 3877 df-op 3881 df-uni 4089 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-id 4632 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-fo 5421 df-fv 5423

This theorem is referenced by: imasaddvallem 14463 imasaddflem 14464 imasaddfn 14465 imasmulfn 14468

W3C validator