Theorem oaordi 3148

Description: Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58.

Assertion

Ref	Expression
oaordi	⊢ ((B ∈ On ∧ C ∈ On) → (A ∈ B → (C +o A) ∈ (C +o B)))

Proof of Theorem oaordi

Step	Hyp	Ref	Expression
1		onelon 2223	. . . . 5 ⊢ ((B ∈ On ∧ A ∈ B) → A ∈ On)
2	1	adantll 309	. . . 4 ⊢ (((C ∈ On ∧ B ∈ On) ∧ A ∈ B) → A ∈ On)
3		eloni 2209	. . . . . . . . . 10 ⊢ (B ∈ On → Ord B)
4		ordsucss 2320	. . . . . . . . . 10 ⊢ (Ord B → (A ∈ B → suc A ⊆ B))
5	3, 4	syl 12	. . . . . . . . 9 ⊢ (B ∈ On → (A ∈ B → suc A ⊆ B))
6	5	ad2antlr 321	. . . . . . . 8 ⊢ (((C ∈ On ∧ B ∈ On) ∧ A ∈ On) → (A ∈ B → suc A ⊆ B))
7		opreq2 3007	. . . . . . . . . . . . . . 15 ⊢ (x = suc A → (C +o x) = (C +o suc A))
8	7	sseq2d 1528	. . . . . . . . . . . . . 14 ⊢ (x = suc A → ((C +o suc A) ⊆ (C +o x) ↔ (C +o suc A) ⊆ (C +o suc A)))
9	8	imbi2d 464	. . . . . . . . . . . . 13 ⊢ (x = suc A → ((C ∈ On → (C +o suc A) ⊆ (C +o x)) ↔ (C ∈ On → (C +o suc A) ⊆ (C +o suc A))))
10		opreq2 3007	. . . . . . . . . . . . . . 15 ⊢ (x = y → (C +o x) = (C +o y))
11	10	sseq2d 1528	. . . . . . . . . . . . . 14 ⊢ (x = y → ((C +o suc A) ⊆ (C +o x) ↔ (C +o suc A) ⊆ (C +o y)))
12	11	imbi2d 464	. . . . . . . . . . . . 13 ⊢ (x = y → ((C ∈ On → (C +o suc A) ⊆ (C +o x)) ↔ (C ∈ On → (C +o suc A) ⊆ (C +o y))))
13		opreq2 3007	. . . . . . . . . . . . . . 15 ⊢ (x = suc y → (C +o x) = (C +o suc y))
14	13	sseq2d 1528	. . . . . . . . . . . . . 14 ⊢ (x = suc y → ((C +o suc A) ⊆ (C +o x) ↔ (C +o suc A) ⊆ (C +o suc y)))
15	14	imbi2d 464	. . . . . . . . . . . . 13 ⊢ (x = suc y → ((C ∈ On → (C +o suc A) ⊆ (C +o x)) ↔ (C ∈ On → (C +o suc A) ⊆ (C +o suc y))))
16		opreq2 3007	. . . . . . . . . . . . . . 15 ⊢ (x = B → (C +o x) = (C +o B))
17	16	sseq2d 1528	. . . . . . . . . . . . . 14 ⊢ (x = B → ((C +o suc A) ⊆ (C +o x) ↔ (C +o suc A) ⊆ (C +o B)))
18	17	imbi2d 464	. . . . . . . . . . . . 13 ⊢ (x = B → ((C ∈ On → (C +o suc A) ⊆ (C +o x)) ↔ (C ∈ On → (C +o suc A) ⊆ (C +o B))))
19		ssid 1519	. . . . . . . . . . . . . . 15 ⊢ (C +o suc A) ⊆ (C +o suc A)
20	19	a1i 7	. . . . . . . . . . . . . 14 ⊢ (C ∈ On → (C +o suc A) ⊆ (C +o suc A))
21	20	a1i 7	. . . . . . . . . . . . 13 ⊢ (suc A ∈ On → (C ∈ On → (C +o suc A) ⊆ (C +o suc A)))
22		oasuc 3131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((C ∈ On ∧ y ∈ On) → (C +o suc y) = suc (C +o y))
23	22	ancoms 334	. . . . . . . . . . . . . . . . . 18 ⊢ ((y ∈ On ∧ C ∈ On) → (C +o suc y) = suc (C +o y))
24	23	sseq2d 1528	. . . . . . . . . . . . . . . . 17 ⊢ ((y ∈ On ∧ C ∈ On) → ((C +o suc A) ⊆ (C +o suc y) ↔ (C +o suc A) ⊆ suc (C +o y)))
25		sssucid 2300	. . . . . . . . . . . . . . . . . 18 ⊢ (C +o y) ⊆ suc (C +o y)
26		sstr2 1510	. . . . . . . . . . . . . . . . . 18 ⊢ ((C +o suc A) ⊆ (C +o y) → ((C +o y) ⊆ suc (C +o y) → (C +o suc A) ⊆ suc (C +o y)))
27	25, 26	mpi 44	. . . . . . . . . . . . . . . . 17 ⊢ ((C +o suc A) ⊆ (C +o y) → (C +o suc A) ⊆ suc (C +o y))
28	24, 27	syl5bir 184	. . . . . . . . . . . . . . . 16 ⊢ ((y ∈ On ∧ C ∈ On) → ((C +o suc A) ⊆ (C +o y) → (C +o suc A) ⊆ (C +o suc y)))
29	28	exp 291	. . . . . . . . . . . . . . 15 ⊢ (y ∈ On → (C ∈ On → ((C +o suc A) ⊆ (C +o y) → (C +o suc A) ⊆ (C +o suc y))))
30	29	ad2antll 320	. . . . . . . . . . . . . 14 ⊢ (((y ∈ On ∧ suc A ∈ On) ∧ suc A ⊆ y) → (C ∈ On → ((C +o suc A) ⊆ (C +o y) → (C +o suc A) ⊆ (C +o suc y))))
31	30	a2d 15	. . . . . . . . . . . . 13 ⊢ (((y ∈ On ∧ suc A ∈ On) ∧ suc A ⊆ y) → ((C ∈ On → (C +o suc A) ⊆ (C +o y)) → (C ∈ On → (C +o suc A) ⊆ (C +o suc y))))
32		sucelon 2319	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (A ∈ On ↔ suc A ∈ On)
33		sucssel 2321	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (A ∈ On → (suc A ⊆ x → A ∈ x))
34	32, 33	sylbir 176	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc A ∈ On → (suc A ⊆ x → A ∈ x))
35		limsuc 2361	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Lim x → (A ∈ x ↔ suc A ∈ x))
36	35	biimpd 135	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim x → (A ∈ x → suc A ∈ x))
37	34, 36	sylan9r 360	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Lim x ∧ suc A ∈ On) → (suc A ⊆ x → suc A ∈ x))
38	37	imp 277	. . . . . . . . . . . . . . . . . 18 ⊢ (((Lim x ∧ suc A ∈ On) ∧ suc A ⊆ x) → suc A ∈ x)
39		opreq2 3007	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = suc A → (C +o y) = (C +o suc A))
40	39	ssiun2s 2020	. . . . . . . . . . . . . . . . . 18 ⊢ (suc A ∈ x → (C +o suc A) ⊆ ∪y ∈ x (C +o y))
41	38, 40	syl 12	. . . . . . . . . . . . . . . . 17 ⊢ (((Lim x ∧ suc A ∈ On) ∧ suc A ⊆ x) → (C +o suc A) ⊆ ∪y ∈ x (C +o y))
42	41	adantr 306	. . . . . . . . . . . . . . . 16 ⊢ ((((Lim x ∧ suc A ∈ On) ∧ suc A ⊆ x) ∧ C ∈ On) → (C +o suc A) ⊆ ∪y ∈ x (C +o y))
43		visset 1350	. . . . . . . . . . . . . . . . . . . 20 ⊢ x ∈ V
44		oalim 3135	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((C ∈ On ∧ (x ∈ V ∧ Lim x)) → (C +o x) = ∪y ∈ x (C +o y))
45	43, 44	mpan21 531	. . . . . . . . . . . . . . . . . . 19 ⊢ ((C ∈ On ∧ Lim x) → (C +o x) = ∪y ∈ x (C +o y))
46	45	ancoms 334	. . . . . . . . . . . . . . . . . 18 ⊢ ((Lim x ∧ C ∈ On) → (C +o x) = ∪y ∈ x (C +o y))
47	46	adantlr 310	. . . . . . . . . . . . . . . . 17 ⊢ (((Lim x ∧ suc A ∈ On) ∧ C ∈ On) → (C +o x) = ∪y ∈ x (C +o y))
48	47	adantlr 310	. . . . . . . . . . . . . . . 16 ⊢ ((((Lim x ∧ suc A ∈ On) ∧ suc A ⊆ x) ∧ C ∈ On) → (C +o x) = ∪y ∈ x (C +o y))
49	42, 48	sseqtr4d 1537	. . . . . . . . . . . . . . 15 ⊢ ((((Lim x ∧ suc A ∈ On) ∧ suc A ⊆ x) ∧ C ∈ On) → (C +o suc A) ⊆ (C +o x))
50	49	exp 291	. . . . . . . . . . . . . 14 ⊢ (((Lim x ∧ suc A ∈ On) ∧ suc A ⊆ x) → (C ∈ On → (C +o suc A) ⊆ (C +o x)))
51	50	a1d 14	. . . . . . . . . . . . 13 ⊢ (((Lim x ∧ suc A ∈ On) ∧ suc A ⊆ x) → (∀y ∈ x (suc A ⊆ y → (C ∈ On → (C +o suc A) ⊆ (C +o y))) → (C ∈ On → (C +o suc A) ⊆ (C +o x))))
52	9, 12, 15, 18, 21, 31, 51	tfindsg 2402	. . . . . . . . . . . 12 ⊢ (((B ∈ On ∧ suc A ∈ On) ∧ suc A ⊆ B) → (C ∈ On → (C +o suc A) ⊆ (C +o B)))
53	52	exp31 293	. . . . . . . . . . 11 ⊢ (B ∈ On → (suc A ∈ On → (suc A ⊆ B → (C ∈ On → (C +o suc A) ⊆ (C +o B)))))
54	53, 32	syl5ib 181	. . . . . . . . . 10 ⊢ (B ∈ On → (A ∈ On → (suc A ⊆ B → (C ∈ On → (C +o suc A) ⊆ (C +o B)))))
55	54	com4r 41	. . . . . . . . 9 ⊢ (C ∈ On → (B ∈ On → (A ∈ On → (suc A ⊆ B → (C +o suc A) ⊆ (C +o B)))))
56	55	imp31 280	. . . . . . . 8 ⊢ (((C ∈ On ∧ B ∈ On) ∧ A ∈ On) → (suc A ⊆ B → (C +o suc A) ⊆ (C +o B)))
57	6, 56	syld 27	. . . . . . 7 ⊢ (((C ∈ On ∧ B ∈ On) ∧ A ∈ On) → (A ∈ B → (C +o suc A) ⊆ (C +o B)))
58		oasuc 3131	. . . . . . . . . 10 ⊢ ((C ∈ On ∧ A ∈ On) → (C +o suc A) = suc (C +o A))
59	58	sseq1d 1527	. . . . . . . . 9 ⊢ ((C ∈ On ∧ A ∈ On) → ((C +o suc A) ⊆ (C +o B) ↔ suc (C +o A) ⊆ (C +o B)))
60		oprex 3018	. . . . . . . . . 10 ⊢ (C +o A) ∈ V
61		sucssel 2321	. . . . . . . . . 10 ⊢ ((C +o A) ∈ V → (suc (C +o A) ⊆ (C +o B) → (C +o A) ∈ (C +o B)))
62	60, 61	ax-mp 6	. . . . . . . . 9 ⊢ (suc (C +o A) ⊆ (C +o B) → (C +o A) ∈ (C +o B))
63	59, 62	syl6bi 187	. . . . . . . 8 ⊢ ((C ∈ On ∧ A ∈ On) → ((C +o suc A) ⊆ (C +o B) → (C +o A) ∈ (C +o B)))
64	63	adantlr 310	. . . . . . 7 ⊢ (((C ∈ On ∧ B ∈ On) ∧ A ∈ On) → ((C +o suc A) ⊆ (C +o B) → (C +o A) ∈ (C +o B)))
65	57, 64	syld 27	. . . . . 6 ⊢ (((C ∈ On ∧ B ∈ On) ∧ A ∈ On) → (A ∈ B → (C +o A) ∈ (C +o B)))
66	65	imp 277	. . . . 5 ⊢ ((((C ∈ On ∧ B ∈ On) ∧ A ∈ On) ∧ A ∈ B) → (C +o A) ∈ (C +o B))
67	66	an1rs 373	. . . 4 ⊢ ((((C ∈ On ∧ B ∈ On) ∧ A ∈ B) ∧ A ∈ On) → (C +o A) ∈ (C +o B))
68	2, 67	mpdan 527	. . 3 ⊢ (((C ∈ On ∧ B ∈ On) ∧ A ∈ B) → (C +o A) ∈ (C +o B))
69	68	exp 291	. 2 ⊢ ((C ∈ On ∧ B ∈ On) → (A ∈ B → (C +o A) ∈ (C +o B)))
70	69	ancoms 334	1 ⊢ ((B ∈ On ∧ C ∈ On) → (A ∈ B → (C +o A) ∈ (C +o B)))

Syntax hints:   → wi 2   ∧ wa 196   = weq 797   = wceq 1091   ∈ wcel 1092  ∀wral 1201  Vcvv 1348   ⊆ wss 1487  ∪ciun 1994  Ord word 2198  Oncon0 2199  Lim wlim 2200  suc csuc 2201  (class class class)co 3001   +_o coa 3101

This theorem is referenced by:  oaord 3149  oaass 3163  nnaordi 3176

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-fv 2438  df-rdg 2970  df-opr 3003  df-oprab 3004  df-oadd 3106

metamath.org