nnoeomeqom

Description: Any natural number at least as large as two raised to the power of omega is omega. Lemma 3.25 of Schloeder p. 11. (Contributed by RP, 30-Jan-2025)

		Ref	Expression
	Assertion	nnoeomeqom	$⊢ (A \in ω \land 1_{𝑜} \in A) \to A ↑_{𝑜} ω = ω$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ω \land 1_{𝑜} \in A) \to A \in ω$
2		nnon	$⊢ A \in ω \to A \in On$
3	1 2	syl	$⊢ (A \in ω \land 1_{𝑜} \in A) \to A \in On$
4		omelon	$⊢ ω \in On$
5		limom	$⊢ Lim ω$
6	4 5	pm3.2i	$⊢ (ω \in On \land Lim ω)$
7	6	a1i	$⊢ (A \in ω \land 1_{𝑜} \in A) \to (ω \in On \land Lim ω)$
8		0elon	$⊢ \emptyset \in On$
9	8	a1i	$⊢ (A \in ω \land 1_{𝑜} \in A) \to \emptyset \in On$
10		0ss	$⊢ \emptyset \subseteq 1_{𝑜}$
11	10	a1i	$⊢ (A \in ω \land 1_{𝑜} \in A) \to \emptyset \subseteq 1_{𝑜}$
12		simpr	$⊢ (A \in ω \land 1_{𝑜} \in A) \to 1_{𝑜} \in A$
13		ontr2	$⊢ (\emptyset \in On \land A \in On) \to ((\emptyset \subseteq 1_{𝑜} \land 1_{𝑜} \in A) \to \emptyset \in A)$
14	13	imp	$⊢ ((\emptyset \in On \land A \in On) \land (\emptyset \subseteq 1_{𝑜} \land 1_{𝑜} \in A)) \to \emptyset \in A$
15	9 3 11 12 14	syl22anc	$⊢ (A \in ω \land 1_{𝑜} \in A) \to \emptyset \in A$
16		oelim	$⊢ ((A \in On \land (ω \in On \land Lim ω)) \land \emptyset \in A) \to A ↑_{𝑜} ω = ⋃_{x \in ω} (A ↑_{𝑜} x)$
17	3 7 15 16	syl21anc	$⊢ (A \in ω \land 1_{𝑜} \in A) \to A ↑_{𝑜} ω = ⋃_{x \in ω} (A ↑_{𝑜} x)$
18		ovex	$⊢ A ↑_{𝑜} x \in V$
19	18	dfiun2	$⊢ ⋃_{x \in ω} (A ↑_{𝑜} x) = ⋃ \{y \| \exists x \in ω y = A ↑_{𝑜} x\}$
20		eluniab	$⊢ z \in ⋃ \{y \| \exists x \in ω y = A ↑_{𝑜} x\} \leftrightarrow \exists y (z \in y \land \exists x \in ω y = A ↑_{𝑜} x)$
21		19.42v	$⊢ \exists x (z \in y \land (x \in ω \land y = A ↑_{𝑜} x)) \leftrightarrow (z \in y \land \exists x (x \in ω \land y = A ↑_{𝑜} x))$
22		3anass	$⊢ (z \in y \land x \in ω \land y = A ↑_{𝑜} x) \leftrightarrow (z \in y \land (x \in ω \land y = A ↑_{𝑜} x))$
23	22	exbii	$⊢ \exists x (z \in y \land x \in ω \land y = A ↑_{𝑜} x) \leftrightarrow \exists x (z \in y \land (x \in ω \land y = A ↑_{𝑜} x))$
24		df-rex	$⊢ \exists x \in ω y = A ↑_{𝑜} x \leftrightarrow \exists x (x \in ω \land y = A ↑_{𝑜} x)$
25	24	anbi2i	$⊢ (z \in y \land \exists x \in ω y = A ↑_{𝑜} x) \leftrightarrow (z \in y \land \exists x (x \in ω \land y = A ↑_{𝑜} x))$
26	21 23 25	3bitr4ri	$⊢ (z \in y \land \exists x \in ω y = A ↑_{𝑜} x) \leftrightarrow \exists x (z \in y \land x \in ω \land y = A ↑_{𝑜} x)$
27	26	exbii	$⊢ \exists y (z \in y \land \exists x \in ω y = A ↑_{𝑜} x) \leftrightarrow \exists y \exists x (z \in y \land x \in ω \land y = A ↑_{𝑜} x)$
28		excom	$⊢ \exists y \exists x (z \in y \land x \in ω \land y = A ↑_{𝑜} x) \leftrightarrow \exists x \exists y (z \in y \land x \in ω \land y = A ↑_{𝑜} x)$
29	20 27 28	3bitri	$⊢ z \in ⋃ \{y \| \exists x \in ω y = A ↑_{𝑜} x\} \leftrightarrow \exists x \exists y (z \in y \land x \in ω \land y = A ↑_{𝑜} x)$
30		simpr3	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land (z \in y \land x \in ω \land y = A ↑_{𝑜} x)) \to y = A ↑_{𝑜} x$
31		simp2	$⊢ (z \in y \land x \in ω \land y = A ↑_{𝑜} x) \to x \in ω$
32		nnecl	$⊢ (A \in ω \land x \in ω) \to A ↑_{𝑜} x \in ω$
33	1 31 32	syl2an	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land (z \in y \land x \in ω \land y = A ↑_{𝑜} x)) \to A ↑_{𝑜} x \in ω$
34		onelss	$⊢ ω \in On \to (A ↑_{𝑜} x \in ω \to A ↑_{𝑜} x \subseteq ω)$
35	4 33 34	mpsyl	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land (z \in y \land x \in ω \land y = A ↑_{𝑜} x)) \to A ↑_{𝑜} x \subseteq ω$
36	30 35	eqsstrd	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land (z \in y \land x \in ω \land y = A ↑_{𝑜} x)) \to y \subseteq ω$
37		simpr1	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land (z \in y \land x \in ω \land y = A ↑_{𝑜} x)) \to z \in y$
38	36 37	sseldd	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land (z \in y \land x \in ω \land y = A ↑_{𝑜} x)) \to z \in ω$
39	38	ex	$⊢ (A \in ω \land 1_{𝑜} \in A) \to ((z \in y \land x \in ω \land y = A ↑_{𝑜} x) \to z \in ω)$
40	39	exlimdvv	$⊢ (A \in ω \land 1_{𝑜} \in A) \to (\exists x \exists y (z \in y \land x \in ω \land y = A ↑_{𝑜} x) \to z \in ω)$
41		peano2	$⊢ z \in ω \to suc z \in ω$
42	41	adantl	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land z \in ω) \to suc z \in ω$
43		ovex	$⊢ A ↑_{𝑜} suc z \in V$
44	43	a1i	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land z \in ω) \to A ↑_{𝑜} suc z \in V$
45	2	anim1i	$⊢ (A \in ω \land 1_{𝑜} \in A) \to (A \in On \land 1_{𝑜} \in A)$
46		ondif2	$⊢ A \in (On ∖ 2_{𝑜}) \leftrightarrow (A \in On \land 1_{𝑜} \in A)$
47	45 46	sylibr	$⊢ (A \in ω \land 1_{𝑜} \in A) \to A \in (On ∖ 2_{𝑜})$
48		nnon	$⊢ suc z \in ω \to suc z \in On$
49	41 48	syl	$⊢ z \in ω \to suc z \in On$
50		oeworde	$⊢ (A \in (On ∖ 2_{𝑜}) \land suc z \in On) \to suc z \subseteq A ↑_{𝑜} suc z$
51	47 49 50	syl2an	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land z \in ω) \to suc z \subseteq A ↑_{𝑜} suc z$
52		vex	$⊢ z \in V$
53	52	sucid	$⊢ z \in suc z$
54	53	a1i	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land z \in ω) \to z \in suc z$
55	51 54	sseldd	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land z \in ω) \to z \in (A ↑_{𝑜} suc z)$
56		eqidd	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land z \in ω) \to A ↑_{𝑜} suc z = A ↑_{𝑜} suc z$
57	55 42 56	3jca	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land z \in ω) \to (z \in (A ↑_{𝑜} suc z) \land suc z \in ω \land A ↑_{𝑜} suc z = A ↑_{𝑜} suc z)$
58		eleq2	$⊢ y = A ↑_{𝑜} suc z \to (z \in y \leftrightarrow z \in (A ↑_{𝑜} suc z))$
59		eqeq1	$⊢ y = A ↑_{𝑜} suc z \to (y = A ↑_{𝑜} suc z \leftrightarrow A ↑_{𝑜} suc z = A ↑_{𝑜} suc z)$
60	58 59	3anbi13d	$⊢ y = A ↑_{𝑜} suc z \to ((z \in y \land suc z \in ω \land y = A ↑_{𝑜} suc z) \leftrightarrow (z \in (A ↑_{𝑜} suc z) \land suc z \in ω \land A ↑_{𝑜} suc z = A ↑_{𝑜} suc z))$
61	44 57 60	spcedv	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land z \in ω) \to \exists y (z \in y \land suc z \in ω \land y = A ↑_{𝑜} suc z)$
62		eleq1	$⊢ x = suc z \to (x \in ω \leftrightarrow suc z \in ω)$
63		oveq2	$⊢ x = suc z \to A ↑_{𝑜} x = A ↑_{𝑜} suc z$
64	63	eqeq2d	$⊢ x = suc z \to (y = A ↑_{𝑜} x \leftrightarrow y = A ↑_{𝑜} suc z)$
65	62 64	3anbi23d	$⊢ x = suc z \to ((z \in y \land x \in ω \land y = A ↑_{𝑜} x) \leftrightarrow (z \in y \land suc z \in ω \land y = A ↑_{𝑜} suc z))$
66	65	exbidv	$⊢ x = suc z \to (\exists y (z \in y \land x \in ω \land y = A ↑_{𝑜} x) \leftrightarrow \exists y (z \in y \land suc z \in ω \land y = A ↑_{𝑜} suc z))$
67	42 61 66	spcedv	$⊢ ((A \in ω \land 1_{𝑜} \in A) \land z \in ω) \to \exists x \exists y (z \in y \land x \in ω \land y = A ↑_{𝑜} x)$
68	67	ex	$⊢ (A \in ω \land 1_{𝑜} \in A) \to (z \in ω \to \exists x \exists y (z \in y \land x \in ω \land y = A ↑_{𝑜} x))$
69	40 68	impbid	$⊢ (A \in ω \land 1_{𝑜} \in A) \to (\exists x \exists y (z \in y \land x \in ω \land y = A ↑_{𝑜} x) \leftrightarrow z \in ω)$
70	29 69	bitrid	$⊢ (A \in ω \land 1_{𝑜} \in A) \to (z \in ⋃ \{y \| \exists x \in ω y = A ↑_{𝑜} x\} \leftrightarrow z \in ω)$
71	70	eqrdv	$⊢ (A \in ω \land 1_{𝑜} \in A) \to ⋃ \{y \| \exists x \in ω y = A ↑_{𝑜} x\} = ω$
72	19 71	eqtrid	$⊢ (A \in ω \land 1_{𝑜} \in A) \to ⋃_{x \in ω} (A ↑_{𝑜} x) = ω$
73	17 72	eqtrd	$⊢ (A \in ω \land 1_{𝑜} \in A) \to A ↑_{𝑜} ω = ω$

Metamath Proof Explorer

Theorem nnoeomeqom

Proof