ofoafo

Description: Addition operator for functions from a set into a power of omega is an onto binary operator. (Contributed by RP, 5-Jan-2025)

		Ref	Expression
	Assertion	ofoafo	$⊢ (A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \to ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) : (C^{A}) \times (C^{A}) \underset{onto}{⟶} C^{A}$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ A \in V \to A \in V$
2		inidm	$⊢ A \cap A = A$
3	2	eqcomi	$⊢ A = A \cap A$
4	3	a1i	$⊢ A \in V \to A = A \cap A$
5	1 1 4	3jca	$⊢ A \in V \to (A \in V \land A \in V \land A = A \cap A)$
6		ofoaf	$⊢ ((A \in V \land A \in V \land A = A \cap A) \land (B \in On \land C = ω ↑_{𝑜} B)) \to ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) : (C^{A}) \times (C^{A}) ⟶ C^{A}$
7	5 6	sylan	$⊢ (A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \to ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) : (C^{A}) \times (C^{A}) ⟶ C^{A}$
8		simpr	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land h \in (C^{A})) \to h \in (C^{A})$
9		omelon	$⊢ ω \in On$
10	9	a1i	$⊢ (B \in On \land C = ω ↑_{𝑜} B) \to ω \in On$
11		simpl	$⊢ (B \in On \land C = ω ↑_{𝑜} B) \to B \in On$
12	10 11	jca	$⊢ (B \in On \land C = ω ↑_{𝑜} B) \to (ω \in On \land B \in On)$
13		peano1	$⊢ \emptyset \in ω$
14		oen0	$⊢ ((ω \in On \land B \in On) \land \emptyset \in ω) \to \emptyset \in (ω ↑_{𝑜} B)$
15	12 13 14	sylancl	$⊢ (B \in On \land C = ω ↑_{𝑜} B) \to \emptyset \in (ω ↑_{𝑜} B)$
16		simpr	$⊢ (B \in On \land C = ω ↑_{𝑜} B) \to C = ω ↑_{𝑜} B$
17	15 16	eleqtrrd	$⊢ (B \in On \land C = ω ↑_{𝑜} B) \to \emptyset \in C$
18		fconst6g	$⊢ \emptyset \in C \to (A \times \{\emptyset\}) : A ⟶ C$
19	17 18	syl	$⊢ (B \in On \land C = ω ↑_{𝑜} B) \to (A \times \{\emptyset\}) : A ⟶ C$
20	19	adantl	$⊢ (A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \to (A \times \{\emptyset\}) : A ⟶ C$
21		oecl	$⊢ (ω \in On \land B \in On) \to ω ↑_{𝑜} B \in On$
22	9 11 21	sylancr	$⊢ (B \in On \land C = ω ↑_{𝑜} B) \to ω ↑_{𝑜} B \in On$
23	16 22	eqeltrd	$⊢ (B \in On \land C = ω ↑_{𝑜} B) \to C \in On$
24	23	adantl	$⊢ (A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \to C \in On$
25		simpl	$⊢ (A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \to A \in V$
26	24 25	elmapd	$⊢ (A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \to (A \times \{\emptyset\} \in (C^{A}) \leftrightarrow (A \times \{\emptyset\}) : A ⟶ C)$
27	20 26	mpbird	$⊢ (A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \to A \times \{\emptyset\} \in (C^{A})$
28	27	adantr	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land h \in (C^{A})) \to A \times \{\emptyset\} \in (C^{A})$
29		ovres	$⊢ (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A})) \to h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) (A \times \{\emptyset\}) = h {+_{𝑜}}_{f} (A \times \{\emptyset\})$
30	29	adantl	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \to h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) (A \times \{\emptyset\}) = h {+_{𝑜}}_{f} (A \times \{\emptyset\})$
31		elmapi	$⊢ h \in (C^{A}) \to h : A ⟶ C$
32	31	adantr	$⊢ (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A})) \to h : A ⟶ C$
33	32	ffnd	$⊢ (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A})) \to h Fn A$
34	33	adantl	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \to h Fn A$
35		elmapi	$⊢ A \times \{\emptyset\} \in (C^{A}) \to (A \times \{\emptyset\}) : A ⟶ C$
36	35	adantl	$⊢ (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A})) \to (A \times \{\emptyset\}) : A ⟶ C$
37	36	ffnd	$⊢ (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A})) \to (A \times \{\emptyset\}) Fn A$
38	37	adantl	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \to (A \times \{\emptyset\}) Fn A$
39	25	adantr	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \to A \in V$
40	34 38 39 39 2	offn	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \to (h {+_{𝑜}}_{f} (A \times \{\emptyset\})) Fn A$
41		elmapfn	$⊢ h \in (C^{A}) \to h Fn A$
42		elmapfn	$⊢ A \times \{\emptyset\} \in (C^{A}) \to (A \times \{\emptyset\}) Fn A$
43	41 42	anim12i	$⊢ (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A})) \to (h Fn A \land (A \times \{\emptyset\}) Fn A)$
44	43	adantl	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \to (h Fn A \land (A \times \{\emptyset\}) Fn A)$
45	39	anim1i	$⊢ (((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \land a \in A) \to (A \in V \land a \in A)$
46		fnfvof	$⊢ ((h Fn A \land (A \times \{\emptyset\}) Fn A) \land (A \in V \land a \in A)) \to (h {+_{𝑜}}_{f} (A \times \{\emptyset\})) (a) = h (a) +_{𝑜} (A \times \{\emptyset\}) (a)$
47	44 45 46	syl2an2r	$⊢ (((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \land a \in A) \to (h {+_{𝑜}}_{f} (A \times \{\emptyset\})) (a) = h (a) +_{𝑜} (A \times \{\emptyset\}) (a)$
48		simpr	$⊢ (((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \land a \in A) \to a \in A$
49		fvconst2g	$⊢ (\emptyset \in ω \land a \in A) \to (A \times \{\emptyset\}) (a) = \emptyset$
50	13 48 49	sylancr	$⊢ (((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \land a \in A) \to (A \times \{\emptyset\}) (a) = \emptyset$
51	50	oveq2d	$⊢ (((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \land a \in A) \to h (a) +_{𝑜} (A \times \{\emptyset\}) (a) = h (a) +_{𝑜} \emptyset$
52	24	adantr	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \to C \in On$
53	52	adantr	$⊢ (((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \land a \in A) \to C \in On$
54		onss	$⊢ C \in On \to C \subseteq On$
55	53 54	syl	$⊢ (((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \land a \in A) \to C \subseteq On$
56	31	ad2antrl	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \to h : A ⟶ C$
57	56	ffvelcdmda	$⊢ (((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \land a \in A) \to h (a) \in C$
58	55 57	sseldd	$⊢ (((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \land a \in A) \to h (a) \in On$
59		oa0	$⊢ h (a) \in On \to h (a) +_{𝑜} \emptyset = h (a)$
60	58 59	syl	$⊢ (((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \land a \in A) \to h (a) +_{𝑜} \emptyset = h (a)$
61	47 51 60	3eqtrd	$⊢ (((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \land a \in A) \to (h {+_{𝑜}}_{f} (A \times \{\emptyset\})) (a) = h (a)$
62	40 34 61	eqfnfvd	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \to h {+_{𝑜}}_{f} (A \times \{\emptyset\}) = h$
63	30 62	eqtr2d	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (h \in (C^{A}) \land A \times \{\emptyset\} \in (C^{A}))) \to h = h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) (A \times \{\emptyset\})$
64	63	expr	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land h \in (C^{A})) \to (A \times \{\emptyset\} \in (C^{A}) \to h = h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) (A \times \{\emptyset\}))$
65	28 64	jcai	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land h \in (C^{A})) \to (A \times \{\emptyset\} \in (C^{A}) \land h = h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) (A \times \{\emptyset\}))$
66		oveq2	$⊢ z = A \times \{\emptyset\} \to h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z = h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) (A \times \{\emptyset\})$
67	66	rspceeqv	$⊢ (A \times \{\emptyset\} \in (C^{A}) \land h = h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) (A \times \{\emptyset\})) \to \exists z \in (C^{A}) h = h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z$
68	65 67	syl	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land h \in (C^{A})) \to \exists z \in (C^{A}) h = h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z$
69	8 68	jca	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land h \in (C^{A})) \to (h \in (C^{A}) \land \exists z \in (C^{A}) h = h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z)$
70		oveq1	$⊢ f = h \to f ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z = h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z$
71	70	eqeq2d	$⊢ f = h \to (h = f ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z \leftrightarrow h = h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z)$
72	71	rexbidv	$⊢ f = h \to (\exists z \in (C^{A}) h = f ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z \leftrightarrow \exists z \in (C^{A}) h = h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z)$
73	72	rspcev	$⊢ (h \in (C^{A}) \land \exists z \in (C^{A}) h = h ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z) \to \exists f \in (C^{A}) \exists z \in (C^{A}) h = f ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z$
74	69 73	syl	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land h \in (C^{A})) \to \exists f \in (C^{A}) \exists z \in (C^{A}) h = f ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z$
75	74	ralrimiva	$⊢ (A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \to \forall h \in (C^{A}) \exists f \in (C^{A}) \exists z \in (C^{A}) h = f ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z$
76		foov	$⊢ ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) : (C^{A}) \times (C^{A}) \underset{onto}{⟶} C^{A} \leftrightarrow (({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) : (C^{A}) \times (C^{A}) ⟶ C^{A} \land \forall h \in (C^{A}) \exists f \in (C^{A}) \exists z \in (C^{A}) h = f ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) z)$
77	7 75 76	sylanbrc	$⊢ (A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \to ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) : (C^{A}) \times (C^{A}) \underset{onto}{⟶} C^{A}$

Metamath Proof Explorer

Theorem ofoafo

Proof