Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜
∅)) |
2 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜
∅)) |
3 | 1, 2 | sseq12d 3597 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥) ↔ (𝐴 +𝑜 ∅) ⊆
(𝐵 +𝑜
∅))) |
4 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 𝑦)) |
5 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝑦)) |
6 | 4, 5 | sseq12d 3597 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥) ↔ (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦))) |
7 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 suc 𝑦)) |
8 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 suc 𝑦)) |
9 | 7, 8 | sseq12d 3597 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥) ↔ (𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦))) |
10 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 𝐶)) |
11 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝐶)) |
12 | 10, 11 | sseq12d 3597 |
. . . . 5
⊢ (𝑥 = 𝐶 → ((𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥) ↔ (𝐴 +𝑜 𝐶) ⊆ (𝐵 +𝑜 𝐶))) |
13 | | oa0 7483 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (𝐴 +𝑜 ∅)
= 𝐴) |
14 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 ∅)
= 𝐴) |
15 | | oa0 7483 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (𝐵 +𝑜 ∅)
= 𝐵) |
16 | 15 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +𝑜 ∅)
= 𝐵) |
17 | 14, 16 | sseq12d 3597 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +𝑜 ∅)
⊆ (𝐵
+𝑜 ∅) ↔ 𝐴 ⊆ 𝐵)) |
18 | 17 | biimpar 501 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +𝑜 ∅) ⊆
(𝐵 +𝑜
∅)) |
19 | | oacl 7502 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 +𝑜 𝑦) ∈ On) |
20 | | eloni 5650 |
. . . . . . . . . . . 12
⊢ ((𝐴 +𝑜 𝑦) ∈ On → Ord (𝐴 +𝑜 𝑦)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → Ord (𝐴 +𝑜 𝑦)) |
22 | | oacl 7502 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 𝑦) ∈ On) |
23 | | eloni 5650 |
. . . . . . . . . . . 12
⊢ ((𝐵 +𝑜 𝑦) ∈ On → Ord (𝐵 +𝑜 𝑦)) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → Ord (𝐵 +𝑜 𝑦)) |
25 | | ordsucsssuc 6915 |
. . . . . . . . . . 11
⊢ ((Ord
(𝐴 +𝑜
𝑦) ∧ Ord (𝐵 +𝑜 𝑦)) → ((𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) ↔ suc (𝐴 +𝑜 𝑦) ⊆ suc (𝐵 +𝑜 𝑦))) |
26 | 21, 24, 25 | syl2an 493 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → ((𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) ↔ suc (𝐴 +𝑜 𝑦) ⊆ suc (𝐵 +𝑜 𝑦))) |
27 | 26 | anandirs 870 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → ((𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) ↔ suc (𝐴 +𝑜 𝑦) ⊆ suc (𝐵 +𝑜 𝑦))) |
28 | | oasuc 7491 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 +𝑜 suc 𝑦) = suc (𝐴 +𝑜 𝑦)) |
29 | 28 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (𝐴 +𝑜 suc 𝑦) = suc (𝐴 +𝑜 𝑦)) |
30 | | oasuc 7491 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦)) |
31 | 30 | adantll 746 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦)) |
32 | 29, 31 | sseq12d 3597 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → ((𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦) ↔ suc (𝐴 +𝑜 𝑦) ⊆ suc (𝐵 +𝑜 𝑦))) |
33 | 27, 32 | bitr4d 270 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → ((𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) ↔ (𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦))) |
34 | 33 | biimpd 218 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → ((𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) → (𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦))) |
35 | 34 | expcom 450 |
. . . . . 6
⊢ (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) → (𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦)))) |
36 | 35 | adantrd 483 |
. . . . 5
⊢ (𝑦 ∈ On → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ((𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) → (𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦)))) |
37 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
38 | | ss2iun 4472 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝑥 (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) → ∪
𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑦) ⊆ ∪
𝑦 ∈ 𝑥 (𝐵 +𝑜 𝑦)) |
39 | | oalim 7499 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐴 +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑦)) |
40 | 39 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐴 +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑦)) |
41 | | oalim 7499 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐵 +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐵 +𝑜 𝑦)) |
42 | 41 | adantll 746 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐵 +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐵 +𝑜 𝑦)) |
43 | 40, 42 | sseq12d 3597 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → ((𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥) ↔ ∪
𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑦) ⊆ ∪
𝑦 ∈ 𝑥 (𝐵 +𝑜 𝑦))) |
44 | 38, 43 | syl5ibr 235 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (∀𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) → (𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥))) |
45 | 37, 44 | mpanr1 715 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝑥) → (∀𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) → (𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥))) |
46 | 45 | expcom 450 |
. . . . . 6
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(∀𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) → (𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥)))) |
47 | 46 | adantrd 483 |
. . . . 5
⊢ (Lim
𝑥 → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (∀𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) → (𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥)))) |
48 | 3, 6, 9, 12, 18, 36, 47 | tfinds3 6956 |
. . . 4
⊢ (𝐶 ∈ On → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +𝑜 𝐶) ⊆ (𝐵 +𝑜 𝐶))) |
49 | 48 | exp4c 634 |
. . 3
⊢ (𝐶 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝐶) ⊆ (𝐵 +𝑜 𝐶))))) |
50 | 49 | com3l 87 |
. 2
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝐶 ∈ On → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝐶) ⊆ (𝐵 +𝑜 𝐶))))) |
51 | 50 | 3imp 1249 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝐶) ⊆ (𝐵 +𝑜 𝐶))) |