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

Theorem omass 7705
Description: Multiplication of ordinal numbers is associative. Theorem 8.26 of [TakeutiZaring] p. 65. (Contributed by NM, 28-Dec-2004.)
Assertion
Ref Expression
omass ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶)))

Proof of Theorem omass
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6698 . . . . . 6 (𝑥 = ∅ → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜 ∅))
2 oveq2 6698 . . . . . . 7 (𝑥 = ∅ → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 ∅))
32oveq2d 6706 . . . . . 6 (𝑥 = ∅ → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜 ∅)))
41, 3eqeq12d 2666 . . . . 5 (𝑥 = ∅ → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) ↔ ((𝐴 ·𝑜 𝐵) ·𝑜 ∅) = (𝐴 ·𝑜 (𝐵 ·𝑜 ∅))))
5 oveq2 6698 . . . . . 6 (𝑥 = 𝑦 → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦))
6 oveq2 6698 . . . . . . 7 (𝑥 = 𝑦 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 𝑦))
76oveq2d 6706 . . . . . 6 (𝑥 = 𝑦 → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)))
85, 7eqeq12d 2666 . . . . 5 (𝑥 = 𝑦 → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) ↔ ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))
9 oveq2 6698 . . . . . 6 (𝑥 = suc 𝑦 → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦))
10 oveq2 6698 . . . . . . 7 (𝑥 = suc 𝑦 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 suc 𝑦))
1110oveq2d 6706 . . . . . 6 (𝑥 = suc 𝑦 → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦)))
129, 11eqeq12d 2666 . . . . 5 (𝑥 = suc 𝑦 → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) ↔ ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦))))
13 oveq2 6698 . . . . . 6 (𝑥 = 𝐶 → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶))
14 oveq2 6698 . . . . . . 7 (𝑥 = 𝐶 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 𝐶))
1514oveq2d 6706 . . . . . 6 (𝑥 = 𝐶 → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶)))
1613, 15eqeq12d 2666 . . . . 5 (𝑥 = 𝐶 → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) ↔ ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶))))
17 omcl 7661 . . . . . . 7 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 𝐵) ∈ On)
18 om0 7642 . . . . . . 7 ((𝐴 ·𝑜 𝐵) ∈ On → ((𝐴 ·𝑜 𝐵) ·𝑜 ∅) = ∅)
1917, 18syl 17 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜 𝐵) ·𝑜 ∅) = ∅)
20 om0 7642 . . . . . . . 8 (𝐵 ∈ On → (𝐵 ·𝑜 ∅) = ∅)
2120oveq2d 6706 . . . . . . 7 (𝐵 ∈ On → (𝐴 ·𝑜 (𝐵 ·𝑜 ∅)) = (𝐴 ·𝑜 ∅))
22 om0 7642 . . . . . . 7 (𝐴 ∈ On → (𝐴 ·𝑜 ∅) = ∅)
2321, 22sylan9eqr 2707 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 (𝐵 ·𝑜 ∅)) = ∅)
2419, 23eqtr4d 2688 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜 𝐵) ·𝑜 ∅) = (𝐴 ·𝑜 (𝐵 ·𝑜 ∅)))
25 oveq1 6697 . . . . . . . . 9 (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) +𝑜 (𝐴 ·𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))
26 omsuc 7651 . . . . . . . . . . 11 (((𝐴 ·𝑜 𝐵) ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) +𝑜 (𝐴 ·𝑜 𝐵)))
2717, 26stoic3 1741 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) +𝑜 (𝐴 ·𝑜 𝐵)))
28 omsuc 7651 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·𝑜 suc 𝑦) = ((𝐵 ·𝑜 𝑦) +𝑜 𝐵))
29283adant1 1099 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·𝑜 suc 𝑦) = ((𝐵 ·𝑜 𝑦) +𝑜 𝐵))
3029oveq2d 6706 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦)) = (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)))
31 omcl 7661 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·𝑜 𝑦) ∈ On)
32 odi 7704 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ (𝐵 ·𝑜 𝑦) ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))
3331, 32syl3an2 1400 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))
34333exp 1283 . . . . . . . . . . . . . . 15 (𝐴 ∈ On → ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ On → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))))
3534expd 451 . . . . . . . . . . . . . 14 (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (𝐵 ∈ On → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵))))))
3635com34 91 . . . . . . . . . . . . 13 (𝐴 ∈ On → (𝐵 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵))))))
3736pm2.43d 53 . . . . . . . . . . . 12 (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))))
38373imp 1275 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))
3930, 38eqtrd 2685 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))
4027, 39eqeq12d 2666 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦)) ↔ (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) +𝑜 (𝐴 ·𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵))))
4125, 40syl5ibr 236 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦))))
42413exp 1283 . . . . . . 7 (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦))))))
4342com3r 87 . . . . . 6 (𝑦 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦))))))
4443impd 446 . . . . 5 (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦)))))
4517ancoms 468 . . . . . . . . . . . . . 14 ((𝐵 ∈ On ∧ 𝐴 ∈ On) → (𝐴 ·𝑜 𝐵) ∈ On)
46 vex 3234 . . . . . . . . . . . . . . 15 𝑥 ∈ V
47 omlim 7658 . . . . . . . . . . . . . . 15 (((𝐴 ·𝑜 𝐵) ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = 𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦))
4846, 47mpanr1 719 . . . . . . . . . . . . . 14 (((𝐴 ·𝑜 𝐵) ∈ On ∧ Lim 𝑥) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = 𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦))
4945, 48sylan 487 . . . . . . . . . . . . 13 (((𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ Lim 𝑥) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = 𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦))
5049an32s 863 . . . . . . . . . . . 12 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = 𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦))
5150ad2antrr 762 . . . . . . . . . . 11 (((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐵) ∧ ∀𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = 𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦))
52 iuneq2 4569 . . . . . . . . . . . 12 (∀𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → 𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = 𝑦𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)))
53 limelon 5826 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
5446, 53mpan 706 . . . . . . . . . . . . . . . . . . . . 21 (Lim 𝑥𝑥 ∈ On)
5554anim1i 591 . . . . . . . . . . . . . . . . . . . 20 ((Lim 𝑥𝐵 ∈ On) → (𝑥 ∈ On ∧ 𝐵 ∈ On))
5655ancoms 468 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ On ∧ Lim 𝑥) → (𝑥 ∈ On ∧ 𝐵 ∈ On))
57 omordi 7691 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐵) → (𝑦𝑥 → (𝐵 ·𝑜 𝑦) ∈ (𝐵 ·𝑜 𝑥)))
5856, 57sylan 487 . . . . . . . . . . . . . . . . . 18 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) → (𝑦𝑥 → (𝐵 ·𝑜 𝑦) ∈ (𝐵 ·𝑜 𝑥)))
59 ssid 3657 . . . . . . . . . . . . . . . . . . 19 (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))
60 oveq2 6698 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)))
6160sseq2d 3666 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝐵 ·𝑜 𝑦) → ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) ⊆ (𝐴 ·𝑜 𝑧) ↔ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))
6261rspcev 3340 . . . . . . . . . . . . . . . . . . 19 (((𝐵 ·𝑜 𝑦) ∈ (𝐵 ·𝑜 𝑥) ∧ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))) → ∃𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) ⊆ (𝐴 ·𝑜 𝑧))
6359, 62mpan2 707 . . . . . . . . . . . . . . . . . 18 ((𝐵 ·𝑜 𝑦) ∈ (𝐵 ·𝑜 𝑥) → ∃𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) ⊆ (𝐴 ·𝑜 𝑧))
6458, 63syl6 35 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) → (𝑦𝑥 → ∃𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) ⊆ (𝐴 ·𝑜 𝑧)))
6564ralrimiv 2994 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) → ∀𝑦𝑥𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) ⊆ (𝐴 ·𝑜 𝑧))
66 iunss2 4597 . . . . . . . . . . . . . . . 16 (∀𝑦𝑥𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) ⊆ (𝐴 ·𝑜 𝑧) → 𝑦𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) ⊆ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧))
6765, 66syl 17 . . . . . . . . . . . . . . 15 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) → 𝑦𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) ⊆ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧))
6867adantlr 751 . . . . . . . . . . . . . 14 ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐵) → 𝑦𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) ⊆ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧))
69 omcl 7661 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 ·𝑜 𝑥) ∈ On)
7054, 69sylan2 490 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ On ∧ Lim 𝑥) → (𝐵 ·𝑜 𝑥) ∈ On)
71 onelon 5786 . . . . . . . . . . . . . . . . . . . 20 (((𝐵 ·𝑜 𝑥) ∈ On ∧ 𝑧 ∈ (𝐵 ·𝑜 𝑥)) → 𝑧 ∈ On)
7270, 71sylan 487 . . . . . . . . . . . . . . . . . . 19 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝑧 ∈ (𝐵 ·𝑜 𝑥)) → 𝑧 ∈ On)
7372adantlr 751 . . . . . . . . . . . . . . . . . 18 ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ 𝑧 ∈ (𝐵 ·𝑜 𝑥)) → 𝑧 ∈ On)
74 omordlim 7702 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ 𝑧 ∈ (𝐵 ·𝑜 𝑥)) → ∃𝑦𝑥 𝑧 ∈ (𝐵 ·𝑜 𝑦))
7574ex 449 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝑧 ∈ (𝐵 ·𝑜 𝑥) → ∃𝑦𝑥 𝑧 ∈ (𝐵 ·𝑜 𝑦)))
7646, 75mpanr1 719 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ On ∧ Lim 𝑥) → (𝑧 ∈ (𝐵 ·𝑜 𝑥) → ∃𝑦𝑥 𝑧 ∈ (𝐵 ·𝑜 𝑦)))
7776ad2antlr 763 . . . . . . . . . . . . . . . . . . . . 21 (((𝑧 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝑥)) ∧ 𝐴 ∈ On) → (𝑧 ∈ (𝐵 ·𝑜 𝑥) → ∃𝑦𝑥 𝑧 ∈ (𝐵 ·𝑜 𝑦)))
78 onelon 5786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
7954, 78sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Lim 𝑥𝑦𝑥) → 𝑦 ∈ On)
8079, 31sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ On ∧ (Lim 𝑥𝑦𝑥)) → (𝐵 ·𝑜 𝑦) ∈ On)
81 onelss 5804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐵 ·𝑜 𝑦) ∈ On → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → 𝑧 ⊆ (𝐵 ·𝑜 𝑦)))
82813ad2ant2 1103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 ∈ On ∧ (𝐵 ·𝑜 𝑦) ∈ On ∧ 𝐴 ∈ On) → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → 𝑧 ⊆ (𝐵 ·𝑜 𝑦)))
83 omwordi 7696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 ∈ On ∧ (𝐵 ·𝑜 𝑦) ∈ On ∧ 𝐴 ∈ On) → (𝑧 ⊆ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))
8482, 83syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑧 ∈ On ∧ (𝐵 ·𝑜 𝑦) ∈ On ∧ 𝐴 ∈ On) → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))
85843exp 1283 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ On → ((𝐵 ·𝑜 𝑦) ∈ On → (𝐴 ∈ On → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))))
8680, 85syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ On → ((𝐵 ∈ On ∧ (Lim 𝑥𝑦𝑥)) → (𝐴 ∈ On → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))))
8786exp4d 636 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ On → (𝐵 ∈ On → (Lim 𝑥 → (𝑦𝑥 → (𝐴 ∈ On → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))))))
8887imp32 448 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝑥)) → (𝑦𝑥 → (𝐴 ∈ On → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))))
8988com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝑥)) → (𝐴 ∈ On → (𝑦𝑥 → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))))
9089imp 444 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑧 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝑥)) ∧ 𝐴 ∈ On) → (𝑦𝑥 → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)))))
9190reximdvai 3044 . . . . . . . . . . . . . . . . . . . . 21 (((𝑧 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝑥)) ∧ 𝐴 ∈ On) → (∃𝑦𝑥 𝑧 ∈ (𝐵 ·𝑜 𝑦) → ∃𝑦𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))
9277, 91syld 47 . . . . . . . . . . . . . . . . . . . 20 (((𝑧 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝑥)) ∧ 𝐴 ∈ On) → (𝑧 ∈ (𝐵 ·𝑜 𝑥) → ∃𝑦𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))
9392exp31 629 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ On → ((𝐵 ∈ On ∧ Lim 𝑥) → (𝐴 ∈ On → (𝑧 ∈ (𝐵 ·𝑜 𝑥) → ∃𝑦𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))))
9493imp4c 616 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ On → ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ 𝑧 ∈ (𝐵 ·𝑜 𝑥)) → ∃𝑦𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))
9573, 94mpcom 38 . . . . . . . . . . . . . . . . 17 ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ 𝑧 ∈ (𝐵 ·𝑜 𝑥)) → ∃𝑦𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)))
9695ralrimiva 2995 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → ∀𝑧 ∈ (𝐵 ·𝑜 𝑥)∃𝑦𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)))
97 iunss2 4597 . . . . . . . . . . . . . . . 16 (∀𝑧 ∈ (𝐵 ·𝑜 𝑥)∃𝑦𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ 𝑦𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)))
9896, 97syl 17 . . . . . . . . . . . . . . 15 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ 𝑦𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)))
9998adantr 480 . . . . . . . . . . . . . 14 ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐵) → 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ 𝑦𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)))
10068, 99eqssd 3653 . . . . . . . . . . . . 13 ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐵) → 𝑦𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) = 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧))
101 omlimcl 7703 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐵) → Lim (𝐵 ·𝑜 𝑥))
10246, 101mpanlr1 722 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) → Lim (𝐵 ·𝑜 𝑥))
103 ovex 6718 . . . . . . . . . . . . . . . . 17 (𝐵 ·𝑜 𝑥) ∈ V
104 omlim 7658 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ ((𝐵 ·𝑜 𝑥) ∈ V ∧ Lim (𝐵 ·𝑜 𝑥))) → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧))
105103, 104mpanr1 719 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ Lim (𝐵 ·𝑜 𝑥)) → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧))
106102, 105sylan2 490 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ ((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵)) → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧))
107106ancoms 468 . . . . . . . . . . . . . 14 ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) ∧ 𝐴 ∈ On) → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧))
108107an32s 863 . . . . . . . . . . . . 13 ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐵) → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧))
109100, 108eqtr4d 2688 . . . . . . . . . . . 12 ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐵) → 𝑦𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)))
11052, 109sylan9eqr 2707 . . . . . . . . . . 11 (((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐵) ∧ ∀𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))) → 𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)))
11151, 110eqtrd 2685 . . . . . . . . . 10 (((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐵) ∧ ∀𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)))
112111exp31 629 . . . . . . . . 9 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → (∅ ∈ 𝐵 → (∀𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)))))
113 eloni 5771 . . . . . . . . . . . . 13 (𝐵 ∈ On → Ord 𝐵)
114 ord0eln0 5817 . . . . . . . . . . . . . 14 (Ord 𝐵 → (∅ ∈ 𝐵𝐵 ≠ ∅))
115114necon2bbid 2866 . . . . . . . . . . . . 13 (Ord 𝐵 → (𝐵 = ∅ ↔ ¬ ∅ ∈ 𝐵))
116113, 115syl 17 . . . . . . . . . . . 12 (𝐵 ∈ On → (𝐵 = ∅ ↔ ¬ ∅ ∈ 𝐵))
117116ad2antrr 762 . . . . . . . . . . 11 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → (𝐵 = ∅ ↔ ¬ ∅ ∈ 𝐵))
118 oveq2 6698 . . . . . . . . . . . . . . . . . . 19 (𝐵 = ∅ → (𝐴 ·𝑜 𝐵) = (𝐴 ·𝑜 ∅))
119118, 22sylan9eqr 2707 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ On ∧ 𝐵 = ∅) → (𝐴 ·𝑜 𝐵) = ∅)
120119oveq1d 6705 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ 𝐵 = ∅) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (∅ ·𝑜 𝑥))
121 om0r 7664 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ On → (∅ ·𝑜 𝑥) = ∅)
122120, 121sylan9eqr 2707 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 = ∅)) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = ∅)
123122anassrs 681 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ 𝐴 ∈ On) ∧ 𝐵 = ∅) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = ∅)
124 oveq1 6697 . . . . . . . . . . . . . . . . . . 19 (𝐵 = ∅ → (𝐵 ·𝑜 𝑥) = (∅ ·𝑜 𝑥))
125124, 121sylan9eqr 2707 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ On ∧ 𝐵 = ∅) → (𝐵 ·𝑜 𝑥) = ∅)
126125oveq2d 6706 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ On ∧ 𝐵 = ∅) → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = (𝐴 ·𝑜 ∅))
127126, 22sylan9eq 2705 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ On ∧ 𝐵 = ∅) ∧ 𝐴 ∈ On) → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = ∅)
128127an32s 863 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ 𝐴 ∈ On) ∧ 𝐵 = ∅) → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = ∅)
129123, 128eqtr4d 2688 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ 𝐴 ∈ On) ∧ 𝐵 = ∅) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)))
130129ex 449 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ 𝐴 ∈ On) → (𝐵 = ∅ → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥))))
13154, 130sylan 487 . . . . . . . . . . . 12 ((Lim 𝑥𝐴 ∈ On) → (𝐵 = ∅ → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥))))
132131adantll 750 . . . . . . . . . . 11 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → (𝐵 = ∅ → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥))))
133117, 132sylbird 250 . . . . . . . . . 10 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → (¬ ∅ ∈ 𝐵 → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥))))
134133a1dd 50 . . . . . . . . 9 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → (¬ ∅ ∈ 𝐵 → (∀𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)))))
135112, 134pm2.61d 170 . . . . . . . 8 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → (∀𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥))))
136135exp31 629 . . . . . . 7 (𝐵 ∈ On → (Lim 𝑥 → (𝐴 ∈ On → (∀𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥))))))
137136com3l 89 . . . . . 6 (Lim 𝑥 → (𝐴 ∈ On → (𝐵 ∈ On → (∀𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥))))))
138137impd 446 . . . . 5 (Lim 𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∀𝑦𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)))))
1394, 8, 12, 16, 24, 44, 138tfinds3 7106 . . . 4 (𝐶 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶))))
140139expd 451 . . 3 (𝐶 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶)))))
141140com3l 89 . 2 (𝐴 ∈ On → (𝐵 ∈ On → (𝐶 ∈ On → ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶)))))
1421413imp 1275 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  wrex 2942  Vcvv 3231  wss 3607  c0 3948   ciun 4552  Ord word 5760  Oncon0 5761  Lim wlim 5762  suc csuc 5763  (class class class)co 6690   +𝑜 coa 7602   ·𝑜 comu 7603
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-omul 7610
This theorem is referenced by:  oeoalem  7721  omabs  7772
  Copyright terms: Public domain W3C validator