oawordri

Description: Weak ordering property of ordinal addition. Proposition 8.7 of TakeutiZaring p. 59. (Contributed by NM, 7-Dec-2004)

		Ref	Expression
	Assertion	oawordri	$⊢ (A \in On \land B \in On \land C \in On) \to (A \subseteq B \to A +_{𝑜} C \subseteq B +_{𝑜} C)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = \emptyset \to A +_{𝑜} x = A +_{𝑜} \emptyset$
2		oveq2	$⊢ x = \emptyset \to B +_{𝑜} x = B +_{𝑜} \emptyset$
3	1 2	sseq12d	$⊢ x = \emptyset \to (A +_{𝑜} x \subseteq B +_{𝑜} x \leftrightarrow A +_{𝑜} \emptyset \subseteq B +_{𝑜} \emptyset)$
4		oveq2	$⊢ x = y \to A +_{𝑜} x = A +_{𝑜} y$
5		oveq2	$⊢ x = y \to B +_{𝑜} x = B +_{𝑜} y$
6	4 5	sseq12d	$⊢ x = y \to (A +_{𝑜} x \subseteq B +_{𝑜} x \leftrightarrow A +_{𝑜} y \subseteq B +_{𝑜} y)$
7		oveq2	$⊢ x = suc y \to A +_{𝑜} x = A +_{𝑜} suc y$
8		oveq2	$⊢ x = suc y \to B +_{𝑜} x = B +_{𝑜} suc y$
9	7 8	sseq12d	$⊢ x = suc y \to (A +_{𝑜} x \subseteq B +_{𝑜} x \leftrightarrow A +_{𝑜} suc y \subseteq B +_{𝑜} suc y)$
10		oveq2	$⊢ x = C \to A +_{𝑜} x = A +_{𝑜} C$
11		oveq2	$⊢ x = C \to B +_{𝑜} x = B +_{𝑜} C$
12	10 11	sseq12d	$⊢ x = C \to (A +_{𝑜} x \subseteq B +_{𝑜} x \leftrightarrow A +_{𝑜} C \subseteq B +_{𝑜} C)$
13		oa0	$⊢ A \in On \to A +_{𝑜} \emptyset = A$
14	13	adantr	$⊢ (A \in On \land B \in On) \to A +_{𝑜} \emptyset = A$
15		oa0	$⊢ B \in On \to B +_{𝑜} \emptyset = B$
16	15	adantl	$⊢ (A \in On \land B \in On) \to B +_{𝑜} \emptyset = B$
17	14 16	sseq12d	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} \emptyset \subseteq B +_{𝑜} \emptyset \leftrightarrow A \subseteq B)$
18	17	biimpar	$⊢ ((A \in On \land B \in On) \land A \subseteq B) \to A +_{𝑜} \emptyset \subseteq B +_{𝑜} \emptyset$
19		oacl	$⊢ (A \in On \land y \in On) \to A +_{𝑜} y \in On$
20		eloni	$⊢ A +_{𝑜} y \in On \to Ord (A +_{𝑜} y)$
21	19 20	syl	$⊢ (A \in On \land y \in On) \to Ord (A +_{𝑜} y)$
22		oacl	$⊢ (B \in On \land y \in On) \to B +_{𝑜} y \in On$
23		eloni	$⊢ B +_{𝑜} y \in On \to Ord (B +_{𝑜} y)$
24	22 23	syl	$⊢ (B \in On \land y \in On) \to Ord (B +_{𝑜} y)$
25		ordsucsssuc	$⊢ (Ord (A +_{𝑜} y) \land Ord (B +_{𝑜} y)) \to (A +_{𝑜} y \subseteq B +_{𝑜} y \leftrightarrow suc (A +_{𝑜} y) \subseteq suc (B +_{𝑜} y))$
26	21 24 25	syl2an	$⊢ ((A \in On \land y \in On) \land (B \in On \land y \in On)) \to (A +_{𝑜} y \subseteq B +_{𝑜} y \leftrightarrow suc (A +_{𝑜} y) \subseteq suc (B +_{𝑜} y))$
27	26	anandirs	$⊢ ((A \in On \land B \in On) \land y \in On) \to (A +_{𝑜} y \subseteq B +_{𝑜} y \leftrightarrow suc (A +_{𝑜} y) \subseteq suc (B +_{𝑜} y))$
28		oasuc	$⊢ (A \in On \land y \in On) \to A +_{𝑜} suc y = suc (A +_{𝑜} y)$
29	28	adantlr	$⊢ ((A \in On \land B \in On) \land y \in On) \to A +_{𝑜} suc y = suc (A +_{𝑜} y)$
30		oasuc	$⊢ (B \in On \land y \in On) \to B +_{𝑜} suc y = suc (B +_{𝑜} y)$
31	30	adantll	$⊢ ((A \in On \land B \in On) \land y \in On) \to B +_{𝑜} suc y = suc (B +_{𝑜} y)$
32	29 31	sseq12d	$⊢ ((A \in On \land B \in On) \land y \in On) \to (A +_{𝑜} suc y \subseteq B +_{𝑜} suc y \leftrightarrow suc (A +_{𝑜} y) \subseteq suc (B +_{𝑜} y))$
33	27 32	bitr4d	$⊢ ((A \in On \land B \in On) \land y \in On) \to (A +_{𝑜} y \subseteq B +_{𝑜} y \leftrightarrow A +_{𝑜} suc y \subseteq B +_{𝑜} suc y)$
34	33	biimpd	$⊢ ((A \in On \land B \in On) \land y \in On) \to (A +_{𝑜} y \subseteq B +_{𝑜} y \to A +_{𝑜} suc y \subseteq B +_{𝑜} suc y)$
35	34	expcom	$⊢ y \in On \to ((A \in On \land B \in On) \to (A +_{𝑜} y \subseteq B +_{𝑜} y \to A +_{𝑜} suc y \subseteq B +_{𝑜} suc y))$
36	35	adantrd	$⊢ y \in On \to (((A \in On \land B \in On) \land A \subseteq B) \to (A +_{𝑜} y \subseteq B +_{𝑜} y \to A +_{𝑜} suc y \subseteq B +_{𝑜} suc y))$
37		vex	$⊢ x \in V$
38		ss2iun	$⊢ \forall y \in x A +_{𝑜} y \subseteq B +_{𝑜} y \to ⋃_{y \in x} (A +_{𝑜} y) \subseteq ⋃_{y \in x} (B +_{𝑜} y)$
39		oalim	$⊢ (A \in On \land (x \in V \land Lim x)) \to A +_{𝑜} x = ⋃_{y \in x} (A +_{𝑜} y)$
40	39	adantlr	$⊢ ((A \in On \land B \in On) \land (x \in V \land Lim x)) \to A +_{𝑜} x = ⋃_{y \in x} (A +_{𝑜} y)$
41		oalim	$⊢ (B \in On \land (x \in V \land Lim x)) \to B +_{𝑜} x = ⋃_{y \in x} (B +_{𝑜} y)$
42	41	adantll	$⊢ ((A \in On \land B \in On) \land (x \in V \land Lim x)) \to B +_{𝑜} x = ⋃_{y \in x} (B +_{𝑜} y)$
43	40 42	sseq12d	$⊢ ((A \in On \land B \in On) \land (x \in V \land Lim x)) \to (A +_{𝑜} x \subseteq B +_{𝑜} x \leftrightarrow ⋃_{y \in x} (A +_{𝑜} y) \subseteq ⋃_{y \in x} (B +_{𝑜} y))$
44	38 43	imbitrrid	$⊢ ((A \in On \land B \in On) \land (x \in V \land Lim x)) \to (\forall y \in x A +_{𝑜} y \subseteq B +_{𝑜} y \to A +_{𝑜} x \subseteq B +_{𝑜} x)$
45	37 44	mpanr1	$⊢ ((A \in On \land B \in On) \land Lim x) \to (\forall y \in x A +_{𝑜} y \subseteq B +_{𝑜} y \to A +_{𝑜} x \subseteq B +_{𝑜} x)$
46	45	expcom	$⊢ Lim x \to ((A \in On \land B \in On) \to (\forall y \in x A +_{𝑜} y \subseteq B +_{𝑜} y \to A +_{𝑜} x \subseteq B +_{𝑜} x))$
47	46	adantrd	$⊢ Lim x \to (((A \in On \land B \in On) \land A \subseteq B) \to (\forall y \in x A +_{𝑜} y \subseteq B +_{𝑜} y \to A +_{𝑜} x \subseteq B +_{𝑜} x))$
48	3 6 9 12 18 36 47	tfinds3	$⊢ C \in On \to (((A \in On \land B \in On) \land A \subseteq B) \to A +_{𝑜} C \subseteq B +_{𝑜} C)$
49	48	exp4c	$⊢ C \in On \to (A \in On \to (B \in On \to (A \subseteq B \to A +_{𝑜} C \subseteq B +_{𝑜} C)))$
50	49	3imp231	$⊢ (A \in On \land B \in On \land C \in On) \to (A \subseteq B \to A +_{𝑜} C \subseteq B +_{𝑜} C)$

Metamath Proof Explorer

Theorem oawordri

Proof