oadif1

Description: Express the set difference of an ordinal sum and its left addend as a class of sums. (Contributed by RP, 13-Feb-2025)

		Ref	Expression
	Assertion	oadif1	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B) ∖ A = \{x \| \exists b \in B x = A +_{𝑜} b\}$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in On \land B \in On) \to A \in On$
2		oacl	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B \in On$
3		onelon	$⊢ (A +_{𝑜} B \in On \land y \in (A +_{𝑜} B)) \to y \in On$
4	2 3	sylan	$⊢ ((A \in On \land B \in On) \land y \in (A +_{𝑜} B)) \to y \in On$
5		ontri1	$⊢ (A \in On \land y \in On) \to (A \subseteq y \leftrightarrow \neg y \in A)$
6	1 4 5	syl2an2r	$⊢ ((A \in On \land B \in On) \land y \in (A +_{𝑜} B)) \to (A \subseteq y \leftrightarrow \neg y \in A)$
7	6	pm5.32da	$⊢ (A \in On \land B \in On) \to ((y \in (A +_{𝑜} B) \land A \subseteq y) \leftrightarrow (y \in (A +_{𝑜} B) \land \neg y \in A))$
8		ancom	$⊢ (y \in (A +_{𝑜} B) \land A \subseteq y) \leftrightarrow (A \subseteq y \land y \in (A +_{𝑜} B))$
9	7 8	bitr3di	$⊢ (A \in On \land B \in On) \to ((y \in (A +_{𝑜} B) \land \neg y \in A) \leftrightarrow (A \subseteq y \land y \in (A +_{𝑜} B)))$
10		oawordex2	$⊢ ((A \in On \land B \in On) \land (A \subseteq y \land y \in (A +_{𝑜} B))) \to \exists b \in B A +_{𝑜} b = y$
11	9 10	sylbida	$⊢ ((A \in On \land B \in On) \land (y \in (A +_{𝑜} B) \land \neg y \in A)) \to \exists b \in B A +_{𝑜} b = y$
12		eqcom	$⊢ A +_{𝑜} b = y \leftrightarrow y = A +_{𝑜} b$
13	12	rexbii	$⊢ \exists b \in B A +_{𝑜} b = y \leftrightarrow \exists b \in B y = A +_{𝑜} b$
14	11 13	sylib	$⊢ ((A \in On \land B \in On) \land (y \in (A +_{𝑜} B) \land \neg y \in A)) \to \exists b \in B y = A +_{𝑜} b$
15	14	ex	$⊢ (A \in On \land B \in On) \to ((y \in (A +_{𝑜} B) \land \neg y \in A) \to \exists b \in B y = A +_{𝑜} b)$
16		simpr	$⊢ (((A \in On \land B \in On) \land b \in B) \land y = A +_{𝑜} b) \to y = A +_{𝑜} b$
17		oaordi	$⊢ (B \in On \land A \in On) \to (b \in B \to A +_{𝑜} b \in (A +_{𝑜} B))$
18	17	ancoms	$⊢ (A \in On \land B \in On) \to (b \in B \to A +_{𝑜} b \in (A +_{𝑜} B))$
19	18	imp	$⊢ ((A \in On \land B \in On) \land b \in B) \to A +_{𝑜} b \in (A +_{𝑜} B)$
20	19	adantr	$⊢ (((A \in On \land B \in On) \land b \in B) \land y = A +_{𝑜} b) \to A +_{𝑜} b \in (A +_{𝑜} B)$
21	16 20	eqeltrd	$⊢ (((A \in On \land B \in On) \land b \in B) \land y = A +_{𝑜} b) \to y \in (A +_{𝑜} B)$
22		simpr	$⊢ (A \in On \land B \in On) \to B \in On$
23		onelon	$⊢ (B \in On \land b \in B) \to b \in On$
24	22 23	sylan	$⊢ ((A \in On \land B \in On) \land b \in B) \to b \in On$
25		oaword1	$⊢ (A \in On \land b \in On) \to A \subseteq A +_{𝑜} b$
26	1 24 25	syl2an2r	$⊢ ((A \in On \land B \in On) \land b \in B) \to A \subseteq A +_{𝑜} b$
27		oacl	$⊢ (A \in On \land b \in On) \to A +_{𝑜} b \in On$
28	1 24 27	syl2an2r	$⊢ ((A \in On \land B \in On) \land b \in B) \to A +_{𝑜} b \in On$
29		ontri1	$⊢ (A \in On \land A +_{𝑜} b \in On) \to (A \subseteq A +_{𝑜} b \leftrightarrow \neg A +_{𝑜} b \in A)$
30	1 28 29	syl2an2r	$⊢ ((A \in On \land B \in On) \land b \in B) \to (A \subseteq A +_{𝑜} b \leftrightarrow \neg A +_{𝑜} b \in A)$
31	26 30	mpbid	$⊢ ((A \in On \land B \in On) \land b \in B) \to \neg A +_{𝑜} b \in A$
32	31	adantr	$⊢ (((A \in On \land B \in On) \land b \in B) \land y = A +_{𝑜} b) \to \neg A +_{𝑜} b \in A$
33	16 32	eqneltrd	$⊢ (((A \in On \land B \in On) \land b \in B) \land y = A +_{𝑜} b) \to \neg y \in A$
34	21 33	jca	$⊢ (((A \in On \land B \in On) \land b \in B) \land y = A +_{𝑜} b) \to (y \in (A +_{𝑜} B) \land \neg y \in A)$
35	34	rexlimdva2	$⊢ (A \in On \land B \in On) \to (\exists b \in B y = A +_{𝑜} b \to (y \in (A +_{𝑜} B) \land \neg y \in A))$
36	15 35	impbid	$⊢ (A \in On \land B \in On) \to ((y \in (A +_{𝑜} B) \land \neg y \in A) \leftrightarrow \exists b \in B y = A +_{𝑜} b)$
37		eldif	$⊢ y \in ((A +_{𝑜} B) ∖ A) \leftrightarrow (y \in (A +_{𝑜} B) \land \neg y \in A)$
38		vex	$⊢ y \in V$
39		eqeq1	$⊢ x = y \to (x = A +_{𝑜} b \leftrightarrow y = A +_{𝑜} b)$
40	39	rexbidv	$⊢ x = y \to (\exists b \in B x = A +_{𝑜} b \leftrightarrow \exists b \in B y = A +_{𝑜} b)$
41	38 40	elab	$⊢ y \in \{x \| \exists b \in B x = A +_{𝑜} b\} \leftrightarrow \exists b \in B y = A +_{𝑜} b$
42	36 37 41	3bitr4g	$⊢ (A \in On \land B \in On) \to (y \in ((A +_{𝑜} B) ∖ A) \leftrightarrow y \in \{x \| \exists b \in B x = A +_{𝑜} b\})$
43	42	eqrdv	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B) ∖ A = \{x \| \exists b \in B x = A +_{𝑜} b\}$

Metamath Proof Explorer

Theorem oadif1

Proof