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

Theorem oaass 7878
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 6882 . . . . 5 (𝑥 = ∅ → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ((𝐴 +𝑜 𝐵) +𝑜 ∅))
2 oveq2 6882 . . . . . 6 (𝑥 = ∅ → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 ∅))
32oveq2d 6890 . . . . 5 (𝑥 = ∅ → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 +𝑜 (𝐵 +𝑜 ∅)))
41, 3eqeq12d 2821 . . . 4 (𝑥 = ∅ → (((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) ↔ ((𝐴 +𝑜 𝐵) +𝑜 ∅) = (𝐴 +𝑜 (𝐵 +𝑜 ∅))))
5 oveq2 6882 . . . . 5 (𝑥 = 𝑦 → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
6 oveq2 6882 . . . . . 6 (𝑥 = 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝑦))
76oveq2d 6890 . . . . 5 (𝑥 = 𝑦 → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
85, 7eqeq12d 2821 . . . 4 (𝑥 = 𝑦 → (((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) ↔ ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
9 oveq2 6882 . . . . 5 (𝑥 = suc 𝑦 → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦))
10 oveq2 6882 . . . . . 6 (𝑥 = suc 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 suc 𝑦))
1110oveq2d 6890 . . . . 5 (𝑥 = suc 𝑦 → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)))
129, 11eqeq12d 2821 . . . 4 (𝑥 = suc 𝑦 → (((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) ↔ ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦))))
13 oveq2 6882 . . . . 5 (𝑥 = 𝐶 → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ((𝐴 +𝑜 𝐵) +𝑜 𝐶))
14 oveq2 6882 . . . . . 6 (𝑥 = 𝐶 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝐶))
1514oveq2d 6890 . . . . 5 (𝑥 = 𝐶 → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶)))
1613, 15eqeq12d 2821 . . . 4 (𝑥 = 𝐶 → (((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) ↔ ((𝐴 +𝑜 𝐵) +𝑜 𝐶) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶))))
17 oacl 7852 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 𝐵) ∈ On)
18 oa0 7833 . . . . . 6 ((𝐴 +𝑜 𝐵) ∈ On → ((𝐴 +𝑜 𝐵) +𝑜 ∅) = (𝐴 +𝑜 𝐵))
1917, 18syl 17 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 ∅) = (𝐴 +𝑜 𝐵))
20 oa0 7833 . . . . . . 7 (𝐵 ∈ On → (𝐵 +𝑜 ∅) = 𝐵)
2120oveq2d 6890 . . . . . 6 (𝐵 ∈ On → (𝐴 +𝑜 (𝐵 +𝑜 ∅)) = (𝐴 +𝑜 𝐵))
2221adantl 469 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 (𝐵 +𝑜 ∅)) = (𝐴 +𝑜 𝐵))
2319, 22eqtr4d 2843 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 ∅) = (𝐴 +𝑜 (𝐵 +𝑜 ∅)))
24 suceq 6003 . . . . . 6 (((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → suc ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
25 oasuc 7841 . . . . . . . 8 (((𝐴 +𝑜 𝐵) ∈ On ∧ 𝑦 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = suc ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
2617, 25sylan 571 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = suc ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
27 oasuc 7841 . . . . . . . . . . 11 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦))
2827oveq2d 6890 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) = (𝐴 +𝑜 suc (𝐵 +𝑜 𝑦)))
2928adantl 469 . . . . . . . . 9 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) = (𝐴 +𝑜 suc (𝐵 +𝑜 𝑦)))
30 oacl 7852 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 𝑦) ∈ On)
31 oasuc 7841 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (𝐵 +𝑜 𝑦) ∈ On) → (𝐴 +𝑜 suc (𝐵 +𝑜 𝑦)) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
3230, 31sylan2 582 . . . . . . . . 9 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +𝑜 suc (𝐵 +𝑜 𝑦)) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
3329, 32eqtrd 2840 . . . . . . . 8 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
3433anassrs 455 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
3526, 34eqeq12d 2821 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) ↔ suc ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
3624, 35syl5ibr 237 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦))))
3736expcom 400 . . . 4 (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)))))
38 vex 3394 . . . . . . . . . 10 𝑥 ∈ V
39 oalim 7849 . . . . . . . . . 10 (((𝐴 +𝑜 𝐵) ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
4038, 39mpanr1 686 . . . . . . . . 9 (((𝐴 +𝑜 𝐵) ∈ On ∧ Lim 𝑥) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
4117, 40sylan 571 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝑥) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
4241ancoms 448 . . . . . . 7 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
4342adantr 468 . . . . . 6 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
44 oalimcl 7877 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (𝐵 +𝑜 𝑥))
4538, 44mpanr1 686 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ Lim 𝑥) → Lim (𝐵 +𝑜 𝑥))
4645ancoms 448 . . . . . . . . . . 11 ((Lim 𝑥𝐵 ∈ On) → Lim (𝐵 +𝑜 𝑥))
47 ovex 6906 . . . . . . . . . . . 12 (𝐵 +𝑜 𝑥) ∈ V
48 oalim 7849 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ ((𝐵 +𝑜 𝑥) ∈ V ∧ Lim (𝐵 +𝑜 𝑥))) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧))
4947, 48mpanr1 686 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ Lim (𝐵 +𝑜 𝑥)) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧))
5046, 49sylan2 582 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧))
51 limelon 6001 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
5238, 51mpan 673 . . . . . . . . . . . . . . . . 17 (Lim 𝑥𝑥 ∈ On)
53 oacl 7852 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 +𝑜 𝑥) ∈ On)
5453ancoms 448 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +𝑜 𝑥) ∈ On)
55 onelon 5961 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐵 +𝑜 𝑥) ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ∈ On)
5655ex 399 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 +𝑜 𝑥) ∈ On → (𝑧 ∈ (𝐵 +𝑜 𝑥) → 𝑧 ∈ On))
5754, 56syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → 𝑧 ∈ On))
5857adantld 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ∈ On))
5958adantl 469 . . . . . . . . . . . . . . . . . . 19 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ∈ On))
60 0ellim 6000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑥 → ∅ ∈ 𝑥)
61 onelss 5979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐵 ∈ On → (𝑧𝐵𝑧𝐵))
6220sseq2d 3830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐵 ∈ On → (𝑧 ⊆ (𝐵 +𝑜 ∅) ↔ 𝑧𝐵))
6361, 62sylibrd 250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐵 ∈ On → (𝑧𝐵𝑧 ⊆ (𝐵 +𝑜 ∅)))
6463imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐵 ∈ On ∧ 𝑧𝐵) → 𝑧 ⊆ (𝐵 +𝑜 ∅))
65 oveq2 6882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → (𝐵 +𝑜 𝑦) = (𝐵 +𝑜 ∅))
6665sseq2d 3830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → (𝑧 ⊆ (𝐵 +𝑜 𝑦) ↔ 𝑧 ⊆ (𝐵 +𝑜 ∅)))
6766rspcev 3502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((∅ ∈ 𝑥𝑧 ⊆ (𝐵 +𝑜 ∅)) → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))
6860, 64, 67syl2an 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Lim 𝑥 ∧ (𝐵 ∈ On ∧ 𝑧𝐵)) → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))
6968expr 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Lim 𝑥𝐵 ∈ On) → (𝑧𝐵 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
7069adantrl 698 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧𝐵 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
7170adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim 𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On))) → (𝑧𝐵 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
72 oawordex 7874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝐵𝑧 ↔ ∃𝑦 ∈ On (𝐵 +𝑜 𝑦) = 𝑧))
7372ad2ant2l 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On)) → (𝐵𝑧 ↔ ∃𝑦 ∈ On (𝐵 +𝑜 𝑦) = 𝑧))
74 oaord 7864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦𝑥 ↔ (𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥)))
75743expb 1142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑦 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑦𝑥 ↔ (𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥)))
76 eleq1 2873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐵 +𝑜 𝑦) = 𝑧 → ((𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥) ↔ 𝑧 ∈ (𝐵 +𝑜 𝑥)))
7775, 76sylan9bb 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑦 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +𝑜 𝑦) = 𝑧) → (𝑦𝑥𝑧 ∈ (𝐵 +𝑜 𝑥)))
7877an32s 634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑦𝑥𝑧 ∈ (𝐵 +𝑜 𝑥)))
7978biimpar 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑦𝑥)
80 eqimss2 3855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐵 +𝑜 𝑦) = 𝑧𝑧 ⊆ (𝐵 +𝑜 𝑦))
8180ad3antlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ⊆ (𝐵 +𝑜 𝑦))
8279, 81jca 503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑦𝑥𝑧 ⊆ (𝐵 +𝑜 𝑦)))
8382anasss 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥))) → (𝑦𝑥𝑧 ⊆ (𝐵 +𝑜 𝑦)))
8483expcom 400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) → (𝑦𝑥𝑧 ⊆ (𝐵 +𝑜 𝑦))))
8584reximdv2 3201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (∃𝑦 ∈ On (𝐵 +𝑜 𝑦) = 𝑧 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
8685adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On)) → (∃𝑦 ∈ On (𝐵 +𝑜 𝑦) = 𝑧 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
8773, 86sylbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On)) → (𝐵𝑧 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
8887adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim 𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On))) → (𝐵𝑧 → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))
89 eloni 5946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ On → Ord 𝑧)
90 eloni 5946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ On → Ord 𝐵)
91 ordtri2or 6035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Ord 𝑧 ∧ Ord 𝐵) → (𝑧𝐵𝐵𝑧))
9289, 90, 91syl2anr 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝑧𝐵𝐵𝑧))
9392ad2ant2l 743 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On)) → (𝑧𝐵𝐵𝑧))
9493adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Lim 𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On))) → (𝑧𝐵𝐵𝑧))
9571, 88, 94mpjaod 878 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Lim 𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On))) → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))
9695exp45 427 . . . . . . . . . . . . . . . . . . . . . . . 24 (Lim 𝑥 → ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → (𝑧 ∈ On → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))))
9796imp 395 . . . . . . . . . . . . . . . . . . . . . . 23 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → (𝑧 ∈ On → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))))
9897adantld 480 . . . . . . . . . . . . . . . . . . . . . 22 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧 ∈ On → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))))
9998imp32 407 . . . . . . . . . . . . . . . . . . . . 21 (((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) → ∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))
100 simplrr 787 . . . . . . . . . . . . . . . . . . . . . . 23 ((((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦𝑥) → 𝑧 ∈ On)
101 onelon 5961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
102101, 30sylan2 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵 ∈ On ∧ (𝑥 ∈ On ∧ 𝑦𝑥)) → (𝐵 +𝑜 𝑦) ∈ On)
103102exp32 409 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐵 ∈ On → (𝑥 ∈ On → (𝑦𝑥 → (𝐵 +𝑜 𝑦) ∈ On)))
104103com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ On → (𝐵 ∈ On → (𝑦𝑥 → (𝐵 +𝑜 𝑦) ∈ On)))
105104imp31 406 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦𝑥) → (𝐵 +𝑜 𝑦) ∈ On)
106105adantll 696 . . . . . . . . . . . . . . . . . . . . . . . 24 (((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑦𝑥) → (𝐵 +𝑜 𝑦) ∈ On)
107106adantlr 697 . . . . . . . . . . . . . . . . . . . . . . 23 ((((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦𝑥) → (𝐵 +𝑜 𝑦) ∈ On)
108 simpll 774 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On) → 𝐴 ∈ On)
109108ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . 23 ((((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦𝑥) → 𝐴 ∈ On)
110 oaword 7866 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ On ∧ (𝐵 +𝑜 𝑦) ∈ On ∧ 𝐴 ∈ On) → (𝑧 ⊆ (𝐵 +𝑜 𝑦) ↔ (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
111100, 107, 109, 110syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . 22 ((((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦𝑥) → (𝑧 ⊆ (𝐵 +𝑜 𝑦) ↔ (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
112111rexbidva 3237 . . . . . . . . . . . . . . . . . . . . 21 (((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) → (∃𝑦𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦) ↔ ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
11399, 112mpbid 223 . . . . . . . . . . . . . . . . . . . 20 (((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
114113exp32 409 . . . . . . . . . . . . . . . . . . 19 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧 ∈ On → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))))
11559, 114mpdd 43 . . . . . . . . . . . . . . . . . 18 ((Lim 𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
116115exp32 409 . . . . . . . . . . . . . . . . 17 (Lim 𝑥 → (𝑥 ∈ On → (𝐵 ∈ On → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))))
11752, 116mpd 15 . . . . . . . . . . . . . . . 16 (Lim 𝑥 → (𝐵 ∈ On → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))))
118117exp4a 420 . . . . . . . . . . . . . . 15 (Lim 𝑥 → (𝐵 ∈ On → (𝐴 ∈ On → (𝑧 ∈ (𝐵 +𝑜 𝑥) → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))))
119118imp31 406 . . . . . . . . . . . . . 14 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐴 ∈ On) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → ∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
120119ralrimiv 3153 . . . . . . . . . . . . 13 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐴 ∈ On) → ∀𝑧 ∈ (𝐵 +𝑜 𝑥)∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
121 iunss2 4757 . . . . . . . . . . . . 13 (∀𝑧 ∈ (𝐵 +𝑜 𝑥)∃𝑦𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) ⊆ 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
122120, 121syl 17 . . . . . . . . . . . 12 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐴 ∈ On) → 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) ⊆ 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
123122ancoms 448 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) ⊆ 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
124 oaordi 7863 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦𝑥 → (𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥)))
125124anim1d 600 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝑦𝑥𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ((𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥) ∧ 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))))
126 oveq2 6882 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝐵 +𝑜 𝑦) → (𝐴 +𝑜 𝑧) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
127126eleq2d 2871 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐵 +𝑜 𝑦) → (𝑤 ∈ (𝐴 +𝑜 𝑧) ↔ 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))
128127rspcev 3502 . . . . . . . . . . . . . . . . . 18 (((𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥) ∧ 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧))
129125, 128syl6 35 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝑦𝑥𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧)))
130129expd 402 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦𝑥 → (𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧))))
131130rexlimdv 3218 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (∃𝑦𝑥 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧)))
132 eliun 4716 . . . . . . . . . . . . . . 15 (𝑤 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) ↔ ∃𝑦𝑥 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
133 eliun 4716 . . . . . . . . . . . . . . 15 (𝑤 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) ↔ ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧))
134131, 132, 1333imtr4g 287 . . . . . . . . . . . . . 14 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑤 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → 𝑤 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧)))
135134ssrdv 3804 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) ⊆ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧))
13652, 135sylan 571 . . . . . . . . . . . 12 ((Lim 𝑥𝐵 ∈ On) → 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) ⊆ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧))
137136adantl 469 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) ⊆ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧))
138123, 137eqssd 3815 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) = 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
13950, 138eqtrd 2840 . . . . . . . . 9 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
140139an12s 631 . . . . . . . 8 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
141140adantr 468 . . . . . . 7 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
142 iuneq2 4729 . . . . . . . 8 (∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
143142adantl 469 . . . . . . 7 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = 𝑦𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))
144141, 143eqtr4d 2843 . . . . . 6 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = 𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦))
14543, 144eqtr4d 2843 . . . . 5 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)))
146145exp31 408 . . . 4 (Lim 𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∀𝑦𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)))))
1474, 8, 12, 16, 23, 37, 146tfinds3 7294 . . 3 (𝐶 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 𝐶) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶))))
148147com12 32 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐶 ∈ On → ((𝐴 +𝑜 𝐵) +𝑜 𝐶) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶))))
1491483impia 1138 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 𝐶) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wcel 2156  wral 3096  wrex 3097  Vcvv 3391  wss 3769  c0 4116   ciun 4712  Ord word 5935  Oncon0 5936  Lim wlim 5937  suc csuc 5938  (class class class)co 6874   +𝑜 coa 7793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-oadd 7800
This theorem is referenced by:  odi  7896  oaabs  7961  oaabs2  7962
  Copyright terms: Public domain W3C validator