eldifsucnn

Description: Condition for membership in the difference of _om and a nonzero finite ordinal. (Contributed by Scott Fenton, 24-Oct-2024)

		Ref	Expression
	Assertion	eldifsucnn	$⊢ A \in ω \to (B \in (ω ∖ suc A) \leftrightarrow \exists x \in (ω ∖ A) B = suc x)$

Proof

Step	Hyp	Ref	Expression
1		peano2	$⊢ A \in ω \to suc A \in ω$
2		nnawordex	$⊢ (suc A \in ω \land B \in ω) \to (suc A \subseteq B \leftrightarrow \exists y \in ω suc A +_{𝑜} y = B)$
3	1 2	sylan	$⊢ (A \in ω \land B \in ω) \to (suc A \subseteq B \leftrightarrow \exists y \in ω suc A +_{𝑜} y = B)$
4		nnacl	$⊢ (A \in ω \land y \in ω) \to A +_{𝑜} y \in ω$
5		nnaword1	$⊢ (A \in ω \land y \in ω) \to A \subseteq A +_{𝑜} y$
6		nnasuc	$⊢ (y \in ω \land A \in ω) \to y +_{𝑜} suc A = suc (y +_{𝑜} A)$
7	6	ancoms	$⊢ (A \in ω \land y \in ω) \to y +_{𝑜} suc A = suc (y +_{𝑜} A)$
8		nnacom	$⊢ (suc A \in ω \land y \in ω) \to suc A +_{𝑜} y = y +_{𝑜} suc A$
9	1 8	sylan	$⊢ (A \in ω \land y \in ω) \to suc A +_{𝑜} y = y +_{𝑜} suc A$
10		nnacom	$⊢ (A \in ω \land y \in ω) \to A +_{𝑜} y = y +_{𝑜} A$
11		suceq	$⊢ A +_{𝑜} y = y +_{𝑜} A \to suc (A +_{𝑜} y) = suc (y +_{𝑜} A)$
12	10 11	syl	$⊢ (A \in ω \land y \in ω) \to suc (A +_{𝑜} y) = suc (y +_{𝑜} A)$
13	7 9 12	3eqtr4d	$⊢ (A \in ω \land y \in ω) \to suc A +_{𝑜} y = suc (A +_{𝑜} y)$
14		sseq2	$⊢ x = A +_{𝑜} y \to (A \subseteq x \leftrightarrow A \subseteq A +_{𝑜} y)$
15		suceq	$⊢ x = A +_{𝑜} y \to suc x = suc (A +_{𝑜} y)$
16	15	eqeq2d	$⊢ x = A +_{𝑜} y \to (suc A +_{𝑜} y = suc x \leftrightarrow suc A +_{𝑜} y = suc (A +_{𝑜} y))$
17	14 16	anbi12d	$⊢ x = A +_{𝑜} y \to ((A \subseteq x \land suc A +_{𝑜} y = suc x) \leftrightarrow (A \subseteq A +_{𝑜} y \land suc A +_{𝑜} y = suc (A +_{𝑜} y)))$
18	17	rspcev	$⊢ (A +_{𝑜} y \in ω \land (A \subseteq A +_{𝑜} y \land suc A +_{𝑜} y = suc (A +_{𝑜} y))) \to \exists x \in ω (A \subseteq x \land suc A +_{𝑜} y = suc x)$
19	4 5 13 18	syl12anc	$⊢ (A \in ω \land y \in ω) \to \exists x \in ω (A \subseteq x \land suc A +_{𝑜} y = suc x)$
20		eqeq1	$⊢ suc A +_{𝑜} y = B \to (suc A +_{𝑜} y = suc x \leftrightarrow B = suc x)$
21	20	anbi2d	$⊢ suc A +_{𝑜} y = B \to ((A \subseteq x \land suc A +_{𝑜} y = suc x) \leftrightarrow (A \subseteq x \land B = suc x))$
22	21	rexbidv	$⊢ suc A +_{𝑜} y = B \to (\exists x \in ω (A \subseteq x \land suc A +_{𝑜} y = suc x) \leftrightarrow \exists x \in ω (A \subseteq x \land B = suc x))$
23	19 22	syl5ibcom	$⊢ (A \in ω \land y \in ω) \to (suc A +_{𝑜} y = B \to \exists x \in ω (A \subseteq x \land B = suc x))$
24	23	rexlimdva	$⊢ A \in ω \to (\exists y \in ω suc A +_{𝑜} y = B \to \exists x \in ω (A \subseteq x \land B = suc x))$
25	24	adantr	$⊢ (A \in ω \land B \in ω) \to (\exists y \in ω suc A +_{𝑜} y = B \to \exists x \in ω (A \subseteq x \land B = suc x))$
26	3 25	sylbid	$⊢ (A \in ω \land B \in ω) \to (suc A \subseteq B \to \exists x \in ω (A \subseteq x \land B = suc x))$
27	26	expimpd	$⊢ A \in ω \to ((B \in ω \land suc A \subseteq B) \to \exists x \in ω (A \subseteq x \land B = suc x))$
28		peano2	$⊢ x \in ω \to suc x \in ω$
29	28	ad2antlr	$⊢ ((A \in ω \land x \in ω) \land A \subseteq x) \to suc x \in ω$
30		nnord	$⊢ A \in ω \to Ord A$
31		nnord	$⊢ x \in ω \to Ord x$
32		ordsucsssuc	$⊢ (Ord A \land Ord x) \to (A \subseteq x \leftrightarrow suc A \subseteq suc x)$
33	30 31 32	syl2an	$⊢ (A \in ω \land x \in ω) \to (A \subseteq x \leftrightarrow suc A \subseteq suc x)$
34	33	biimpa	$⊢ ((A \in ω \land x \in ω) \land A \subseteq x) \to suc A \subseteq suc x$
35	29 34	jca	$⊢ ((A \in ω \land x \in ω) \land A \subseteq x) \to (suc x \in ω \land suc A \subseteq suc x)$
36		eleq1	$⊢ B = suc x \to (B \in ω \leftrightarrow suc x \in ω)$
37		sseq2	$⊢ B = suc x \to (suc A \subseteq B \leftrightarrow suc A \subseteq suc x)$
38	36 37	anbi12d	$⊢ B = suc x \to ((B \in ω \land suc A \subseteq B) \leftrightarrow (suc x \in ω \land suc A \subseteq suc x))$
39	35 38	syl5ibrcom	$⊢ ((A \in ω \land x \in ω) \land A \subseteq x) \to (B = suc x \to (B \in ω \land suc A \subseteq B))$
40	39	expimpd	$⊢ (A \in ω \land x \in ω) \to ((A \subseteq x \land B = suc x) \to (B \in ω \land suc A \subseteq B))$
41	40	rexlimdva	$⊢ A \in ω \to (\exists x \in ω (A \subseteq x \land B = suc x) \to (B \in ω \land suc A \subseteq B))$
42	27 41	impbid	$⊢ A \in ω \to ((B \in ω \land suc A \subseteq B) \leftrightarrow \exists x \in ω (A \subseteq x \land B = suc x))$
43		eldif	$⊢ B \in (ω ∖ suc A) \leftrightarrow (B \in ω \land \neg B \in suc A)$
44		nnord	$⊢ suc A \in ω \to Ord suc A$
45	1 44	syl	$⊢ A \in ω \to Ord suc A$
46		nnord	$⊢ B \in ω \to Ord B$
47		ordtri1	$⊢ (Ord suc A \land Ord B) \to (suc A \subseteq B \leftrightarrow \neg B \in suc A)$
48	45 46 47	syl2an	$⊢ (A \in ω \land B \in ω) \to (suc A \subseteq B \leftrightarrow \neg B \in suc A)$
49	48	pm5.32da	$⊢ A \in ω \to ((B \in ω \land suc A \subseteq B) \leftrightarrow (B \in ω \land \neg B \in suc A))$
50	43 49	bitr4id	$⊢ A \in ω \to (B \in (ω ∖ suc A) \leftrightarrow (B \in ω \land suc A \subseteq B))$
51		eldif	$⊢ x \in (ω ∖ A) \leftrightarrow (x \in ω \land \neg x \in A)$
52	51	anbi1i	$⊢ (x \in (ω ∖ A) \land B = suc x) \leftrightarrow ((x \in ω \land \neg x \in A) \land B = suc x)$
53		anass	$⊢ ((x \in ω \land \neg x \in A) \land B = suc x) \leftrightarrow (x \in ω \land (\neg x \in A \land B = suc x))$
54	52 53	bitri	$⊢ (x \in (ω ∖ A) \land B = suc x) \leftrightarrow (x \in ω \land (\neg x \in A \land B = suc x))$
55	54	rexbii2	$⊢ \exists x \in (ω ∖ A) B = suc x \leftrightarrow \exists x \in ω (\neg x \in A \land B = suc x)$
56		ordtri1	$⊢ (Ord A \land Ord x) \to (A \subseteq x \leftrightarrow \neg x \in A)$
57	30 31 56	syl2an	$⊢ (A \in ω \land x \in ω) \to (A \subseteq x \leftrightarrow \neg x \in A)$
58	57	anbi1d	$⊢ (A \in ω \land x \in ω) \to ((A \subseteq x \land B = suc x) \leftrightarrow (\neg x \in A \land B = suc x))$
59	58	rexbidva	$⊢ A \in ω \to (\exists x \in ω (A \subseteq x \land B = suc x) \leftrightarrow \exists x \in ω (\neg x \in A \land B = suc x))$
60	55 59	bitr4id	$⊢ A \in ω \to (\exists x \in (ω ∖ A) B = suc x \leftrightarrow \exists x \in ω (A \subseteq x \land B = suc x))$
61	42 50 60	3bitr4d	$⊢ A \in ω \to (B \in (ω ∖ suc A) \leftrightarrow \exists x \in (ω ∖ A) B = suc x)$

Metamath Proof Explorer

Theorem eldifsucnn

Proof