oaordi

Description: Ordering property of ordinal addition. Proposition 8.4 of TakeutiZaring p. 58. (Contributed by NM, 5-Dec-2004)

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

Proof

Step	Hyp	Ref	Expression
1		onelon	$⊢ (B \in On \land A \in B) \to A \in On$
2	1	adantll	$⊢ ((C \in On \land B \in On) \land A \in B) \to A \in On$
3		eloni	$⊢ B \in On \to Ord B$
4		ordsucss	$⊢ Ord B \to (A \in B \to suc A \subseteq B)$
5	3 4	syl	$⊢ B \in On \to (A \in B \to suc A \subseteq B)$
6	5	ad2antlr	$⊢ ((C \in On \land B \in On) \land A \in On) \to (A \in B \to suc A \subseteq B)$
7		onsucb	$⊢ A \in On \leftrightarrow suc A \in On$
8		oveq2	$⊢ x = suc A \to C +_{𝑜} x = C +_{𝑜} suc A$
9	8	sseq2d	$⊢ x = suc A \to (C +_{𝑜} suc A \subseteq C +_{𝑜} x \leftrightarrow C +_{𝑜} suc A \subseteq C +_{𝑜} suc A)$
10	9	imbi2d	$⊢ x = suc A \to ((C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} x) \leftrightarrow (C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc A))$
11		oveq2	$⊢ x = y \to C +_{𝑜} x = C +_{𝑜} y$
12	11	sseq2d	$⊢ x = y \to (C +_{𝑜} suc A \subseteq C +_{𝑜} x \leftrightarrow C +_{𝑜} suc A \subseteq C +_{𝑜} y)$
13	12	imbi2d	$⊢ x = y \to ((C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} x) \leftrightarrow (C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} y))$
14		oveq2	$⊢ x = suc y \to C +_{𝑜} x = C +_{𝑜} suc y$
15	14	sseq2d	$⊢ x = suc y \to (C +_{𝑜} suc A \subseteq C +_{𝑜} x \leftrightarrow C +_{𝑜} suc A \subseteq C +_{𝑜} suc y)$
16	15	imbi2d	$⊢ x = suc y \to ((C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} x) \leftrightarrow (C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc y))$
17		oveq2	$⊢ x = B \to C +_{𝑜} x = C +_{𝑜} B$
18	17	sseq2d	$⊢ x = B \to (C +_{𝑜} suc A \subseteq C +_{𝑜} x \leftrightarrow C +_{𝑜} suc A \subseteq C +_{𝑜} B)$
19	18	imbi2d	$⊢ x = B \to ((C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} x) \leftrightarrow (C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} B))$
20		ssid	$⊢ C +_{𝑜} suc A \subseteq C +_{𝑜} suc A$
21	20	2a1i	$⊢ suc A \in On \to (C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc A)$
22		sssucid	$⊢ C +_{𝑜} y \subseteq suc (C +_{𝑜} y)$
23		sstr2	$⊢ C +_{𝑜} suc A \subseteq C +_{𝑜} y \to (C +_{𝑜} y \subseteq suc (C +_{𝑜} y) \to C +_{𝑜} suc A \subseteq suc (C +_{𝑜} y))$
24	22 23	mpi	$⊢ C +_{𝑜} suc A \subseteq C +_{𝑜} y \to C +_{𝑜} suc A \subseteq suc (C +_{𝑜} y)$
25		oasuc	$⊢ (C \in On \land y \in On) \to C +_{𝑜} suc y = suc (C +_{𝑜} y)$
26	25	ancoms	$⊢ (y \in On \land C \in On) \to C +_{𝑜} suc y = suc (C +_{𝑜} y)$
27	26	sseq2d	$⊢ (y \in On \land C \in On) \to (C +_{𝑜} suc A \subseteq C +_{𝑜} suc y \leftrightarrow C +_{𝑜} suc A \subseteq suc (C +_{𝑜} y))$
28	24 27	imbitrrid	$⊢ (y \in On \land C \in On) \to (C +_{𝑜} suc A \subseteq C +_{𝑜} y \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc y)$
29	28	ex	$⊢ y \in On \to (C \in On \to (C +_{𝑜} suc A \subseteq C +_{𝑜} y \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc y))$
30	29	ad2antrr	$⊢ ((y \in On \land suc A \in On) \land suc A \subseteq y) \to (C \in On \to (C +_{𝑜} suc A \subseteq C +_{𝑜} y \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc y))$
31	30	a2d	$⊢ ((y \in On \land suc A \in On) \land suc A \subseteq y) \to ((C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} y) \to (C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc y))$
32		sucssel	$⊢ A \in On \to (suc A \subseteq x \to A \in x)$
33	7 32	sylbir	$⊢ suc A \in On \to (suc A \subseteq x \to A \in x)$
34		limsuc	$⊢ Lim x \to (A \in x \leftrightarrow suc A \in x)$
35	34	biimpd	$⊢ Lim x \to (A \in x \to suc A \in x)$
36	33 35	sylan9r	$⊢ (Lim x \land suc A \in On) \to (suc A \subseteq x \to suc A \in x)$
37	36	imp	$⊢ ((Lim x \land suc A \in On) \land suc A \subseteq x) \to suc A \in x$
38		oveq2	$⊢ y = suc A \to C +_{𝑜} y = C +_{𝑜} suc A$
39	38	ssiun2s	$⊢ suc A \in x \to C +_{𝑜} suc A \subseteq ⋃_{y \in x} (C +_{𝑜} y)$
40	37 39	syl	$⊢ ((Lim x \land suc A \in On) \land suc A \subseteq x) \to C +_{𝑜} suc A \subseteq ⋃_{y \in x} (C +_{𝑜} y)$
41	40	adantr	$⊢ (((Lim x \land suc A \in On) \land suc A \subseteq x) \land C \in On) \to C +_{𝑜} suc A \subseteq ⋃_{y \in x} (C +_{𝑜} y)$
42		vex	$⊢ x \in V$
43		oalim	$⊢ (C \in On \land (x \in V \land Lim x)) \to C +_{𝑜} x = ⋃_{y \in x} (C +_{𝑜} y)$
44	42 43	mpanr1	$⊢ (C \in On \land Lim x) \to C +_{𝑜} x = ⋃_{y \in x} (C +_{𝑜} y)$
45	44	ancoms	$⊢ (Lim x \land C \in On) \to C +_{𝑜} x = ⋃_{y \in x} (C +_{𝑜} y)$
46	45	adantlr	$⊢ ((Lim x \land suc A \in On) \land C \in On) \to C +_{𝑜} x = ⋃_{y \in x} (C +_{𝑜} y)$
47	46	adantlr	$⊢ (((Lim x \land suc A \in On) \land suc A \subseteq x) \land C \in On) \to C +_{𝑜} x = ⋃_{y \in x} (C +_{𝑜} y)$
48	41 47	sseqtrrd	$⊢ (((Lim x \land suc A \in On) \land suc A \subseteq x) \land C \in On) \to C +_{𝑜} suc A \subseteq C +_{𝑜} x$
49	48	ex	$⊢ ((Lim x \land suc A \in On) \land suc A \subseteq x) \to (C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} x)$
50	49	a1d	$⊢ ((Lim x \land suc A \in On) \land suc A \subseteq x) \to (\forall y \in x (suc A \subseteq y \to (C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} y)) \to (C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} x))$
51	10 13 16 19 21 31 50	tfindsg	$⊢ ((B \in On \land suc A \in On) \land suc A \subseteq B) \to (C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} B)$
52	51	exp31	$⊢ B \in On \to (suc A \in On \to (suc A \subseteq B \to (C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} B)))$
53	7 52	biimtrid	$⊢ B \in On \to (A \in On \to (suc A \subseteq B \to (C \in On \to C +_{𝑜} suc A \subseteq C +_{𝑜} B)))$
54	53	com4r	$⊢ C \in On \to (B \in On \to (A \in On \to (suc A \subseteq B \to C +_{𝑜} suc A \subseteq C +_{𝑜} B)))$
55	54	imp31	$⊢ ((C \in On \land B \in On) \land A \in On) \to (suc A \subseteq B \to C +_{𝑜} suc A \subseteq C +_{𝑜} B)$
56		oasuc	$⊢ (C \in On \land A \in On) \to C +_{𝑜} suc A = suc (C +_{𝑜} A)$
57	56	sseq1d	$⊢ (C \in On \land A \in On) \to (C +_{𝑜} suc A \subseteq C +_{𝑜} B \leftrightarrow suc (C +_{𝑜} A) \subseteq C +_{𝑜} B)$
58		ovex	$⊢ C +_{𝑜} A \in V$
59		sucssel	$⊢ C +_{𝑜} A \in V \to (suc (C +_{𝑜} A) \subseteq C +_{𝑜} B \to C +_{𝑜} A \in (C +_{𝑜} B))$
60	58 59	ax-mp	$⊢ suc (C +_{𝑜} A) \subseteq C +_{𝑜} B \to C +_{𝑜} A \in (C +_{𝑜} B)$
61	57 60	biimtrdi	$⊢ (C \in On \land A \in On) \to (C +_{𝑜} suc A \subseteq C +_{𝑜} B \to C +_{𝑜} A \in (C +_{𝑜} B))$
62	61	adantlr	$⊢ ((C \in On \land B \in On) \land A \in On) \to (C +_{𝑜} suc A \subseteq C +_{𝑜} B \to C +_{𝑜} A \in (C +_{𝑜} B))$
63	6 55 62	3syld	$⊢ ((C \in On \land B \in On) \land A \in On) \to (A \in B \to C +_{𝑜} A \in (C +_{𝑜} B))$
64	63	imp	$⊢ (((C \in On \land B \in On) \land A \in On) \land A \in B) \to C +_{𝑜} A \in (C +_{𝑜} B)$
65	64	an32s	$⊢ (((C \in On \land B \in On) \land A \in B) \land A \in On) \to C +_{𝑜} A \in (C +_{𝑜} B)$
66	2 65	mpdan	$⊢ ((C \in On \land B \in On) \land A \in B) \to C +_{𝑜} A \in (C +_{𝑜} B)$
67	66	ex	$⊢ (C \in On \land B \in On) \to (A \in B \to C +_{𝑜} A \in (C +_{𝑜} B))$
68	67	ancoms	$⊢ (B \in On \land C \in On) \to (A \in B \to C +_{𝑜} A \in (C +_{𝑜} B))$

Metamath Proof Explorer

Theorem oaordi

Proof