ofoaf

Description: Addition operator for functions from sets into power of omega results in a function from the intersection of sets to that power of omega. (Contributed by RP, 5-Jan-2025)

		Ref	Expression
	Assertion	ofoaf	$⊢ ((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E = ω ↑_{𝑜} D)) \to ({\circ_{f} +_{𝑜} ↾}_{((E^{A}) \times (E^{B}))}) : (E^{A}) \times (E^{B}) ⟶ E^{C}$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to E = ω ↑_{𝑜} D$
2		omelon	$⊢ ω \in On$
3		simpl	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to D \in On$
4		oecl	$⊢ (ω \in On \land D \in On) \to ω ↑_{𝑜} D \in On$
5	2 3 4	sylancr	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to ω ↑_{𝑜} D \in On$
6	1 5	eqeltrd	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to E \in On$
7	3 2	jctil	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to (ω \in On \land D \in On)$
8		peano1	$⊢ \emptyset \in ω$
9		oen0	$⊢ ((ω \in On \land D \in On) \land \emptyset \in ω) \to \emptyset \in (ω ↑_{𝑜} D)$
10	7 8 9	sylancl	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to \emptyset \in (ω ↑_{𝑜} D)$
11	10 1	eleqtrrd	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to \emptyset \in E$
12		oveq1	$⊢ x = \emptyset \to x +_{𝑜} E = \emptyset +_{𝑜} E$
13	12	sseq2d	$⊢ x = \emptyset \to (E \subseteq x +_{𝑜} E \leftrightarrow E \subseteq \emptyset +_{𝑜} E)$
14	13	adantl	$⊢ ((D \in On \land E = ω ↑_{𝑜} D) \land x = \emptyset) \to (E \subseteq x +_{𝑜} E \leftrightarrow E \subseteq \emptyset +_{𝑜} E)$
15		oa0r	$⊢ E \in On \to \emptyset +_{𝑜} E = E$
16	6 15	syl	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to \emptyset +_{𝑜} E = E$
17		ssid	$⊢ \emptyset +_{𝑜} E \subseteq \emptyset +_{𝑜} E$
18	16 17	eqsstrrdi	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to E \subseteq \emptyset +_{𝑜} E$
19	11 14 18	rspcedvd	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to \exists x \in E E \subseteq x +_{𝑜} E$
20		ssiun	$⊢ \exists x \in E E \subseteq x +_{𝑜} E \to E \subseteq ⋃_{x \in E} (x +_{𝑜} E)$
21	19 20	syl	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to E \subseteq ⋃_{x \in E} (x +_{𝑜} E)$
22	1	eleq2d	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to (x \in E \leftrightarrow x \in (ω ↑_{𝑜} D))$
23	22	biimpa	$⊢ ((D \in On \land E = ω ↑_{𝑜} D) \land x \in E) \to x \in (ω ↑_{𝑜} D)$
24	6	adantr	$⊢ ((D \in On \land E = ω ↑_{𝑜} D) \land x \in E) \to E \in On$
25	1	adantr	$⊢ ((D \in On \land E = ω ↑_{𝑜} D) \land x \in E) \to E = ω ↑_{𝑜} D$
26		ssid	$⊢ E \subseteq E$
27	25 26	eqsstrrdi	$⊢ ((D \in On \land E = ω ↑_{𝑜} D) \land x \in E) \to ω ↑_{𝑜} D \subseteq E$
28		oaabs2	$⊢ ((x \in (ω ↑_{𝑜} D) \land E \in On) \land ω ↑_{𝑜} D \subseteq E) \to x +_{𝑜} E = E$
29	23 24 27 28	syl21anc	$⊢ ((D \in On \land E = ω ↑_{𝑜} D) \land x \in E) \to x +_{𝑜} E = E$
30	29 26	eqsstrdi	$⊢ ((D \in On \land E = ω ↑_{𝑜} D) \land x \in E) \to x +_{𝑜} E \subseteq E$
31	30	iunssd	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to ⋃_{x \in E} (x +_{𝑜} E) \subseteq E$
32	21 31	eqssd	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to E = ⋃_{x \in E} (x +_{𝑜} E)$
33	6 6 32	3jca	$⊢ (D \in On \land E = ω ↑_{𝑜} D) \to (E \in On \land E \in On \land E = ⋃_{x \in E} (x +_{𝑜} E))$
34		ofoafg	$⊢ ((A \in V \land B \in W \land C = A \cap B) \land (E \in On \land E \in On \land E = ⋃_{x \in E} (x +_{𝑜} E))) \to ({\circ_{f} +_{𝑜} ↾}_{((E^{A}) \times (E^{B}))}) : (E^{A}) \times (E^{B}) ⟶ E^{C}$
35	33 34	sylan2	$⊢ ((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E = ω ↑_{𝑜} D)) \to ({\circ_{f} +_{𝑜} ↾}_{((E^{A}) \times (E^{B}))}) : (E^{A}) \times (E^{B}) ⟶ E^{C}$

Metamath Proof Explorer

Theorem ofoaf

Proof