MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oaordi Structured version   Visualization version   GIF version

Theorem oaordi 8567
Description: Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58. (Contributed by NM, 5-Dec-2004.)
Assertion
Ref Expression
oaordi ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴𝐵 → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵)))

Proof of Theorem oaordi
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 onelon 6396 . . . . 5 ((𝐵 ∈ On ∧ 𝐴𝐵) → 𝐴 ∈ On)
21adantll 712 . . . 4 (((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴𝐵) → 𝐴 ∈ On)
3 eloni 6381 . . . . . . . . 9 (𝐵 ∈ On → Ord 𝐵)
4 ordsucss 7822 . . . . . . . . 9 (Ord 𝐵 → (𝐴𝐵 → suc 𝐴𝐵))
53, 4syl 17 . . . . . . . 8 (𝐵 ∈ On → (𝐴𝐵 → suc 𝐴𝐵))
65ad2antlr 725 . . . . . . 7 (((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → (𝐴𝐵 → suc 𝐴𝐵))
7 onsucb 7821 . . . . . . . . . 10 (𝐴 ∈ On ↔ suc 𝐴 ∈ On)
8 oveq2 7427 . . . . . . . . . . . . . 14 (𝑥 = suc 𝐴 → (𝐶 +o 𝑥) = (𝐶 +o suc 𝐴))
98sseq2d 4009 . . . . . . . . . . . . 13 (𝑥 = suc 𝐴 → ((𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑥) ↔ (𝐶 +o suc 𝐴) ⊆ (𝐶 +o suc 𝐴)))
109imbi2d 339 . . . . . . . . . . . 12 (𝑥 = suc 𝐴 → ((𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑥)) ↔ (𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o suc 𝐴))))
11 oveq2 7427 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝐶 +o 𝑥) = (𝐶 +o 𝑦))
1211sseq2d 4009 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑥) ↔ (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑦)))
1312imbi2d 339 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑥)) ↔ (𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑦))))
14 oveq2 7427 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (𝐶 +o 𝑥) = (𝐶 +o suc 𝑦))
1514sseq2d 4009 . . . . . . . . . . . . 13 (𝑥 = suc 𝑦 → ((𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑥) ↔ (𝐶 +o suc 𝐴) ⊆ (𝐶 +o suc 𝑦)))
1615imbi2d 339 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → ((𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑥)) ↔ (𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o suc 𝑦))))
17 oveq2 7427 . . . . . . . . . . . . . 14 (𝑥 = 𝐵 → (𝐶 +o 𝑥) = (𝐶 +o 𝐵))
1817sseq2d 4009 . . . . . . . . . . . . 13 (𝑥 = 𝐵 → ((𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑥) ↔ (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝐵)))
1918imbi2d 339 . . . . . . . . . . . 12 (𝑥 = 𝐵 → ((𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑥)) ↔ (𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝐵))))
20 ssid 3999 . . . . . . . . . . . . 13 (𝐶 +o suc 𝐴) ⊆ (𝐶 +o suc 𝐴)
21202a1i 12 . . . . . . . . . . . 12 (suc 𝐴 ∈ On → (𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o suc 𝐴)))
22 sssucid 6451 . . . . . . . . . . . . . . . . 17 (𝐶 +o 𝑦) ⊆ suc (𝐶 +o 𝑦)
23 sstr2 3983 . . . . . . . . . . . . . . . . 17 ((𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑦) → ((𝐶 +o 𝑦) ⊆ suc (𝐶 +o 𝑦) → (𝐶 +o suc 𝐴) ⊆ suc (𝐶 +o 𝑦)))
2422, 23mpi 20 . . . . . . . . . . . . . . . 16 ((𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑦) → (𝐶 +o suc 𝐴) ⊆ suc (𝐶 +o 𝑦))
25 oasuc 8545 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 +o suc 𝑦) = suc (𝐶 +o 𝑦))
2625ancoms 457 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ On ∧ 𝐶 ∈ On) → (𝐶 +o suc 𝑦) = suc (𝐶 +o 𝑦))
2726sseq2d 4009 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ On ∧ 𝐶 ∈ On) → ((𝐶 +o suc 𝐴) ⊆ (𝐶 +o suc 𝑦) ↔ (𝐶 +o suc 𝐴) ⊆ suc (𝐶 +o 𝑦)))
2824, 27imbitrrid 245 . . . . . . . . . . . . . . 15 ((𝑦 ∈ On ∧ 𝐶 ∈ On) → ((𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑦) → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o suc 𝑦)))
2928ex 411 . . . . . . . . . . . . . 14 (𝑦 ∈ On → (𝐶 ∈ On → ((𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑦) → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o suc 𝑦))))
3029ad2antrr 724 . . . . . . . . . . . . 13 (((𝑦 ∈ On ∧ suc 𝐴 ∈ On) ∧ suc 𝐴𝑦) → (𝐶 ∈ On → ((𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑦) → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o suc 𝑦))))
3130a2d 29 . . . . . . . . . . . 12 (((𝑦 ∈ On ∧ suc 𝐴 ∈ On) ∧ suc 𝐴𝑦) → ((𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑦)) → (𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o suc 𝑦))))
32 sucssel 6466 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ On → (suc 𝐴𝑥𝐴𝑥))
337, 32sylbir 234 . . . . . . . . . . . . . . . . . . 19 (suc 𝐴 ∈ On → (suc 𝐴𝑥𝐴𝑥))
34 limsuc 7854 . . . . . . . . . . . . . . . . . . . 20 (Lim 𝑥 → (𝐴𝑥 ↔ suc 𝐴𝑥))
3534biimpd 228 . . . . . . . . . . . . . . . . . . 19 (Lim 𝑥 → (𝐴𝑥 → suc 𝐴𝑥))
3633, 35sylan9r 507 . . . . . . . . . . . . . . . . . 18 ((Lim 𝑥 ∧ suc 𝐴 ∈ On) → (suc 𝐴𝑥 → suc 𝐴𝑥))
3736imp 405 . . . . . . . . . . . . . . . . 17 (((Lim 𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴𝑥) → suc 𝐴𝑥)
38 oveq2 7427 . . . . . . . . . . . . . . . . . 18 (𝑦 = suc 𝐴 → (𝐶 +o 𝑦) = (𝐶 +o suc 𝐴))
3938ssiun2s 5052 . . . . . . . . . . . . . . . . 17 (suc 𝐴𝑥 → (𝐶 +o suc 𝐴) ⊆ 𝑦𝑥 (𝐶 +o 𝑦))
4037, 39syl 17 . . . . . . . . . . . . . . . 16 (((Lim 𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴𝑥) → (𝐶 +o suc 𝐴) ⊆ 𝑦𝑥 (𝐶 +o 𝑦))
4140adantr 479 . . . . . . . . . . . . . . 15 ((((Lim 𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴𝑥) ∧ 𝐶 ∈ On) → (𝐶 +o suc 𝐴) ⊆ 𝑦𝑥 (𝐶 +o 𝑦))
42 vex 3465 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
43 oalim 8553 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐶 +o 𝑥) = 𝑦𝑥 (𝐶 +o 𝑦))
4442, 43mpanr1 701 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ On ∧ Lim 𝑥) → (𝐶 +o 𝑥) = 𝑦𝑥 (𝐶 +o 𝑦))
4544ancoms 457 . . . . . . . . . . . . . . . . 17 ((Lim 𝑥𝐶 ∈ On) → (𝐶 +o 𝑥) = 𝑦𝑥 (𝐶 +o 𝑦))
4645adantlr 713 . . . . . . . . . . . . . . . 16 (((Lim 𝑥 ∧ suc 𝐴 ∈ On) ∧ 𝐶 ∈ On) → (𝐶 +o 𝑥) = 𝑦𝑥 (𝐶 +o 𝑦))
4746adantlr 713 . . . . . . . . . . . . . . 15 ((((Lim 𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴𝑥) ∧ 𝐶 ∈ On) → (𝐶 +o 𝑥) = 𝑦𝑥 (𝐶 +o 𝑦))
4841, 47sseqtrrd 4018 . . . . . . . . . . . . . 14 ((((Lim 𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴𝑥) ∧ 𝐶 ∈ On) → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑥))
4948ex 411 . . . . . . . . . . . . 13 (((Lim 𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴𝑥) → (𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑥)))
5049a1d 25 . . . . . . . . . . . 12 (((Lim 𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴𝑥) → (∀𝑦𝑥 (suc 𝐴𝑦 → (𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑦))) → (𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝑥))))
5110, 13, 16, 19, 21, 31, 50tfindsg 7866 . . . . . . . . . . 11 (((𝐵 ∈ On ∧ suc 𝐴 ∈ On) ∧ suc 𝐴𝐵) → (𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝐵)))
5251exp31 418 . . . . . . . . . 10 (𝐵 ∈ On → (suc 𝐴 ∈ On → (suc 𝐴𝐵 → (𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝐵)))))
537, 52biimtrid 241 . . . . . . . . 9 (𝐵 ∈ On → (𝐴 ∈ On → (suc 𝐴𝐵 → (𝐶 ∈ On → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝐵)))))
5453com4r 94 . . . . . . . 8 (𝐶 ∈ On → (𝐵 ∈ On → (𝐴 ∈ On → (suc 𝐴𝐵 → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝐵)))))
5554imp31 416 . . . . . . 7 (((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → (suc 𝐴𝐵 → (𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝐵)))
56 oasuc 8545 . . . . . . . . . 10 ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶 +o suc 𝐴) = suc (𝐶 +o 𝐴))
5756sseq1d 4008 . . . . . . . . 9 ((𝐶 ∈ On ∧ 𝐴 ∈ On) → ((𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝐵) ↔ suc (𝐶 +o 𝐴) ⊆ (𝐶 +o 𝐵)))
58 ovex 7452 . . . . . . . . . 10 (𝐶 +o 𝐴) ∈ V
59 sucssel 6466 . . . . . . . . . 10 ((𝐶 +o 𝐴) ∈ V → (suc (𝐶 +o 𝐴) ⊆ (𝐶 +o 𝐵) → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵)))
6058, 59ax-mp 5 . . . . . . . . 9 (suc (𝐶 +o 𝐴) ⊆ (𝐶 +o 𝐵) → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))
6157, 60biimtrdi 252 . . . . . . . 8 ((𝐶 ∈ On ∧ 𝐴 ∈ On) → ((𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝐵) → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵)))
6261adantlr 713 . . . . . . 7 (((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → ((𝐶 +o suc 𝐴) ⊆ (𝐶 +o 𝐵) → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵)))
636, 55, 623syld 60 . . . . . 6 (((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → (𝐴𝐵 → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵)))
6463imp 405 . . . . 5 ((((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) ∧ 𝐴𝐵) → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))
6564an32s 650 . . . 4 ((((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴𝐵) ∧ 𝐴 ∈ On) → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))
662, 65mpdan 685 . . 3 (((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴𝐵) → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))
6766ex 411 . 2 ((𝐶 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝐵 → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵)))
6867ancoms 457 1 ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴𝐵 → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1533  wcel 2098  wral 3050  Vcvv 3461  wss 3944   ciun 4997  Ord word 6370  Oncon0 6371  Lim wlim 6372  suc csuc 6373  (class class class)co 7419   +o coa 8484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-oadd 8491
This theorem is referenced by:  oaord  8568  oaass  8582  odi  8600  onexomgt  42811  onexoegt  42814  oaltublim  42861  oaordi3  42862  oacl2g  42901  tfsconcatfv2  42911  tfsconcatrn  42913  tfsconcatrev  42919  ofoafg  42925  oaun3lem1  42945  oaun3lem2  42946  oadif1  42951  naddwordnexlem0  42968  naddwordnexlem3  42971  naddwordnexlem4  42973  oaltom  42977
  Copyright terms: Public domain W3C validator