cantnftermord

Description: For terms of the form of a power of omega times a non-zero natural number, ordering of the exponents implies ordering of the terms. Lemma 5.1 of Schloeder p. 15. (Contributed by RP, 30-Jan-2025)

		Ref	Expression
	Assertion	cantnftermord	$⊢ ((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \to (A \in B \to (ω ↑_{𝑜} A) \cdot_{𝑜} C \in ((ω ↑_{𝑜} B) \cdot_{𝑜} D))$

Proof

Step	Hyp	Ref	Expression
1		simplll	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to A \in On$
2		onsuc	$⊢ A \in On \to suc A \in On$
3	1 2	syl	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to suc A \in On$
4		simpllr	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to B \in On$
5		omelon	$⊢ ω \in On$
6		1onn	$⊢ 1_{𝑜} \in ω$
7		ondif2	$⊢ ω \in (On ∖ 2_{𝑜}) \leftrightarrow (ω \in On \land 1_{𝑜} \in ω)$
8	5 6 7	mpbir2an	$⊢ ω \in (On ∖ 2_{𝑜})$
9	8	a1i	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to ω \in (On ∖ 2_{𝑜})$
10		onsucss	$⊢ B \in On \to (A \in B \to suc A \subseteq B)$
11	10	ad2antlr	$⊢ ((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \to (A \in B \to suc A \subseteq B)$
12	11	imp	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to suc A \subseteq B$
13		oeword	$⊢ (suc A \in On \land B \in On \land ω \in (On ∖ 2_{𝑜})) \to (suc A \subseteq B \leftrightarrow ω ↑_{𝑜} suc A \subseteq ω ↑_{𝑜} B)$
14	13	biimpa	$⊢ ((suc A \in On \land B \in On \land ω \in (On ∖ 2_{𝑜})) \land suc A \subseteq B) \to ω ↑_{𝑜} suc A \subseteq ω ↑_{𝑜} B$
15	3 4 9 12 14	syl31anc	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to ω ↑_{𝑜} suc A \subseteq ω ↑_{𝑜} B$
16	5	a1i	$⊢ (A \in On \land B \in On) \to ω \in On$
17		oecl	$⊢ (ω \in On \land B \in On) \to ω ↑_{𝑜} B \in On$
18	16 17	sylancom	$⊢ (A \in On \land B \in On) \to ω ↑_{𝑜} B \in On$
19		omsson	$⊢ ω \subseteq On$
20		ssdif	$⊢ ω \subseteq On \to ω ∖ 1_{𝑜} \subseteq On ∖ 1_{𝑜}$
21	19 20	ax-mp	$⊢ ω ∖ 1_{𝑜} \subseteq On ∖ 1_{𝑜}$
22	21	sseli	$⊢ D \in (ω ∖ 1_{𝑜}) \to D \in (On ∖ 1_{𝑜})$
23		ondif1	$⊢ D \in (On ∖ 1_{𝑜}) \leftrightarrow (D \in On \land \emptyset \in D)$
24	22 23	sylib	$⊢ D \in (ω ∖ 1_{𝑜}) \to (D \in On \land \emptyset \in D)$
25	24	adantl	$⊢ (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜})) \to (D \in On \land \emptyset \in D)$
26	18 25	anim12i	$⊢ ((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \to (ω ↑_{𝑜} B \in On \land (D \in On \land \emptyset \in D))$
27	26	adantr	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to (ω ↑_{𝑜} B \in On \land (D \in On \land \emptyset \in D))$
28		anass	$⊢ ((ω ↑_{𝑜} B \in On \land D \in On) \land \emptyset \in D) \leftrightarrow (ω ↑_{𝑜} B \in On \land (D \in On \land \emptyset \in D))$
29	27 28	sylibr	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to ((ω ↑_{𝑜} B \in On \land D \in On) \land \emptyset \in D)$
30		omword1	$⊢ ((ω ↑_{𝑜} B \in On \land D \in On) \land \emptyset \in D) \to ω ↑_{𝑜} B \subseteq (ω ↑_{𝑜} B) \cdot_{𝑜} D$
31	29 30	syl	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to ω ↑_{𝑜} B \subseteq (ω ↑_{𝑜} B) \cdot_{𝑜} D$
32	15 31	sstrd	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to ω ↑_{𝑜} suc A \subseteq (ω ↑_{𝑜} B) \cdot_{𝑜} D$
33	5	a1i	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to ω \in On$
34	1 5	jctil	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to (ω \in On \land A \in On)$
35		oecl	$⊢ (ω \in On \land A \in On) \to ω ↑_{𝑜} A \in On$
36	34 35	syl	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to ω ↑_{𝑜} A \in On$
37		peano1	$⊢ \emptyset \in ω$
38		oen0	$⊢ ((ω \in On \land A \in On) \land \emptyset \in ω) \to \emptyset \in (ω ↑_{𝑜} A)$
39	34 37 38	sylancl	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to \emptyset \in (ω ↑_{𝑜} A)$
40		simplrl	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to C \in (ω ∖ 1_{𝑜})$
41	40	eldifad	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to C \in ω$
42		omordi	$⊢ ((ω \in On \land ω ↑_{𝑜} A \in On) \land \emptyset \in (ω ↑_{𝑜} A)) \to (C \in ω \to (ω ↑_{𝑜} A) \cdot_{𝑜} C \in ((ω ↑_{𝑜} A) \cdot_{𝑜} ω))$
43	42	imp	$⊢ (((ω \in On \land ω ↑_{𝑜} A \in On) \land \emptyset \in (ω ↑_{𝑜} A)) \land C \in ω) \to (ω ↑_{𝑜} A) \cdot_{𝑜} C \in ((ω ↑_{𝑜} A) \cdot_{𝑜} ω)$
44	33 36 39 41 43	syl1111anc	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to (ω ↑_{𝑜} A) \cdot_{𝑜} C \in ((ω ↑_{𝑜} A) \cdot_{𝑜} ω)$
45		oesuc	$⊢ (ω \in On \land A \in On) \to ω ↑_{𝑜} suc A = (ω ↑_{𝑜} A) \cdot_{𝑜} ω$
46	34 45	syl	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to ω ↑_{𝑜} suc A = (ω ↑_{𝑜} A) \cdot_{𝑜} ω$
47	44 46	eleqtrrd	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to (ω ↑_{𝑜} A) \cdot_{𝑜} C \in (ω ↑_{𝑜} suc A)$
48	32 47	sseldd	$⊢ (((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \land A \in B) \to (ω ↑_{𝑜} A) \cdot_{𝑜} C \in ((ω ↑_{𝑜} B) \cdot_{𝑜} D)$
49	48	ex	$⊢ ((A \in On \land B \in On) \land (C \in (ω ∖ 1_{𝑜}) \land D \in (ω ∖ 1_{𝑜}))) \to (A \in B \to (ω ↑_{𝑜} A) \cdot_{𝑜} C \in ((ω ↑_{𝑜} B) \cdot_{𝑜} D))$

Metamath Proof Explorer

Theorem cantnftermord

Proof