Step | Hyp | Ref
| Expression |
1 | | oveq2 7279 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ·o 𝑥) = (𝐴 ·o
∅)) |
2 | | oveq2 7279 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐵 ·o 𝑥) = (𝐵 ·o
∅)) |
3 | 1, 2 | sseq12d 3959 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐴 ·o 𝑥) ⊆ (𝐵 ·o 𝑥) ↔ (𝐴 ·o ∅) ⊆
(𝐵 ·o
∅))) |
4 | | oveq2 7279 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝑦)) |
5 | | oveq2 7279 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐵 ·o 𝑥) = (𝐵 ·o 𝑦)) |
6 | 4, 5 | sseq12d 3959 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 ·o 𝑥) ⊆ (𝐵 ·o 𝑥) ↔ (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦))) |
7 | | oveq2 7279 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o suc 𝑦)) |
8 | | oveq2 7279 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐵 ·o 𝑥) = (𝐵 ·o suc 𝑦)) |
9 | 7, 8 | sseq12d 3959 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝐴 ·o 𝑥) ⊆ (𝐵 ·o 𝑥) ↔ (𝐴 ·o suc 𝑦) ⊆ (𝐵 ·o suc 𝑦))) |
10 | | oveq2 7279 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝐶)) |
11 | | oveq2 7279 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝐵 ·o 𝑥) = (𝐵 ·o 𝐶)) |
12 | 10, 11 | sseq12d 3959 |
. . . . 5
⊢ (𝑥 = 𝐶 → ((𝐴 ·o 𝑥) ⊆ (𝐵 ·o 𝑥) ↔ (𝐴 ·o 𝐶) ⊆ (𝐵 ·o 𝐶))) |
13 | | om0 8332 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝐴 ·o ∅) =
∅) |
14 | | 0ss 4336 |
. . . . . . 7
⊢ ∅
⊆ (𝐵
·o ∅) |
15 | 13, 14 | eqsstrdi 3980 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐴 ·o ∅)
⊆ (𝐵
·o ∅)) |
16 | 15 | ad2antrr 723 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ·o ∅) ⊆
(𝐵 ·o
∅)) |
17 | | omcl 8351 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o 𝑦) ∈ On) |
18 | 17 | 3adant2 1130 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o 𝑦) ∈ On) |
19 | | omcl 8351 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·o 𝑦) ∈ On) |
20 | 19 | 3adant1 1129 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·o 𝑦) ∈ On) |
21 | | simp1 1135 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → 𝐴 ∈ On) |
22 | | oawordri 8366 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ·o 𝑦) ∈ On ∧ (𝐵 ·o 𝑦) ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦) → ((𝐴 ·o 𝑦) +o 𝐴) ⊆ ((𝐵 ·o 𝑦) +o 𝐴))) |
23 | 18, 20, 21, 22 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦) → ((𝐴 ·o 𝑦) +o 𝐴) ⊆ ((𝐵 ·o 𝑦) +o 𝐴))) |
24 | 23 | imp 407 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦)) → ((𝐴 ·o 𝑦) +o 𝐴) ⊆ ((𝐵 ·o 𝑦) +o 𝐴)) |
25 | 24 | adantrl 713 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦))) → ((𝐴 ·o 𝑦) +o 𝐴) ⊆ ((𝐵 ·o 𝑦) +o 𝐴)) |
26 | | oaword 8365 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ (𝐵 ·o 𝑦) ∈ On) → (𝐴 ⊆ 𝐵 ↔ ((𝐵 ·o 𝑦) +o 𝐴) ⊆ ((𝐵 ·o 𝑦) +o 𝐵))) |
27 | 20, 26 | syld3an3 1408 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ((𝐵 ·o 𝑦) +o 𝐴) ⊆ ((𝐵 ·o 𝑦) +o 𝐵))) |
28 | 27 | biimpa 477 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ((𝐵 ·o 𝑦) +o 𝐴) ⊆ ((𝐵 ·o 𝑦) +o 𝐵)) |
29 | 28 | adantrr 714 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦))) → ((𝐵 ·o 𝑦) +o 𝐴) ⊆ ((𝐵 ·o 𝑦) +o 𝐵)) |
30 | 25, 29 | sstrd 3936 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦))) → ((𝐴 ·o 𝑦) +o 𝐴) ⊆ ((𝐵 ·o 𝑦) +o 𝐵)) |
31 | | omsuc 8341 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o suc 𝑦) = ((𝐴 ·o 𝑦) +o 𝐴)) |
32 | 31 | 3adant2 1130 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o suc 𝑦) = ((𝐴 ·o 𝑦) +o 𝐴)) |
33 | 32 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦))) → (𝐴 ·o suc 𝑦) = ((𝐴 ·o 𝑦) +o 𝐴)) |
34 | | omsuc 8341 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·o suc 𝑦) = ((𝐵 ·o 𝑦) +o 𝐵)) |
35 | 34 | 3adant1 1129 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·o suc 𝑦) = ((𝐵 ·o 𝑦) +o 𝐵)) |
36 | 35 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦))) → (𝐵 ·o suc 𝑦) = ((𝐵 ·o 𝑦) +o 𝐵)) |
37 | 30, 33, 36 | 3sstr4d 3973 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦))) → (𝐴 ·o suc 𝑦) ⊆ (𝐵 ·o suc 𝑦)) |
38 | 37 | exp520 1356 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (𝐴 ⊆ 𝐵 → ((𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦) → (𝐴 ·o suc 𝑦) ⊆ (𝐵 ·o suc 𝑦)))))) |
39 | 38 | com3r 87 |
. . . . . 6
⊢ (𝑦 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → (𝐴 ⊆ 𝐵 → ((𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦) → (𝐴 ·o suc 𝑦) ⊆ (𝐵 ·o suc 𝑦)))))) |
40 | 39 | imp4c 424 |
. . . . 5
⊢ (𝑦 ∈ On → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ((𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦) → (𝐴 ·o suc 𝑦) ⊆ (𝐵 ·o suc 𝑦)))) |
41 | | vex 3435 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
42 | | ss2iun 4948 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑥 (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦) → ∪
𝑦 ∈ 𝑥 (𝐴 ·o 𝑦) ⊆ ∪
𝑦 ∈ 𝑥 (𝐵 ·o 𝑦)) |
43 | | omlim 8348 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐴 ·o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ·o 𝑦)) |
44 | 43 | ad2ant2rl 746 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ (𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥))) → (𝐴 ·o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ·o 𝑦)) |
45 | | omlim 8348 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐵 ·o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐵 ·o 𝑦)) |
46 | 45 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ (𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥))) → (𝐵 ·o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐵 ·o 𝑦)) |
47 | 44, 46 | sseq12d 3959 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ (𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥))) → ((𝐴 ·o 𝑥) ⊆ (𝐵 ·o 𝑥) ↔ ∪
𝑦 ∈ 𝑥 (𝐴 ·o 𝑦) ⊆ ∪
𝑦 ∈ 𝑥 (𝐵 ·o 𝑦))) |
48 | 42, 47 | syl5ibr 245 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ (𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥))) → (∀𝑦 ∈ 𝑥 (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦) → (𝐴 ·o 𝑥) ⊆ (𝐵 ·o 𝑥))) |
49 | 48 | anandirs 676 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (∀𝑦 ∈ 𝑥 (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦) → (𝐴 ·o 𝑥) ⊆ (𝐵 ·o 𝑥))) |
50 | 41, 49 | mpanr1 700 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝑥) → (∀𝑦 ∈ 𝑥 (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦) → (𝐴 ·o 𝑥) ⊆ (𝐵 ·o 𝑥))) |
51 | 50 | expcom 414 |
. . . . . 6
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(∀𝑦 ∈ 𝑥 (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦) → (𝐴 ·o 𝑥) ⊆ (𝐵 ·o 𝑥)))) |
52 | 51 | adantrd 492 |
. . . . 5
⊢ (Lim
𝑥 → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (∀𝑦 ∈ 𝑥 (𝐴 ·o 𝑦) ⊆ (𝐵 ·o 𝑦) → (𝐴 ·o 𝑥) ⊆ (𝐵 ·o 𝑥)))) |
53 | 3, 6, 9, 12, 16, 40, 52 | tfinds3 7705 |
. . . 4
⊢ (𝐶 ∈ On → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ·o 𝐶) ⊆ (𝐵 ·o 𝐶))) |
54 | 53 | expd 416 |
. . 3
⊢ (𝐶 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐴 ·o 𝐶) ⊆ (𝐵 ·o 𝐶)))) |
55 | 54 | 3impib 1115 |
. 2
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐴 ·o 𝐶) ⊆ (𝐵 ·o 𝐶))) |
56 | 55 | 3coml 1126 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐴 ·o 𝐶) ⊆ (𝐵 ·o 𝐶))) |