ofun

Description: A function operation of unions of disjoint functions is a union of function operations. (Contributed by SN, 16-Jun-2024)

	Ref	Expression
Hypotheses	ofun.a	$⊢ φ \to A Fn M$
	ofun.b	$⊢ φ \to B Fn M$
	ofun.c	$⊢ φ \to C Fn N$
	ofun.d	$⊢ φ \to D Fn N$
	ofun.m	$⊢ φ \to M \in V$
	ofun.n	$⊢ φ \to N \in W$
	ofun.1	$⊢ φ \to M \cap N = \emptyset$
Assertion	ofun	$⊢ φ \to (A \cup C) R_{f} (B \cup D) = (A R_{f} B) \cup (C R_{f} D)$

Proof

Step	Hyp	Ref	Expression
1		ofun.a	$⊢ φ \to A Fn M$
2		ofun.b	$⊢ φ \to B Fn M$
3		ofun.c	$⊢ φ \to C Fn N$
4		ofun.d	$⊢ φ \to D Fn N$
5		ofun.m	$⊢ φ \to M \in V$
6		ofun.n	$⊢ φ \to N \in W$
7		ofun.1	$⊢ φ \to M \cap N = \emptyset$
8	1 3 7	fnund	$⊢ φ \to (A \cup C) Fn (M \cup N)$
9	2 4 7	fnund	$⊢ φ \to (B \cup D) Fn (M \cup N)$
10	5 6	unexd	$⊢ φ \to M \cup N \in V$
11		inidm	$⊢ (M \cup N) \cap (M \cup N) = M \cup N$
12	8 9 10 10 11	offn	$⊢ φ \to ((A \cup C) R_{f} (B \cup D)) Fn (M \cup N)$
13		inidm	$⊢ M \cap M = M$
14	1 2 5 5 13	offn	$⊢ φ \to (A R_{f} B) Fn M$
15		inidm	$⊢ N \cap N = N$
16	3 4 6 6 15	offn	$⊢ φ \to (C R_{f} D) Fn N$
17	14 16 7	fnund	$⊢ φ \to ((A R_{f} B) \cup (C R_{f} D)) Fn (M \cup N)$
18		eqidd	$⊢ (φ \land x \in (M \cup N)) \to (A \cup C) (x) = (A \cup C) (x)$
19		eqidd	$⊢ (φ \land x \in (M \cup N)) \to (B \cup D) (x) = (B \cup D) (x)$
20	8 9 10 10 11 18 19	ofval	$⊢ (φ \land x \in (M \cup N)) \to ((A \cup C) R_{f} (B \cup D)) (x) = (A \cup C) (x) R (B \cup D) (x)$
21		elun	$⊢ x \in (M \cup N) \leftrightarrow (x \in M \lor x \in N)$
22		eqidd	$⊢ (φ \land x \in M) \to A (x) = A (x)$
23		eqidd	$⊢ (φ \land x \in M) \to B (x) = B (x)$
24	1 2 5 5 13 22 23	ofval	$⊢ (φ \land x \in M) \to (A R_{f} B) (x) = A (x) R B (x)$
25	14	adantr	$⊢ (φ \land x \in M) \to (A R_{f} B) Fn M$
26	16	adantr	$⊢ (φ \land x \in M) \to (C R_{f} D) Fn N$
27	7	adantr	$⊢ (φ \land x \in M) \to M \cap N = \emptyset$
28		simpr	$⊢ (φ \land x \in M) \to x \in M$
29	25 26 27 28	fvun1d	$⊢ (φ \land x \in M) \to ((A R_{f} B) \cup (C R_{f} D)) (x) = (A R_{f} B) (x)$
30	1	adantr	$⊢ (φ \land x \in M) \to A Fn M$
31	3	adantr	$⊢ (φ \land x \in M) \to C Fn N$
32	30 31 27 28	fvun1d	$⊢ (φ \land x \in M) \to (A \cup C) (x) = A (x)$
33	2	adantr	$⊢ (φ \land x \in M) \to B Fn M$
34	4	adantr	$⊢ (φ \land x \in M) \to D Fn N$
35	33 34 27 28	fvun1d	$⊢ (φ \land x \in M) \to (B \cup D) (x) = B (x)$
36	32 35	oveq12d	$⊢ (φ \land x \in M) \to (A \cup C) (x) R (B \cup D) (x) = A (x) R B (x)$
37	24 29 36	3eqtr4rd	$⊢ (φ \land x \in M) \to (A \cup C) (x) R (B \cup D) (x) = ((A R_{f} B) \cup (C R_{f} D)) (x)$
38		eqidd	$⊢ (φ \land x \in N) \to C (x) = C (x)$
39		eqidd	$⊢ (φ \land x \in N) \to D (x) = D (x)$
40	3 4 6 6 15 38 39	ofval	$⊢ (φ \land x \in N) \to (C R_{f} D) (x) = C (x) R D (x)$
41	14	adantr	$⊢ (φ \land x \in N) \to (A R_{f} B) Fn M$
42	16	adantr	$⊢ (φ \land x \in N) \to (C R_{f} D) Fn N$
43	7	adantr	$⊢ (φ \land x \in N) \to M \cap N = \emptyset$
44		simpr	$⊢ (φ \land x \in N) \to x \in N$
45	41 42 43 44	fvun2d	$⊢ (φ \land x \in N) \to ((A R_{f} B) \cup (C R_{f} D)) (x) = (C R_{f} D) (x)$
46	1	adantr	$⊢ (φ \land x \in N) \to A Fn M$
47	3	adantr	$⊢ (φ \land x \in N) \to C Fn N$
48	46 47 43 44	fvun2d	$⊢ (φ \land x \in N) \to (A \cup C) (x) = C (x)$
49	2	adantr	$⊢ (φ \land x \in N) \to B Fn M$
50	4	adantr	$⊢ (φ \land x \in N) \to D Fn N$
51	49 50 43 44	fvun2d	$⊢ (φ \land x \in N) \to (B \cup D) (x) = D (x)$
52	48 51	oveq12d	$⊢ (φ \land x \in N) \to (A \cup C) (x) R (B \cup D) (x) = C (x) R D (x)$
53	40 45 52	3eqtr4rd	$⊢ (φ \land x \in N) \to (A \cup C) (x) R (B \cup D) (x) = ((A R_{f} B) \cup (C R_{f} D)) (x)$
54	37 53	jaodan	$⊢ (φ \land (x \in M \lor x \in N)) \to (A \cup C) (x) R (B \cup D) (x) = ((A R_{f} B) \cup (C R_{f} D)) (x)$
55	21 54	sylan2b	$⊢ (φ \land x \in (M \cup N)) \to (A \cup C) (x) R (B \cup D) (x) = ((A R_{f} B) \cup (C R_{f} D)) (x)$
56	20 55	eqtrd	$⊢ (φ \land x \in (M \cup N)) \to ((A \cup C) R_{f} (B \cup D)) (x) = ((A R_{f} B) \cup (C R_{f} D)) (x)$
57	12 17 56	eqfnfvd	$⊢ φ \to (A \cup C) R_{f} (B \cup D) = (A R_{f} B) \cup (C R_{f} D)$

Metamath Proof Explorer

Theorem ofun

Proof