fresaun - Metamath Proof Explorer

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

Theorem fresaun 5766

Description: The union of two functions which agree on their common domain is a function. (Contributed by Stefan O'Rear, 9-Oct-2014.)

**Assertion**
Ref	Expression
fresaun	$/\$ $/\$

**Proof of Theorem fresaun**
Step	Hyp	Ref	Expression
1		simp1 1030	. . . 4 $/\$ $/\$
2		inss1 3643	. . . 4
3		fssres 5761	. . . 4 $/\$
4	1, 2, 3	sylancl 675	. . 3 $/\$ $/\$
5		difss 3549	. . . . 5 $\$
6		fssres 5761	. . . . 5 $/\$ $\$ $\$ $\$
7	1, 5, 6	sylancl 675	. . . 4 $/\$ $/\$ $\$ $\$
8		simp2 1031	. . . . 5 $/\$ $/\$
9		difss 3549	. . . . 5 $\$
10		fssres 5761	. . . . 5 $/\$ $\$ $\$ $\$
11	8, 9, 10	sylancl 675	. . . 4 $/\$ $/\$ $\$ $\$
12		indifdir 3690	. . . . . 6 $\$ $\$ $\$ $\$ $\$
13		disjdif 3830	. . . . . . 7 $\$
14	13	difeq1i 3536	. . . . . 6 $\$ $\$ $\$ $\$ $\$
15		0dif 3771	. . . . . 6 $\$ $\$
16	12, 14, 15	3eqtri 2497	. . . . 5 $\$ $\$
17	16	a1i 11	. . . 4 $/\$ $/\$ $\$ $\$
18		fun2 5759	. . . 4 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
19	7, 11, 17, 18	syl21anc 1291	. . 3 $/\$ $/\$ $\$ $\$ $\$ $\$
20		indi 3680	. . . . 5 $\$ $\$ $\$ $\$
21		inass 3633	. . . . . . 7 $\$ $\$
22		disjdif 3830	. . . . . . . 8 $\$
23	22	ineq2i 3622	. . . . . . 7 $\$
24		in0 3763	. . . . . . 7
25	21, 23, 24	3eqtri 2497	. . . . . 6 $\$
26		incom 3616	. . . . . . . 8
27	26	ineq1i 3621	. . . . . . 7 $\$ $\$
28		inass 3633	. . . . . . . 8 $\$ $\$
29	13	ineq2i 3622	. . . . . . . 8 $\$
30		in0 3763	. . . . . . . 8
31	28, 29, 30	3eqtri 2497	. . . . . . 7 $\$
32	27, 31	eqtri 2493	. . . . . 6 $\$
33	25, 32	uneq12i 3577	. . . . 5 $\$ $\$
34		un0 3762	. . . . 5
35	20, 33, 34	3eqtri 2497	. . . 4 $\$ $\$
36	35	a1i 11	. . 3 $/\$ $/\$ $\$ $\$
37		fun2 5759	. . 3 $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
38	4, 19, 36, 37	syl21anc 1291	. 2 $/\$ $/\$ $\$ $\$ $\$ $\$
39		ffn 5739	. . . . 5
40		ffn 5739	. . . . 5
41		id 22	. . . . 5
42		resasplit 5765	. . . . 5 $/\$ $/\$ $\$ $\$
43	39, 40, 41, 42	syl3an 1334	. . . 4 $/\$ $/\$ $\$ $\$
44	43	feq1d 5724	. . 3 $/\$ $/\$ $\$ $\$
45		un12 3583	. . . . 5 $\$ $\$ $\$ $\$
46	26	uneq1i 3575	. . . . . . 7 $\$ $\$
47		inundif 3836	. . . . . . 7 $\$
48	46, 47	eqtri 2493	. . . . . 6 $\$
49	48	uneq2i 3576	. . . . 5 $\$ $\$ $\$
50		undif1 3833	. . . . 5 $\$
51	45, 49, 50	3eqtri 2497	. . . 4 $\$ $\$
52	51	feq2i 5731	. . 3 $\$ $\$ $\$ $\$ $\$ $\$
53	44, 52	syl6rbbr 272	. 2 $/\$ $/\$ $\$ $\$ $\$ $\$
54	38, 53	mpbid 215	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ w3a 1007

wceq 1452 $\$ cdif 3387

cun 3388

cin 3389

wss 3390

c0 3722

cres 4841

wfn 5584

wf 5585

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pr 4639

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-rab 2765 df-v 3033 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-sn 3960 df-pr 3962 df-op 3966 df-br 4396 df-opab 4455 df-id 4754 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-fun 5591 df-fn 5592 df-f 5593

This theorem is referenced by: cvmliftlem10 30089 elmapresaun 35684

W3C validator