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

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

Proof of Theorem oaass
Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6531 . . . . 5 (𝑥 = ∅ → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ((𝐴 +𝑜 𝐵) +𝑜 ∅))
2 oveq2 6531 . . . . . 6 (𝑥 = ∅ → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 ∅))
32oveq2d 6539 . . . . 5 (𝑥 = ∅ → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 +𝑜 (𝐵 +𝑜 ∅)))
41, 3eqeq12d 2620 . . . 4 (𝑥 = ∅ → (((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) ↔ ((𝐴 +𝑜 𝐵) +𝑜 ∅) = (𝐴 +𝑜 (𝐵 +𝑜 ∅))))
5 oveq2 6531 . . . . 5 (𝑥 = 𝑦 → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
6 oveq2 6531 . . . . . 6 (𝑥 = 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝑦))
76oveq2d 6539 . . . . 5 (𝑥 = 𝑦 → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
85, 7eqeq12d 2620 . . . 4 (𝑥 = 𝑦 → (((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) ↔ ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
9 oveq2 6531 . . . . 5 (𝑥 = suc 𝑦 → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦))
10 oveq2 6531 . . . . . 6 (𝑥 = suc 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 suc 𝑦))
1110oveq2d 6539 . . . . 5 (𝑥 = suc 𝑦 → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)))
129, 11eqeq12d 2620 . . . 4 (𝑥 = suc 𝑦 → (((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) ↔ ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦))))
13 oveq2 6531 . . . . 5 (𝑥 = 𝐶 → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ((𝐴 +𝑜 𝐵) +𝑜 𝐶))
14 oveq2 6531 . . . . . 6 (𝑥 = 𝐶 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝐶))
1514oveq2d 6539 . . . . 5 (𝑥 = 𝐶 → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶)))
1613, 15eqeq12d 2620 . . . 4 (𝑥 = 𝐶 → (((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) ↔ ((𝐴 +𝑜 𝐵) +𝑜 𝐶) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶))))
17 oacl 7475 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 𝐵) ∈ On)
18 oa0 7456 . . . . . 6 ((𝐴 +𝑜 𝐵) ∈ On → ((𝐴 +𝑜 𝐵) +𝑜 ∅) = (𝐴 +𝑜 𝐵))
1917, 18syl 17 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 ∅) = (𝐴 +𝑜 𝐵))
20 oa0 7456 . . . . . . 7 (𝐵 ∈ On → (𝐵 +𝑜 ∅) = 𝐵)
2120oveq2d 6539 . . . . . 6 (𝐵 ∈ On → (𝐴 +𝑜 (𝐵 +𝑜 ∅)) = (𝐴 +𝑜 𝐵))
2221adantl 480 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 (𝐵 +𝑜 ∅)) = (𝐴 +𝑜 𝐵))
2319, 22eqtr4d 2642 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 ∅) = (𝐴 +𝑜 (𝐵 +𝑜 ∅)))
24 suceq 5689 . . . . . 6 (((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → suc ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
25 oasuc 7464 . . . . . . . 8 (((𝐴 +𝑜 𝐵) ∈ On ∧ 𝑦 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = suc ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
2617, 25sylan 486 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = suc ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
27 oasuc 7464 . . . . . . . . . . 11 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦))
2827oveq2d 6539 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) = (𝐴 +𝑜 suc (𝐵 +𝑜 𝑦)))
2928adantl 480 . . . . . . . . 9 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) = (𝐴 +𝑜 suc (𝐵 +𝑜 𝑦)))
30 oacl 7475 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 𝑦) ∈ On)
31 oasuc 7464 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (𝐵 +𝑜 𝑦) ∈ On) → (𝐴 +𝑜 suc (𝐵 +𝑜 𝑦)) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
3230, 31sylan2 489 . . . . . . . . 9 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +𝑜 suc (𝐵 +𝑜 𝑦)) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
3329, 32eqtrd 2639 . . . . . . . 8 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
3433anassrs 677 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
3526, 34eqeq12d 2620 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) ↔ suc ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
3624, 35syl5ibr 234 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦))))
3736expcom 449 . . . 4 (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)))))
38 vex 3171 . . . . . . . . . 10 𝑥 ∈ V
39 oalim 7472 . . . . . . . . . 10 (((𝐴 +𝑜 𝐵) ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
4038, 39mpanr1 714 . . . . . . . . 9 (((𝐴 +𝑜 𝐵) ∈ On ∧ Lim 𝑥) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
4117, 40sylan 486 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝑥) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
4241ancoms 467 . . . . . . 7 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
4342adantr 479 . . . . . 6 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
44 oalimcl 7500 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (𝐵 +𝑜 𝑥))
4538, 44mpanr1 714 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ Lim 𝑥) → Lim (𝐵 +𝑜 𝑥))
4645ancoms 467 . . . . . . . . . . 11 ((Lim 𝑥𝐵 ∈ On) → Lim (𝐵 +𝑜 𝑥))
47 ovex 6551 . . . . . . . . . . . 12 (𝐵 +𝑜 𝑥) ∈ V
48 oalim 7472 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ ((𝐵 +𝑜 𝑥) ∈ V ∧ Lim (𝐵 +𝑜 𝑥))) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧))
4947, 48mpanr1 714 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ Lim (𝐵 +𝑜 𝑥)) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧))
5046, 49sylan2 489 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧))
51 limelon 5687 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
5238, 51mpan 701 . . . . . . . . . . . . . . . . 17 (Lim 𝑥𝑥 ∈ On)
53 oacl 7475 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 +𝑜 𝑥) ∈ On)
5453ancoms 467 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +𝑜 𝑥) ∈ On)
55 onelon 5647 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐵 +𝑜 𝑥) ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ∈ On)
5655ex 448 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 +𝑜 𝑥) ∈ On → (𝑧 ∈ (𝐵 +𝑜 𝑥) → 𝑧 ∈ On))
5754, 56syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → 𝑧 ∈ On))
5857adantld 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ∈ On))
5958adantl 480 . . . . . . . . . . . . . . . . . . 19 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ∈ On))
60 0ellim 5686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑥 → ∅ ∈ 𝑥)
61 onelss 5665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐵 ∈ On → (𝑧𝐵𝑧𝐵))
6220sseq2d 3591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐵 ∈ On → (𝑧 ⊆ (𝐵 +𝑜 ∅) ↔ 𝑧𝐵))
6361, 62sylibrd 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐵 ∈ On → (𝑧𝐵𝑧 ⊆ (𝐵 +𝑜 ∅)))
6463imp 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐵 ∈ On ∧ 𝑧𝐵) → 𝑧 ⊆ (𝐵 +𝑜 ∅))
65 oveq2 6531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → (𝐵 +𝑜 𝑦) = (𝐵 +𝑜 ∅))
6665sseq2d 3591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → (𝑧 ⊆ (𝐵 +𝑜 𝑦) ↔ 𝑧 ⊆ (𝐵 +𝑜 ∅)))
6766rspcev 3277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((∅ ∈ 𝑥𝑧 ⊆ (𝐵 +𝑜 ∅)) → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))
6860, 64, 67syl2an 492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Lim 𝑥 ∧ (𝐵 ∈ On ∧ 𝑧𝐵)) → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))
6968expr 640 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Lim 𝑥𝐵 ∈ On) → (𝑧𝐵 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
7069adantrl 747 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧𝐵 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
7170adantrr 748 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim 𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On))) → (𝑧𝐵 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
72 oawordex 7497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝐵𝑧 ↔ ∃𝑦 ∈ On (𝐵 +𝑜 𝑦) = 𝑧))
7372ad2ant2l 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On)) → (𝐵𝑧 ↔ ∃𝑦 ∈ On (𝐵 +𝑜 𝑦) = 𝑧))
74 oaord 7487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦𝑥 ↔ (𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥)))
75743expb 1257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑦 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑦𝑥 ↔ (𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥)))
76 eleq1 2671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐵 +𝑜 𝑦) = 𝑧 → ((𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥) ↔ 𝑧 ∈ (𝐵 +𝑜 𝑥)))
7775, 76sylan9bb 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑦 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +𝑜 𝑦) = 𝑧) → (𝑦𝑥𝑧 ∈ (𝐵 +𝑜 𝑥)))
7877an32s 841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑦𝑥𝑧 ∈ (𝐵 +𝑜 𝑥)))
7978biimpar 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑦𝑥)
80 eqimss2 3616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐵 +𝑜 𝑦) = 𝑧𝑧 ⊆ (𝐵 +𝑜 𝑦))
8180ad3antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ⊆ (𝐵 +𝑜 𝑦))
8279, 81jca 552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑦𝑥𝑧 ⊆ (𝐵 +𝑜 𝑦)))
8382anasss 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥))) → (𝑦𝑥𝑧 ⊆ (𝐵 +𝑜 𝑦)))
8483expcom 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) → (𝑦𝑥𝑧 ⊆ (𝐵 +𝑜 𝑦))))
8584reximdv2 2992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (∃𝑦 ∈ On (𝐵 +𝑜 𝑦) = 𝑧 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
8685adantrr 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On)) → (∃𝑦 ∈ On (𝐵 +𝑜 𝑦) = 𝑧 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
8773, 86sylbid 228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On)) → (𝐵𝑧 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
8887adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim 𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On))) → (𝐵𝑧 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
89 eloni 5632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ On → Ord 𝑧)
90 eloni 5632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ On → Ord 𝐵)
91 ordtri2or 5721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Ord 𝑧 ∧ Ord 𝐵) → (𝑧𝐵𝐵𝑧))
9289, 90, 91syl2anr 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝑧𝐵𝐵𝑧))
9392ad2ant2l 777 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On)) → (𝑧𝐵𝐵𝑧))
9493adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim 𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On))) → (𝑧𝐵𝐵𝑧))
9571, 88, 94mpjaod 394 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim 𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On))) → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))
9695exp45 639 . . . . . . . . . . . . . . . . . . . . . . . 24 (Lim 𝑥 → ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → (𝑧 ∈ On → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))))
9796imp 443 . . . . . . . . . . . . . . . . . . . . . . 23 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → (𝑧 ∈ On → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))))
9897adantld 481 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧 ∈ On → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))))
9998imp32 447 . . . . . . . . . . . . . . . . . . . . 21 (((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))
100 simplrr 796 . . . . . . . . . . . . . . . . . . . . . . 23 ((((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦𝑥) → 𝑧 ∈ On)
101 onelon 5647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
102101, 30sylan2 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵 ∈ On ∧ (𝑥 ∈ On ∧ 𝑦𝑥)) → (𝐵 +𝑜 𝑦) ∈ On)
103102exp32 628 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐵 ∈ On → (𝑥 ∈ On → (𝑦𝑥 → (𝐵 +𝑜 𝑦) ∈ On)))
104103com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ On → (𝐵 ∈ On → (𝑦𝑥 → (𝐵 +𝑜 𝑦) ∈ On)))
105104imp31 446 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦𝑥) → (𝐵 +𝑜 𝑦) ∈ On)
106105adantll 745 . . . . . . . . . . . . . . . . . . . . . . . 24 (((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑦𝑥) → (𝐵 +𝑜 𝑦) ∈ On)
107106adantlr 746 . . . . . . . . . . . . . . . . . . . . . . 23 ((((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦𝑥) → (𝐵 +𝑜 𝑦) ∈ On)
108 simpll 785 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On) → 𝐴 ∈ On)
109108ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . 23 ((((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦𝑥) → 𝐴 ∈ On)
110 oaword 7489 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ On ∧ (𝐵 +𝑜 𝑦) ∈ On ∧ 𝐴 ∈ On) → (𝑧 ⊆ (𝐵 +𝑜 𝑦) ↔ (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
111100, 107, 109, 110syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . 22 ((((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦𝑥) → (𝑧 ⊆ (𝐵 +𝑜 𝑦) ↔ (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
112111rexbidva 3026 . . . . . . . . . . . . . . . . . . . . 21 (((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) → (∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦) ↔ ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
11399, 112mpbid 220 . . . . . . . . . . . . . . . . . . . 20 (((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
114113exp32 628 . . . . . . . . . . . . . . . . . . 19 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧 ∈ On → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))))
11559, 114mpdd 41 . . . . . . . . . . . . . . . . . 18 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
116115exp32 628 . . . . . . . . . . . . . . . . 17 (Lim 𝑥 → (𝑥 ∈ On → (𝐵 ∈ On → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))))
11752, 116mpd 15 . . . . . . . . . . . . . . . 16 (Lim 𝑥 → (𝐵 ∈ On → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))))
118117exp4a 630 . . . . . . . . . . . . . . 15 (Lim 𝑥 → (𝐵 ∈ On → (𝐴 ∈ On → (𝑧 ∈ (𝐵 +𝑜 𝑥) → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))))
119118imp31 446 . . . . . . . . . . . . . 14 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐴 ∈ On) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
120119ralrimiv 2943 . . . . . . . . . . . . 13 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐴 ∈ On) → ∀𝑧 ∈ (𝐵 +𝑜 𝑥)∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
121 iunss2 4491 . . . . . . . . . . . . 13 (∀𝑧 ∈ (𝐵 +𝑜 𝑥)∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) ⊆ 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
122120, 121syl 17 . . . . . . . . . . . 12 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐴 ∈ On) → 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) ⊆ 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
123122ancoms 467 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) ⊆ 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
124 oaordi 7486 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦𝑥 → (𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥)))
125124anim1d 585 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝑦𝑥𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ((𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥) ∧ 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))))
126 oveq2 6531 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝐵 +𝑜 𝑦) → (𝐴 +𝑜 𝑧) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
127126eleq2d 2668 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐵 +𝑜 𝑦) → (𝑤 ∈ (𝐴 +𝑜 𝑧) ↔ 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
128127rspcev 3277 . . . . . . . . . . . . . . . . . 18 (((𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥) ∧ 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧))
129125, 128syl6 34 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝑦𝑥𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧)))
130129expd 450 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦𝑥 → (𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧))))
131130rexlimdv 3007 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (∃𝑦𝑥 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧)))
132 eliun 4450 . . . . . . . . . . . . . . 15 (𝑤 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) ↔ ∃𝑦𝑥 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
133 eliun 4450 . . . . . . . . . . . . . . 15 (𝑤 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) ↔ ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧))
134131, 132, 1333imtr4g 283 . . . . . . . . . . . . . 14 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑤 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → 𝑤 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧)))
135134ssrdv 3569 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) ⊆ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧))
13652, 135sylan 486 . . . . . . . . . . . 12 ((Lim 𝑥𝐵 ∈ On) → 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) ⊆ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧))
137136adantl 480 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) ⊆ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧))
138123, 137eqssd 3580 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) = 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
13950, 138eqtrd 2639 . . . . . . . . 9 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
140139an12s 838 . . . . . . . 8 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
141140adantr 479 . . . . . . 7 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
142 iuneq2 4463 . . . . . . . 8 (∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
143142adantl 480 . . . . . . 7 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
144141, 143eqtr4d 2642 . . . . . 6 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
14543, 144eqtr4d 2642 . . . . 5 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)))
146145exp31 627 . . . 4 (Lim 𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)))))
1474, 8, 12, 16, 23, 37, 146tfinds3 6929 . . 3 (𝐶 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 𝐶) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶))))
148147com12 32 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐶 ∈ On → ((𝐴 +𝑜 𝐵) +𝑜 𝐶) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶))))
1491483impia 1252 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 𝐶) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1975  wral 2891  wrex 2892  Vcvv 3168  wss 3535  c0 3869   ciun 4445  Ord word 5621  Oncon0 5622  Lim wlim 5623  suc csuc 5624  (class class class)co 6523   +𝑜 coa 7417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-int 4401  df-iun 4447  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-om 6931  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-oadd 7424
This theorem is referenced by:  odi  7519  oaabs  7584  oaabs2  7585
  Copyright terms: Public domain W3C validator