nnaordex2

Description: Equivalence for ordering. (Contributed by Scott Fenton, 18-Apr-2025)

		Ref	Expression
	Assertion	nnaordex2	$⊢ (A \in ω \land B \in ω) \to (A \in B \leftrightarrow \exists x \in ω A +_{𝑜} suc x = B)$

Proof

Step	Hyp	Ref	Expression
1		nnaordex	$⊢ (A \in ω \land B \in ω) \to (A \in B \leftrightarrow \exists y \in ω (\emptyset \in y \land A +_{𝑜} y = B))$
2		nn0suc	$⊢ y \in ω \to (y = \emptyset \lor \exists x \in ω y = suc x)$
3	2	ad2antrl	$⊢ ((A \in ω \land B \in ω) \land (y \in ω \land (\emptyset \in y \land A +_{𝑜} y = B))) \to (y = \emptyset \lor \exists x \in ω y = suc x)$
4		simprrl	$⊢ ((A \in ω \land B \in ω) \land (y \in ω \land (\emptyset \in y \land A +_{𝑜} y = B))) \to \emptyset \in y$
5		n0i	$⊢ \emptyset \in y \to \neg y = \emptyset$
6	4 5	syl	$⊢ ((A \in ω \land B \in ω) \land (y \in ω \land (\emptyset \in y \land A +_{𝑜} y = B))) \to \neg y = \emptyset$
7	3 6	orcnd	$⊢ ((A \in ω \land B \in ω) \land (y \in ω \land (\emptyset \in y \land A +_{𝑜} y = B))) \to \exists x \in ω y = suc x$
8		simprrr	$⊢ ((A \in ω \land B \in ω) \land (y \in ω \land (\emptyset \in y \land A +_{𝑜} y = B))) \to A +_{𝑜} y = B$
9		oveq2	$⊢ y = suc x \to A +_{𝑜} y = A +_{𝑜} suc x$
10	9	eqeq1d	$⊢ y = suc x \to (A +_{𝑜} y = B \leftrightarrow A +_{𝑜} suc x = B)$
11	8 10	syl5ibcom	$⊢ ((A \in ω \land B \in ω) \land (y \in ω \land (\emptyset \in y \land A +_{𝑜} y = B))) \to (y = suc x \to A +_{𝑜} suc x = B)$
12	11	reximdv	$⊢ ((A \in ω \land B \in ω) \land (y \in ω \land (\emptyset \in y \land A +_{𝑜} y = B))) \to (\exists x \in ω y = suc x \to \exists x \in ω A +_{𝑜} suc x = B)$
13	7 12	mpd	$⊢ ((A \in ω \land B \in ω) \land (y \in ω \land (\emptyset \in y \land A +_{𝑜} y = B))) \to \exists x \in ω A +_{𝑜} suc x = B$
14	13	rexlimdvaa	$⊢ (A \in ω \land B \in ω) \to (\exists y \in ω (\emptyset \in y \land A +_{𝑜} y = B) \to \exists x \in ω A +_{𝑜} suc x = B)$
15		peano2	$⊢ x \in ω \to suc x \in ω$
16	15	ad2antrl	$⊢ ((A \in ω \land B \in ω) \land (x \in ω \land A +_{𝑜} suc x = B)) \to suc x \in ω$
17		nnord	$⊢ x \in ω \to Ord x$
18	17	ad2antrl	$⊢ ((A \in ω \land B \in ω) \land (x \in ω \land A +_{𝑜} suc x = B)) \to Ord x$
19		0elsuc	$⊢ Ord x \to \emptyset \in suc x$
20	18 19	syl	$⊢ ((A \in ω \land B \in ω) \land (x \in ω \land A +_{𝑜} suc x = B)) \to \emptyset \in suc x$
21		simprr	$⊢ ((A \in ω \land B \in ω) \land (x \in ω \land A +_{𝑜} suc x = B)) \to A +_{𝑜} suc x = B$
22		eleq2	$⊢ y = suc x \to (\emptyset \in y \leftrightarrow \emptyset \in suc x)$
23	22 10	anbi12d	$⊢ y = suc x \to ((\emptyset \in y \land A +_{𝑜} y = B) \leftrightarrow (\emptyset \in suc x \land A +_{𝑜} suc x = B))$
24	23	rspcev	$⊢ (suc x \in ω \land (\emptyset \in suc x \land A +_{𝑜} suc x = B)) \to \exists y \in ω (\emptyset \in y \land A +_{𝑜} y = B)$
25	16 20 21 24	syl12anc	$⊢ ((A \in ω \land B \in ω) \land (x \in ω \land A +_{𝑜} suc x = B)) \to \exists y \in ω (\emptyset \in y \land A +_{𝑜} y = B)$
26	25	rexlimdvaa	$⊢ (A \in ω \land B \in ω) \to (\exists x \in ω A +_{𝑜} suc x = B \to \exists y \in ω (\emptyset \in y \land A +_{𝑜} y = B))$
27	14 26	impbid	$⊢ (A \in ω \land B \in ω) \to (\exists y \in ω (\emptyset \in y \land A +_{𝑜} y = B) \leftrightarrow \exists x \in ω A +_{𝑜} suc x = B)$
28	1 27	bitrd	$⊢ (A \in ω \land B \in ω) \to (A \in B \leftrightarrow \exists x \in ω A +_{𝑜} suc x = B)$

Metamath Proof Explorer

Theorem nnaordex2

Proof