imasaddfnlem - Metamath Proof Explorer

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

Theorem imasaddfnlem 14935

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 4626	. . . . . . . . 9
2		fvex 5784	. . . . . . . . 9
3	1, 2	relsnop 5020	. . . . . . . 8
4	3	rgenw 2743	. . . . . . 7
5		reliun 5035	. . . . . . 7
6	4, 5	mpbir 209	. . . . . 6
7	6	rgenw 2743	. . . . 5
8		reliun 5035	. . . . 5
9	7, 8	mpbir 209	. . . 4
10		imasaddflem.a	. . . . 5
11	10	releqd 5000	. . . 4
12	9, 11	mpbiri 233	. . 3
13		imasaddf.f	. . . . . . . . . . . . . . . . . 18
14		fof 5703	. . . . . . . . . . . . . . . . . 18
15	13, 14	syl 16	. . . . . . . . . . . . . . . . 17
16		ffvelrn 5931	. . . . . . . . . . . . . . . . . 18 $/\$
17		ffvelrn 5931	. . . . . . . . . . . . . . . . . 18 $/\$
18	16, 17	anim12dan 835	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
19	15, 18	sylan 469	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
20		opelxpi 4945	. . . . . . . . . . . . . . . 16 $/\$
21	19, 20	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
22		opelxpi 4945	. . . . . . . . . . . . . . 15 $/\$
23	21, 2, 22	sylancl 660	. . . . . . . . . . . . . 14 $/\$ $/\$
24	23	snssd 4089	. . . . . . . . . . . . 13 $/\$ $/\$
25	24	anassrs 646	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralrimiva 2796	. . . . . . . . . . 11 $/\$
27		iunss 4284	. . . . . . . . . . 11
28	26, 27	sylibr 212	. . . . . . . . . 10 $/\$
29	28	ralrimiva 2796	. . . . . . . . 9
30		iunss 4284	. . . . . . . . 9
31	29, 30	sylibr 212	. . . . . . . 8
32	10, 31	eqsstrd 3451	. . . . . . 7
33		dmss 5115	. . . . . . 7
34	32, 33	syl 16	. . . . . 6
35		vn0 3719	. . . . . . 7
36		dmxp 5134	. . . . . . 7
37	35, 36	ax-mp 5	. . . . . 6
38	34, 37	syl6sseq 3463	. . . . 5
39		forn 5706	. . . . . . 7
40	13, 39	syl 16	. . . . . 6
41	40	sqxpeqd 4939	. . . . 5
42	38, 41	sseqtr4d 3454	. . . 4
43	10	eleq2d 2452	. . . . . . . . . . . . 13
44	43	adantr 463	. . . . . . . . . . . 12 $/\$ $/\$
45		df-br 4368	. . . . . . . . . . . 12
46		eliun 4248	. . . . . . . . . . . . 13
47		eliun 4248	. . . . . . . . . . . . . 14
48	47	rexbii 2884	. . . . . . . . . . . . 13
49	46, 48	bitr2i 250	. . . . . . . . . . . 12
50	44, 45, 49	3bitr4g 288	. . . . . . . . . . 11 $/\$ $/\$
51		opex 4626	. . . . . . . . . . . . . . 15
52	51	elsnc 3968	. . . . . . . . . . . . . 14
53		opex 4626	. . . . . . . . . . . . . . . 16
54		vex 3037	. . . . . . . . . . . . . . . 16
55	53, 54	opth 4636	. . . . . . . . . . . . . . 15 $/\$
56		fvex 5784	. . . . . . . . . . . . . . . . . . 19
57		fvex 5784	. . . . . . . . . . . . . . . . . . 19
58	56, 57	opth 4636	. . . . . . . . . . . . . . . . . 18 $/\$
59		imasaddf.e	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
60	58, 59	syl5bi 217	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
61		eqeq2 2397	. . . . . . . . . . . . . . . . . 18
62	61	biimprd 223	. . . . . . . . . . . . . . . . 17
63	60, 62	syl6 33	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
64	63	impd 429	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
65	55, 64	syl5bi 217	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
66	52, 65	syl5bi 217	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	66	3expa 1194	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
68	67	rexlimdvva 2881	. . . . . . . . . . 11 $/\$ $/\$
69	50, 68	sylbid 215	. . . . . . . . . 10 $/\$ $/\$
70	69	alrimiv 1727	. . . . . . . . 9 $/\$ $/\$
71		mo2icl 3203	. . . . . . . . 9
72	70, 71	syl 16	. . . . . . . 8 $/\$ $/\$
73	72	ralrimivva 2803	. . . . . . 7
74		fofn 5705	. . . . . . . . . 10
75	13, 74	syl 16	. . . . . . . . 9
76		opeq2 4132	. . . . . . . . . . . 12
77	76	breq1d 4377	. . . . . . . . . . 11
78	77	mobidv 2241	. . . . . . . . . 10
79	78	ralrn 5936	. . . . . . . . 9
80	75, 79	syl 16	. . . . . . . 8
81	80	ralbidv 2821	. . . . . . 7
82	73, 81	mpbird 232	. . . . . 6
83		opeq1 4131	. . . . . . . . . . 11
84	83	breq1d 4377	. . . . . . . . . 10
85	84	mobidv 2241	. . . . . . . . 9
86	85	ralbidv 2821	. . . . . . . 8
87	86	ralrn 5936	. . . . . . 7
88	75, 87	syl 16	. . . . . 6
89	82, 88	mpbird 232	. . . . 5
90		breq1 4370	. . . . . . 7
91	90	mobidv 2241	. . . . . 6
92	91	ralxp 5057	. . . . 5
93	89, 92	sylibr 212	. . . 4
94		ssralv 3478	. . . 4
95	42, 93, 94	sylc 60	. . 3
96		dffun7 5522	. . 3 $/\$
97	12, 95, 96	sylanbrc 662	. 2
98		eqimss2 3470	. . . . . . . . . . 11
99	10, 98	syl 16	. . . . . . . . . 10
100		iunss 4284	. . . . . . . . . 10
101	99, 100	sylib 196	. . . . . . . . 9
102		iunss 4284	. . . . . . . . . . 11
103		opex 4626	. . . . . . . . . . . . . 14
104	103	snss 4068	. . . . . . . . . . . . 13
105	1, 2	opeldm 5119	. . . . . . . . . . . . 13
106	104, 105	sylbir 213	. . . . . . . . . . . 12
107	106	ralimi 2775	. . . . . . . . . . 11
108	102, 107	sylbi 195	. . . . . . . . . 10
109	108	ralimi 2775	. . . . . . . . 9
110	101, 109	syl 16	. . . . . . . 8
111		opeq2 4132	. . . . . . . . . . . 12
112	111	eleq1d 2451	. . . . . . . . . . 11
113	112	ralrn 5936	. . . . . . . . . 10
114	75, 113	syl 16	. . . . . . . . 9
115	114	ralbidv 2821	. . . . . . . 8
116	110, 115	mpbird 232	. . . . . . 7
117		opeq1 4131	. . . . . . . . . . 11
118	117	eleq1d 2451	. . . . . . . . . 10
119	118	ralbidv 2821	. . . . . . . . 9
120	119	ralrn 5936	. . . . . . . 8
121	75, 120	syl 16	. . . . . . 7
122	116, 121	mpbird 232	. . . . . 6
123		eleq1 2454	. . . . . . 7
124	123	ralxp 5057	. . . . . 6
125	122, 124	sylibr 212	. . . . 5
126		dfss3 3407	. . . . 5
127	125, 126	sylibr 212	. . . 4
128	41, 127	eqsstr3d 3452	. . 3
129	38, 128	eqssd 3434	. 2
130		df-fn 5499	. 2 $/\$
131	97, 129, 130	sylanbrc 662	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wal 1397

wceq 1399

wcel 1826

wmo 2219

wne 2577

wral 2732

wrex 2733

cvv 3034

wss 3389

c0 3711

csn 3944

cop 3950

ciun 4243 class class class wbr 4367

cxp 4911

cdm 4913

crn 4914

wrel 4918

wfun 5490

wfn 5491

wf 5492

wfo 5494

cfv 5496 (class class class)co 6196

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-sep 4488 ax-nul 4496 ax-pr 4601

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-ral 2737 df-rex 2738 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-nul 3712 df-if 3858 df-sn 3945 df-pr 3947 df-op 3951 df-uni 4164 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-id 4709 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-fo 5502 df-fv 5504

This theorem is referenced by: imasaddvallem 14936 imasaddflem 14937 imasaddfn 14938 imasmulfn 14941

W3C validator