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

Theorem oaass 8599
Description: Ordinal addition is associative. Theorem 25 of [Suppes] p. 211. Theorem 4.2 of [Schloeder] p. 11. (Contributed by NM, 10-Dec-2004.)
Assertion
Ref Expression
oaass ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶)))

Proof of Theorem oaass
Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7439 . . . . 5 (𝑥 = ∅ → ((𝐴 +o 𝐵) +o 𝑥) = ((𝐴 +o 𝐵) +o ∅))
2 oveq2 7439 . . . . . 6 (𝑥 = ∅ → (𝐵 +o 𝑥) = (𝐵 +o ∅))
32oveq2d 7447 . . . . 5 (𝑥 = ∅ → (𝐴 +o (𝐵 +o 𝑥)) = (𝐴 +o (𝐵 +o ∅)))
41, 3eqeq12d 2753 . . . 4 (𝑥 = ∅ → (((𝐴 +o 𝐵) +o 𝑥) = (𝐴 +o (𝐵 +o 𝑥)) ↔ ((𝐴 +o 𝐵) +o ∅) = (𝐴 +o (𝐵 +o ∅))))
5 oveq2 7439 . . . . 5 (𝑥 = 𝑦 → ((𝐴 +o 𝐵) +o 𝑥) = ((𝐴 +o 𝐵) +o 𝑦))
6 oveq2 7439 . . . . . 6 (𝑥 = 𝑦 → (𝐵 +o 𝑥) = (𝐵 +o 𝑦))
76oveq2d 7447 . . . . 5 (𝑥 = 𝑦 → (𝐴 +o (𝐵 +o 𝑥)) = (𝐴 +o (𝐵 +o 𝑦)))
85, 7eqeq12d 2753 . . . 4 (𝑥 = 𝑦 → (((𝐴 +o 𝐵) +o 𝑥) = (𝐴 +o (𝐵 +o 𝑥)) ↔ ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦))))
9 oveq2 7439 . . . . 5 (𝑥 = suc 𝑦 → ((𝐴 +o 𝐵) +o 𝑥) = ((𝐴 +o 𝐵) +o suc 𝑦))
10 oveq2 7439 . . . . . 6 (𝑥 = suc 𝑦 → (𝐵 +o 𝑥) = (𝐵 +o suc 𝑦))
1110oveq2d 7447 . . . . 5 (𝑥 = suc 𝑦 → (𝐴 +o (𝐵 +o 𝑥)) = (𝐴 +o (𝐵 +o suc 𝑦)))
129, 11eqeq12d 2753 . . . 4 (𝑥 = suc 𝑦 → (((𝐴 +o 𝐵) +o 𝑥) = (𝐴 +o (𝐵 +o 𝑥)) ↔ ((𝐴 +o 𝐵) +o suc 𝑦) = (𝐴 +o (𝐵 +o suc 𝑦))))
13 oveq2 7439 . . . . 5 (𝑥 = 𝐶 → ((𝐴 +o 𝐵) +o 𝑥) = ((𝐴 +o 𝐵) +o 𝐶))
14 oveq2 7439 . . . . . 6 (𝑥 = 𝐶 → (𝐵 +o 𝑥) = (𝐵 +o 𝐶))
1514oveq2d 7447 . . . . 5 (𝑥 = 𝐶 → (𝐴 +o (𝐵 +o 𝑥)) = (𝐴 +o (𝐵 +o 𝐶)))
1613, 15eqeq12d 2753 . . . 4 (𝑥 = 𝐶 → (((𝐴 +o 𝐵) +o 𝑥) = (𝐴 +o (𝐵 +o 𝑥)) ↔ ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶))))
17 oacl 8573 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) ∈ On)
18 oa0 8554 . . . . . 6 ((𝐴 +o 𝐵) ∈ On → ((𝐴 +o 𝐵) +o ∅) = (𝐴 +o 𝐵))
1917, 18syl 17 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) +o ∅) = (𝐴 +o 𝐵))
20 oa0 8554 . . . . . . 7 (𝐵 ∈ On → (𝐵 +o ∅) = 𝐵)
2120oveq2d 7447 . . . . . 6 (𝐵 ∈ On → (𝐴 +o (𝐵 +o ∅)) = (𝐴 +o 𝐵))
2221adantl 481 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o (𝐵 +o ∅)) = (𝐴 +o 𝐵))
2319, 22eqtr4d 2780 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) +o ∅) = (𝐴 +o (𝐵 +o ∅)))
24 suceq 6450 . . . . . 6 (((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦)) → suc ((𝐴 +o 𝐵) +o 𝑦) = suc (𝐴 +o (𝐵 +o 𝑦)))
25 oasuc 8562 . . . . . . . 8 (((𝐴 +o 𝐵) ∈ On ∧ 𝑦 ∈ On) → ((𝐴 +o 𝐵) +o suc 𝑦) = suc ((𝐴 +o 𝐵) +o 𝑦))
2617, 25sylan 580 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → ((𝐴 +o 𝐵) +o suc 𝑦) = suc ((𝐴 +o 𝐵) +o 𝑦))
27 oasuc 8562 . . . . . . . . . . 11 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +o suc 𝑦) = suc (𝐵 +o 𝑦))
2827oveq2d 7447 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 +o (𝐵 +o suc 𝑦)) = (𝐴 +o suc (𝐵 +o 𝑦)))
2928adantl 481 . . . . . . . . 9 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +o (𝐵 +o suc 𝑦)) = (𝐴 +o suc (𝐵 +o 𝑦)))
30 oacl 8573 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +o 𝑦) ∈ On)
31 oasuc 8562 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (𝐵 +o 𝑦) ∈ On) → (𝐴 +o suc (𝐵 +o 𝑦)) = suc (𝐴 +o (𝐵 +o 𝑦)))
3230, 31sylan2 593 . . . . . . . . 9 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +o suc (𝐵 +o 𝑦)) = suc (𝐴 +o (𝐵 +o 𝑦)))
3329, 32eqtrd 2777 . . . . . . . 8 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +o (𝐵 +o suc 𝑦)) = suc (𝐴 +o (𝐵 +o 𝑦)))
3433anassrs 467 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (𝐴 +o (𝐵 +o suc 𝑦)) = suc (𝐴 +o (𝐵 +o 𝑦)))
3526, 34eqeq12d 2753 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (((𝐴 +o 𝐵) +o suc 𝑦) = (𝐴 +o (𝐵 +o suc 𝑦)) ↔ suc ((𝐴 +o 𝐵) +o 𝑦) = suc (𝐴 +o (𝐵 +o 𝑦))))
3624, 35imbitrrid 246 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦)) → ((𝐴 +o 𝐵) +o suc 𝑦) = (𝐴 +o (𝐵 +o suc 𝑦))))
3736expcom 413 . . . 4 (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦)) → ((𝐴 +o 𝐵) +o suc 𝑦) = (𝐴 +o (𝐵 +o suc 𝑦)))))
38 iuneq2 5011 . . . . . . 7 (∀𝑦𝑥 ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦)) → 𝑦𝑥 ((𝐴 +o 𝐵) +o 𝑦) = 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)))
3938adantl 481 . . . . . 6 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦))) → 𝑦𝑥 ((𝐴 +o 𝐵) +o 𝑦) = 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)))
40 vex 3484 . . . . . . . . . 10 𝑥 ∈ V
41 oalim 8570 . . . . . . . . . 10 (((𝐴 +o 𝐵) ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → ((𝐴 +o 𝐵) +o 𝑥) = 𝑦𝑥 ((𝐴 +o 𝐵) +o 𝑦))
4240, 41mpanr1 703 . . . . . . . . 9 (((𝐴 +o 𝐵) ∈ On ∧ Lim 𝑥) → ((𝐴 +o 𝐵) +o 𝑥) = 𝑦𝑥 ((𝐴 +o 𝐵) +o 𝑦))
4317, 42sylan 580 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝑥) → ((𝐴 +o 𝐵) +o 𝑥) = 𝑦𝑥 ((𝐴 +o 𝐵) +o 𝑦))
4443ancoms 458 . . . . . . 7 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 +o 𝐵) +o 𝑥) = 𝑦𝑥 ((𝐴 +o 𝐵) +o 𝑦))
4544adantr 480 . . . . . 6 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦))) → ((𝐴 +o 𝐵) +o 𝑥) = 𝑦𝑥 ((𝐴 +o 𝐵) +o 𝑦))
46 oalimcl 8598 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (𝐵 +o 𝑥))
4740, 46mpanr1 703 . . . . . . . . . . 11 ((𝐵 ∈ On ∧ Lim 𝑥) → Lim (𝐵 +o 𝑥))
4847ancoms 458 . . . . . . . . . 10 ((Lim 𝑥𝐵 ∈ On) → Lim (𝐵 +o 𝑥))
49 ovex 7464 . . . . . . . . . . 11 (𝐵 +o 𝑥) ∈ V
50 oalim 8570 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ ((𝐵 +o 𝑥) ∈ V ∧ Lim (𝐵 +o 𝑥))) → (𝐴 +o (𝐵 +o 𝑥)) = 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧))
5149, 50mpanr1 703 . . . . . . . . . 10 ((𝐴 ∈ On ∧ Lim (𝐵 +o 𝑥)) → (𝐴 +o (𝐵 +o 𝑥)) = 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧))
5248, 51sylan2 593 . . . . . . . . 9 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → (𝐴 +o (𝐵 +o 𝑥)) = 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧))
53 limelon 6448 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
5440, 53mpan 690 . . . . . . . . . . . . . . . 16 (Lim 𝑥𝑥 ∈ On)
55 oacl 8573 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 +o 𝑥) ∈ On)
5655ancoms 458 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +o 𝑥) ∈ On)
57 onelon 6409 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐵 +o 𝑥) ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑧 ∈ On)
5857ex 412 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 +o 𝑥) ∈ On → (𝑧 ∈ (𝐵 +o 𝑥) → 𝑧 ∈ On))
5956, 58syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +o 𝑥) → 𝑧 ∈ On))
6059adantld 490 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑧 ∈ On))
6160adantl 481 . . . . . . . . . . . . . . . . . 18 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑧 ∈ On))
62 0ellim 6447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑥 → ∅ ∈ 𝑥)
63 onelss 6426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐵 ∈ On → (𝑧𝐵𝑧𝐵))
6420sseq2d 4016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐵 ∈ On → (𝑧 ⊆ (𝐵 +o ∅) ↔ 𝑧𝐵))
6563, 64sylibrd 259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐵 ∈ On → (𝑧𝐵𝑧 ⊆ (𝐵 +o ∅)))
6665imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐵 ∈ On ∧ 𝑧𝐵) → 𝑧 ⊆ (𝐵 +o ∅))
67 oveq2 7439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → (𝐵 +o 𝑦) = (𝐵 +o ∅))
6867sseq2d 4016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → (𝑧 ⊆ (𝐵 +o 𝑦) ↔ 𝑧 ⊆ (𝐵 +o ∅)))
6968rspcev 3622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∅ ∈ 𝑥𝑧 ⊆ (𝐵 +o ∅)) → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦))
7062, 66, 69syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Lim 𝑥 ∧ (𝐵 ∈ On ∧ 𝑧𝐵)) → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦))
7170expr 456 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Lim 𝑥𝐵 ∈ On) → (𝑧𝐵 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦)))
7271adantrl 716 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧𝐵 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦)))
7372adantrr 717 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim 𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On))) → (𝑧𝐵 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦)))
74 oawordex 8595 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝐵𝑧 ↔ ∃𝑦 ∈ On (𝐵 +o 𝑦) = 𝑧))
7574ad2ant2l 746 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On)) → (𝐵𝑧 ↔ ∃𝑦 ∈ On (𝐵 +o 𝑦) = 𝑧))
76 oaord 8585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦𝑥 ↔ (𝐵 +o 𝑦) ∈ (𝐵 +o 𝑥)))
77763expb 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑦 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑦𝑥 ↔ (𝐵 +o 𝑦) ∈ (𝐵 +o 𝑥)))
78 eleq1 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐵 +o 𝑦) = 𝑧 → ((𝐵 +o 𝑦) ∈ (𝐵 +o 𝑥) ↔ 𝑧 ∈ (𝐵 +o 𝑥)))
7977, 78sylan9bb 509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑦 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +o 𝑦) = 𝑧) → (𝑦𝑥𝑧 ∈ (𝐵 +o 𝑥)))
8079an32s 652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑦 ∈ On ∧ (𝐵 +o 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑦𝑥𝑧 ∈ (𝐵 +o 𝑥)))
8180biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑦 ∈ On ∧ (𝐵 +o 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑦𝑥)
82 eqimss2 4043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐵 +o 𝑦) = 𝑧𝑧 ⊆ (𝐵 +o 𝑦))
8382ad3antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑦 ∈ On ∧ (𝐵 +o 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑧 ⊆ (𝐵 +o 𝑦))
8481, 83jca 511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑦 ∈ On ∧ (𝐵 +o 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑦𝑥𝑧 ⊆ (𝐵 +o 𝑦)))
8584anasss 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑦 ∈ On ∧ (𝐵 +o 𝑦) = 𝑧) ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥))) → (𝑦𝑥𝑧 ⊆ (𝐵 +o 𝑦)))
8685expcom 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → ((𝑦 ∈ On ∧ (𝐵 +o 𝑦) = 𝑧) → (𝑦𝑥𝑧 ⊆ (𝐵 +o 𝑦))))
8786reximdv2 3164 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (∃𝑦 ∈ On (𝐵 +o 𝑦) = 𝑧 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦)))
8887adantrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On)) → (∃𝑦 ∈ On (𝐵 +o 𝑦) = 𝑧 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦)))
8975, 88sylbid 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On)) → (𝐵𝑧 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦)))
9089adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim 𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On))) → (𝐵𝑧 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦)))
91 eloni 6394 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ On → Ord 𝑧)
92 eloni 6394 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐵 ∈ On → Ord 𝐵)
93 ordtri2or 6482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Ord 𝑧 ∧ Ord 𝐵) → (𝑧𝐵𝐵𝑧))
9491, 92, 93syl2anr 597 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝑧𝐵𝐵𝑧))
9594ad2ant2l 746 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On)) → (𝑧𝐵𝐵𝑧))
9695adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim 𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On))) → (𝑧𝐵𝐵𝑧))
9773, 90, 96mpjaod 861 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Lim 𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On))) → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦))
9897exp45 438 . . . . . . . . . . . . . . . . . . . . . . 23 (Lim 𝑥 → ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +o 𝑥) → (𝑧 ∈ On → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦)))))
9998imp 406 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧 ∈ (𝐵 +o 𝑥) → (𝑧 ∈ On → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦))))
10099adantld 490 . . . . . . . . . . . . . . . . . . . . 21 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑧 ∈ On → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦))))
101100imp32 418 . . . . . . . . . . . . . . . . . . . 20 (((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦))
102 simplrr 778 . . . . . . . . . . . . . . . . . . . . . 22 ((((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦𝑥) → 𝑧 ∈ On)
103 onelon 6409 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
104103, 30sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐵 ∈ On ∧ (𝑥 ∈ On ∧ 𝑦𝑥)) → (𝐵 +o 𝑦) ∈ On)
105104exp32 420 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵 ∈ On → (𝑥 ∈ On → (𝑦𝑥 → (𝐵 +o 𝑦) ∈ On)))
106105com12 32 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ On → (𝐵 ∈ On → (𝑦𝑥 → (𝐵 +o 𝑦) ∈ On)))
107106imp31 417 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦𝑥) → (𝐵 +o 𝑦) ∈ On)
108107ad4ant24 754 . . . . . . . . . . . . . . . . . . . . . 22 ((((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦𝑥) → (𝐵 +o 𝑦) ∈ On)
109 simpll 767 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On) → 𝐴 ∈ On)
110109ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . 22 ((((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦𝑥) → 𝐴 ∈ On)
111 oaword 8587 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 ∈ On ∧ (𝐵 +o 𝑦) ∈ On ∧ 𝐴 ∈ On) → (𝑧 ⊆ (𝐵 +o 𝑦) ↔ (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦))))
112102, 108, 110, 111syl3anc 1373 . . . . . . . . . . . . . . . . . . . . 21 ((((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦𝑥) → (𝑧 ⊆ (𝐵 +o 𝑦) ↔ (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦))))
113112rexbidva 3177 . . . . . . . . . . . . . . . . . . . 20 (((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) → (∃𝑦𝑥 𝑧 ⊆ (𝐵 +o 𝑦) ↔ ∃𝑦𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦))))
114101, 113mpbid 232 . . . . . . . . . . . . . . . . . . 19 (((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) → ∃𝑦𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦)))
115114exp32 420 . . . . . . . . . . . . . . . . . 18 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑧 ∈ On → ∃𝑦𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦)))))
11661, 115mpdd 43 . . . . . . . . . . . . . . . . 17 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → ∃𝑦𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦))))
117116exp32 420 . . . . . . . . . . . . . . . 16 (Lim 𝑥 → (𝑥 ∈ On → (𝐵 ∈ On → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → ∃𝑦𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦))))))
11854, 117mpd 15 . . . . . . . . . . . . . . 15 (Lim 𝑥 → (𝐵 ∈ On → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → ∃𝑦𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦)))))
119118exp4a 431 . . . . . . . . . . . . . 14 (Lim 𝑥 → (𝐵 ∈ On → (𝐴 ∈ On → (𝑧 ∈ (𝐵 +o 𝑥) → ∃𝑦𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦))))))
120119imp31 417 . . . . . . . . . . . . 13 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐴 ∈ On) → (𝑧 ∈ (𝐵 +o 𝑥) → ∃𝑦𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦))))
121120ralrimiv 3145 . . . . . . . . . . . 12 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐴 ∈ On) → ∀𝑧 ∈ (𝐵 +o 𝑥)∃𝑦𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦)))
122 iunss2 5049 . . . . . . . . . . . 12 (∀𝑧 ∈ (𝐵 +o 𝑥)∃𝑦𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦)) → 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧) ⊆ 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)))
123121, 122syl 17 . . . . . . . . . . 11 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐴 ∈ On) → 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧) ⊆ 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)))
124123ancoms 458 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧) ⊆ 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)))
125 oaordi 8584 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦𝑥 → (𝐵 +o 𝑦) ∈ (𝐵 +o 𝑥)))
126125anim1d 611 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝑦𝑥𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦))) → ((𝐵 +o 𝑦) ∈ (𝐵 +o 𝑥) ∧ 𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦)))))
127 oveq2 7439 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐵 +o 𝑦) → (𝐴 +o 𝑧) = (𝐴 +o (𝐵 +o 𝑦)))
128127eleq2d 2827 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝐵 +o 𝑦) → (𝑤 ∈ (𝐴 +o 𝑧) ↔ 𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦))))
129128rspcev 3622 . . . . . . . . . . . . . . . . 17 (((𝐵 +o 𝑦) ∈ (𝐵 +o 𝑥) ∧ 𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦))) → ∃𝑧 ∈ (𝐵 +o 𝑥)𝑤 ∈ (𝐴 +o 𝑧))
130126, 129syl6 35 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝑦𝑥𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦))) → ∃𝑧 ∈ (𝐵 +o 𝑥)𝑤 ∈ (𝐴 +o 𝑧)))
131130expd 415 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦𝑥 → (𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦)) → ∃𝑧 ∈ (𝐵 +o 𝑥)𝑤 ∈ (𝐴 +o 𝑧))))
132131rexlimdv 3153 . . . . . . . . . . . . . 14 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (∃𝑦𝑥 𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦)) → ∃𝑧 ∈ (𝐵 +o 𝑥)𝑤 ∈ (𝐴 +o 𝑧)))
133 eliun 4995 . . . . . . . . . . . . . 14 (𝑤 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)) ↔ ∃𝑦𝑥 𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦)))
134 eliun 4995 . . . . . . . . . . . . . 14 (𝑤 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧) ↔ ∃𝑧 ∈ (𝐵 +o 𝑥)𝑤 ∈ (𝐴 +o 𝑧))
135132, 133, 1343imtr4g 296 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑤 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)) → 𝑤 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧)))
136135ssrdv 3989 . . . . . . . . . . . 12 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)) ⊆ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧))
13754, 136sylan 580 . . . . . . . . . . 11 ((Lim 𝑥𝐵 ∈ On) → 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)) ⊆ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧))
138137adantl 481 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)) ⊆ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧))
139124, 138eqssd 4001 . . . . . . . . 9 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧) = 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)))
14052, 139eqtrd 2777 . . . . . . . 8 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → (𝐴 +o (𝐵 +o 𝑥)) = 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)))
141140an12s 649 . . . . . . 7 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 +o (𝐵 +o 𝑥)) = 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)))
142141adantr 480 . . . . . 6 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦))) → (𝐴 +o (𝐵 +o 𝑥)) = 𝑦𝑥 (𝐴 +o (𝐵 +o 𝑦)))
14339, 45, 1423eqtr4d 2787 . . . . 5 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦))) → ((𝐴 +o 𝐵) +o 𝑥) = (𝐴 +o (𝐵 +o 𝑥)))
144143exp31 419 . . . 4 (Lim 𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∀𝑦𝑥 ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦)) → ((𝐴 +o 𝐵) +o 𝑥) = (𝐴 +o (𝐵 +o 𝑥)))))
1454, 8, 12, 16, 23, 37, 144tfinds3 7886 . . 3 (𝐶 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶))))
146145com12 32 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐶 ∈ On → ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶))))
1471463impia 1118 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wcel 2108  wral 3061  wrex 3070  Vcvv 3480  wss 3951  c0 4333   ciun 4991  Ord word 6383  Oncon0 6384  Lim wlim 6385  suc csuc 6386  (class class class)co 7431   +o coa 8503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-oadd 8510
This theorem is referenced by:  odi  8617  oaabs  8686  oaabs2  8687  oaabsb  43307  omabs2  43345  ofoaass  43373  naddwordnexlem3  43412  naddwordnexlem4  43414
  Copyright terms: Public domain W3C validator