oaf1o

Description: Left addition by a constant is a bijection from ordinals to ordinals greater than the constant. (Contributed by Mario Carneiro, 30-May-2015)

		Ref	Expression
	Assertion	oaf1o	$⊢ A \in On \to (x \in On ⟼ A +_{𝑜} x) : On \underset{1-1 onto}{⟶} On ∖ A$

Proof

Step	Hyp	Ref	Expression
1		oacl	$⊢ (A \in On \land x \in On) \to A +_{𝑜} x \in On$
2		oaword1	$⊢ (A \in On \land x \in On) \to A \subseteq A +_{𝑜} x$
3		ontri1	$⊢ (A \in On \land A +_{𝑜} x \in On) \to (A \subseteq A +_{𝑜} x \leftrightarrow \neg A +_{𝑜} x \in A)$
4	1 3	syldan	$⊢ (A \in On \land x \in On) \to (A \subseteq A +_{𝑜} x \leftrightarrow \neg A +_{𝑜} x \in A)$
5	2 4	mpbid	$⊢ (A \in On \land x \in On) \to \neg A +_{𝑜} x \in A$
6	1 5	eldifd	$⊢ (A \in On \land x \in On) \to A +_{𝑜} x \in (On ∖ A)$
7	6	ralrimiva	$⊢ A \in On \to \forall x \in On A +_{𝑜} x \in (On ∖ A)$
8		simpl	$⊢ (A \in On \land y \in (On ∖ A)) \to A \in On$
9		eldifi	$⊢ y \in (On ∖ A) \to y \in On$
10	9	adantl	$⊢ (A \in On \land y \in (On ∖ A)) \to y \in On$
11		eldifn	$⊢ y \in (On ∖ A) \to \neg y \in A$
12	11	adantl	$⊢ (A \in On \land y \in (On ∖ A)) \to \neg y \in A$
13		ontri1	$⊢ (A \in On \land y \in On) \to (A \subseteq y \leftrightarrow \neg y \in A)$
14	10 13	syldan	$⊢ (A \in On \land y \in (On ∖ A)) \to (A \subseteq y \leftrightarrow \neg y \in A)$
15	12 14	mpbird	$⊢ (A \in On \land y \in (On ∖ A)) \to A \subseteq y$
16		oawordeu	$⊢ ((A \in On \land y \in On) \land A \subseteq y) \to \exists! x \in On A +_{𝑜} x = y$
17	8 10 15 16	syl21anc	$⊢ (A \in On \land y \in (On ∖ A)) \to \exists! x \in On A +_{𝑜} x = y$
18		eqcom	$⊢ A +_{𝑜} x = y \leftrightarrow y = A +_{𝑜} x$
19	18	reubii	$⊢ \exists! x \in On A +_{𝑜} x = y \leftrightarrow \exists! x \in On y = A +_{𝑜} x$
20	17 19	sylib	$⊢ (A \in On \land y \in (On ∖ A)) \to \exists! x \in On y = A +_{𝑜} x$
21	20	ralrimiva	$⊢ A \in On \to \forall y \in (On ∖ A) \exists! x \in On y = A +_{𝑜} x$
22		eqid	$⊢ (x \in On ⟼ A +_{𝑜} x) = (x \in On ⟼ A +_{𝑜} x)$
23	22	f1ompt	$⊢ (x \in On ⟼ A +_{𝑜} x) : On \underset{1-1 onto}{⟶} On ∖ A \leftrightarrow (\forall x \in On A +_{𝑜} x \in (On ∖ A) \land \forall y \in (On ∖ A) \exists! x \in On y = A +_{𝑜} x)$
24	7 21 23	sylanbrc	$⊢ A \in On \to (x \in On ⟼ A +_{𝑜} x) : On \underset{1-1 onto}{⟶} On ∖ A$

Metamath Proof Explorer

Theorem oaf1o

Proof