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 5754

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 1008	. . . 4 $/\$ $/\$
2		inss1 3652	. . . 4
3		fssres 5749	. . . 4 $/\$
4	1, 2, 3	sylancl 668	. . 3 $/\$ $/\$
5		difss 3560	. . . . 5 $\$
6		fssres 5749	. . . . 5 $/\$ $\$ $\$ $\$
7	1, 5, 6	sylancl 668	. . . 4 $/\$ $/\$ $\$ $\$
8		simp2 1009	. . . . 5 $/\$ $/\$
9		difss 3560	. . . . 5 $\$
10		fssres 5749	. . . . 5 $/\$ $\$ $\$ $\$
11	8, 9, 10	sylancl 668	. . . 4 $/\$ $/\$ $\$ $\$
12		indifdir 3699	. . . . . 6 $\$ $\$ $\$ $\$ $\$
13		disjdif 3839	. . . . . . 7 $\$
14	13	difeq1i 3547	. . . . . 6 $\$ $\$ $\$ $\$ $\$
15		0dif 3838	. . . . . 6 $\$ $\$
16	12, 14, 15	3eqtri 2477	. . . . 5 $\$ $\$
17	16	a1i 11	. . . 4 $/\$ $/\$ $\$ $\$
18		fun2 5747	. . . 4 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
19	7, 11, 17, 18	syl21anc 1267	. . 3 $/\$ $/\$ $\$ $\$ $\$ $\$
20		indi 3689	. . . . 5 $\$ $\$ $\$ $\$
21		inass 3642	. . . . . . 7 $\$ $\$
22		disjdif 3839	. . . . . . . 8 $\$
23	22	ineq2i 3631	. . . . . . 7 $\$
24		in0 3760	. . . . . . 7
25	21, 23, 24	3eqtri 2477	. . . . . 6 $\$
26		incom 3625	. . . . . . . 8
27	26	ineq1i 3630	. . . . . . 7 $\$ $\$
28		inass 3642	. . . . . . . 8 $\$ $\$
29	13	ineq2i 3631	. . . . . . . 8 $\$
30		in0 3760	. . . . . . . 8
31	28, 29, 30	3eqtri 2477	. . . . . . 7 $\$
32	27, 31	eqtri 2473	. . . . . 6 $\$
33	25, 32	uneq12i 3586	. . . . 5 $\$ $\$
34		un0 3759	. . . . 5
35	20, 33, 34	3eqtri 2477	. . . 4 $\$ $\$
36	35	a1i 11	. . 3 $/\$ $/\$ $\$ $\$
37		fun2 5747	. . 3 $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
38	4, 19, 36, 37	syl21anc 1267	. 2 $/\$ $/\$ $\$ $\$ $\$ $\$
39		ffn 5728	. . . . 5
40		ffn 5728	. . . . 5
41		id 22	. . . . 5
42		resasplit 5753	. . . . 5 $/\$ $/\$ $\$ $\$
43	39, 40, 41, 42	syl3an 1310	. . . 4 $/\$ $/\$ $\$ $\$
44	43	feq1d 5714	. . 3 $/\$ $/\$ $\$ $\$
45		un12 3592	. . . . 5 $\$ $\$ $\$ $\$
46	26	uneq1i 3584	. . . . . . 7 $\$ $\$
47		inundif 3845	. . . . . . 7 $\$
48	46, 47	eqtri 2473	. . . . . 6 $\$
49	48	uneq2i 3585	. . . . 5 $\$ $\$ $\$
50		undif1 3842	. . . . 5 $\$
51	45, 49, 50	3eqtri 2477	. . . 4 $\$ $\$
52	51	feq2i 5721	. . 3 $\$ $\$ $\$ $\$ $\$ $\$
53	44, 52	syl6rbbr 268	. 2 $/\$ $/\$ $\$ $\$ $\$ $\$
54	38, 53	mpbid 214	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ w3a 985

wceq 1444 $\$ cdif 3401

cun 3402

cin 3403

wss 3404

c0 3731

cres 4836

wfn 5577

wf 5578

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pr 4639

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3047 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-sn 3969 df-pr 3971 df-op 3975 df-br 4403 df-opab 4462 df-id 4749 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-fun 5584 df-fn 5585 df-f 5586

This theorem is referenced by: cvmliftlem10 30017 elmapresaun 35613

W3C validator