nnaordex

Description: Equivalence for ordering. Compare Exercise 23 of Enderton p. 88. (Contributed by NM, 5-Dec-1995) (Revised by Mario Carneiro, 15-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		nnon	$⊢ B \in ω \to B \in On$
2	1	adantl	$⊢ (A \in ω \land B \in ω) \to B \in On$
3		onelss	$⊢ B \in On \to (A \in B \to A \subseteq B)$
4	2 3	syl	$⊢ (A \in ω \land B \in ω) \to (A \in B \to A \subseteq B)$
5		nnawordex	$⊢ (A \in ω \land B \in ω) \to (A \subseteq B \leftrightarrow \exists x \in ω A +_{𝑜} x = B)$
6	4 5	sylibd	$⊢ (A \in ω \land B \in ω) \to (A \in B \to \exists x \in ω A +_{𝑜} x = B)$
7		simplr	$⊢ ((A \in ω \land A \in B) \land x \in ω) \to A \in B$
8		eleq2	$⊢ A +_{𝑜} x = B \to (A \in (A +_{𝑜} x) \leftrightarrow A \in B)$
9	7 8	syl5ibrcom	$⊢ ((A \in ω \land A \in B) \land x \in ω) \to (A +_{𝑜} x = B \to A \in (A +_{𝑜} x))$
10		peano1	$⊢ \emptyset \in ω$
11		nnaord	$⊢ (\emptyset \in ω \land x \in ω \land A \in ω) \to (\emptyset \in x \leftrightarrow A +_{𝑜} \emptyset \in (A +_{𝑜} x))$
12	10 11	mp3an1	$⊢ (x \in ω \land A \in ω) \to (\emptyset \in x \leftrightarrow A +_{𝑜} \emptyset \in (A +_{𝑜} x))$
13	12	ancoms	$⊢ (A \in ω \land x \in ω) \to (\emptyset \in x \leftrightarrow A +_{𝑜} \emptyset \in (A +_{𝑜} x))$
14		nna0	$⊢ A \in ω \to A +_{𝑜} \emptyset = A$
15	14	adantr	$⊢ (A \in ω \land x \in ω) \to A +_{𝑜} \emptyset = A$
16	15	eleq1d	$⊢ (A \in ω \land x \in ω) \to (A +_{𝑜} \emptyset \in (A +_{𝑜} x) \leftrightarrow A \in (A +_{𝑜} x))$
17	13 16	bitrd	$⊢ (A \in ω \land x \in ω) \to (\emptyset \in x \leftrightarrow A \in (A +_{𝑜} x))$
18	17	adantlr	$⊢ ((A \in ω \land A \in B) \land x \in ω) \to (\emptyset \in x \leftrightarrow A \in (A +_{𝑜} x))$
19	9 18	sylibrd	$⊢ ((A \in ω \land A \in B) \land x \in ω) \to (A +_{𝑜} x = B \to \emptyset \in x)$
20	19	ancrd	$⊢ ((A \in ω \land A \in B) \land x \in ω) \to (A +_{𝑜} x = B \to (\emptyset \in x \land A +_{𝑜} x = B))$
21	20	reximdva	$⊢ (A \in ω \land A \in B) \to (\exists x \in ω A +_{𝑜} x = B \to \exists x \in ω (\emptyset \in x \land A +_{𝑜} x = B))$
22	21	ex	$⊢ A \in ω \to (A \in B \to (\exists x \in ω A +_{𝑜} x = B \to \exists x \in ω (\emptyset \in x \land A +_{𝑜} x = B)))$
23	22	adantr	$⊢ (A \in ω \land B \in ω) \to (A \in B \to (\exists x \in ω A +_{𝑜} x = B \to \exists x \in ω (\emptyset \in x \land A +_{𝑜} x = B)))$
24	6 23	mpdd	$⊢ (A \in ω \land B \in ω) \to (A \in B \to \exists x \in ω (\emptyset \in x \land A +_{𝑜} x = B))$
25	17	biimpa	$⊢ ((A \in ω \land x \in ω) \land \emptyset \in x) \to A \in (A +_{𝑜} x)$
26	25 8	syl5ibcom	$⊢ ((A \in ω \land x \in ω) \land \emptyset \in x) \to (A +_{𝑜} x = B \to A \in B)$
27	26	expimpd	$⊢ (A \in ω \land x \in ω) \to ((\emptyset \in x \land A +_{𝑜} x = B) \to A \in B)$
28	27	rexlimdva	$⊢ A \in ω \to (\exists x \in ω (\emptyset \in x \land A +_{𝑜} x = B) \to A \in B)$
29	28	adantr	$⊢ (A \in ω \land B \in ω) \to (\exists x \in ω (\emptyset \in x \land A +_{𝑜} x = B) \to A \in B)$
30	24 29	impbid	$⊢ (A \in ω \land B \in ω) \to (A \in B \leftrightarrow \exists x \in ω (\emptyset \in x \land A +_{𝑜} x = B))$

Metamath Proof Explorer

Theorem nnaordex

Proof