| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐴 ↑o 𝑥) = (𝐴 ↑o
∅)) |
| 2 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐵 ↑o 𝑥) = (𝐵 ↑o
∅)) |
| 3 | 1, 2 | sseq12d 4017 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐴 ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥) ↔ (𝐴 ↑o ∅) ⊆ (𝐵 ↑o
∅))) |
| 4 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 ↑o 𝑥) = (𝐴 ↑o 𝑦)) |
| 5 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐵 ↑o 𝑥) = (𝐵 ↑o 𝑦)) |
| 6 | 4, 5 | sseq12d 4017 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐴 ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥) ↔ (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦))) |
| 7 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐴 ↑o 𝑥) = (𝐴 ↑o suc 𝑦)) |
| 8 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐵 ↑o 𝑥) = (𝐵 ↑o suc 𝑦)) |
| 9 | 7, 8 | sseq12d 4017 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((𝐴 ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥) ↔ (𝐴 ↑o suc 𝑦) ⊆ (𝐵 ↑o suc 𝑦))) |
| 10 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝐴 ↑o 𝑥) = (𝐴 ↑o 𝐶)) |
| 11 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝐵 ↑o 𝑥) = (𝐵 ↑o 𝐶)) |
| 12 | 10, 11 | sseq12d 4017 |
. . . 4
⊢ (𝑥 = 𝐶 → ((𝐴 ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥) ↔ (𝐴 ↑o 𝐶) ⊆ (𝐵 ↑o 𝐶))) |
| 13 | | onelon 6409 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On) |
| 14 | | oe0 8560 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝐴 ↑o ∅) =
1o) |
| 15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝐴 ↑o ∅) =
1o) |
| 16 | | oe0 8560 |
. . . . . . 7
⊢ (𝐵 ∈ On → (𝐵 ↑o ∅) =
1o) |
| 17 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝐵 ↑o ∅) =
1o) |
| 18 | 15, 17 | eqtr4d 2780 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝐴 ↑o ∅) = (𝐵 ↑o
∅)) |
| 19 | | eqimss 4042 |
. . . . 5
⊢ ((𝐴 ↑o ∅) =
(𝐵 ↑o
∅) → (𝐴
↑o ∅) ⊆ (𝐵 ↑o
∅)) |
| 20 | 18, 19 | syl 17 |
. . . 4
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝐴 ↑o ∅) ⊆ (𝐵 ↑o
∅)) |
| 21 | | simpl 482 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → 𝐵 ∈ On) |
| 22 | | onelss 6426 |
. . . . . . 7
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → 𝐴 ⊆ 𝐵)) |
| 23 | 22 | imp 406 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → 𝐴 ⊆ 𝐵) |
| 24 | 13, 21, 23 | jca31 514 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → ((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵)) |
| 25 | | oecl 8575 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑o 𝑦) ∈ On) |
| 26 | 25 | 3adant2 1132 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑o 𝑦) ∈ On) |
| 27 | | oecl 8575 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ↑o 𝑦) ∈ On) |
| 28 | 27 | 3adant1 1131 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ↑o 𝑦) ∈ On) |
| 29 | | simp1 1137 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → 𝐴 ∈ On) |
| 30 | | omwordri 8610 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ↑o 𝑦) ∈ On ∧ (𝐵 ↑o 𝑦) ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦) → ((𝐴 ↑o 𝑦) ·o 𝐴) ⊆ ((𝐵 ↑o 𝑦) ·o 𝐴))) |
| 31 | 26, 28, 29, 30 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦) → ((𝐴 ↑o 𝑦) ·o 𝐴) ⊆ ((𝐵 ↑o 𝑦) ·o 𝐴))) |
| 32 | 31 | imp 406 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦)) → ((𝐴 ↑o 𝑦) ·o 𝐴) ⊆ ((𝐵 ↑o 𝑦) ·o 𝐴)) |
| 33 | 32 | adantrl 716 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦))) → ((𝐴 ↑o 𝑦) ·o 𝐴) ⊆ ((𝐵 ↑o 𝑦) ·o 𝐴)) |
| 34 | | omwordi 8609 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ (𝐵 ↑o 𝑦) ∈ On) → (𝐴 ⊆ 𝐵 → ((𝐵 ↑o 𝑦) ·o 𝐴) ⊆ ((𝐵 ↑o 𝑦) ·o 𝐵))) |
| 35 | 28, 34 | syld3an3 1411 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ⊆ 𝐵 → ((𝐵 ↑o 𝑦) ·o 𝐴) ⊆ ((𝐵 ↑o 𝑦) ·o 𝐵))) |
| 36 | 35 | imp 406 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ((𝐵 ↑o 𝑦) ·o 𝐴) ⊆ ((𝐵 ↑o 𝑦) ·o 𝐵)) |
| 37 | 36 | adantrr 717 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦))) → ((𝐵 ↑o 𝑦) ·o 𝐴) ⊆ ((𝐵 ↑o 𝑦) ·o 𝐵)) |
| 38 | 33, 37 | sstrd 3994 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦))) → ((𝐴 ↑o 𝑦) ·o 𝐴) ⊆ ((𝐵 ↑o 𝑦) ·o 𝐵)) |
| 39 | | oesuc 8565 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑o suc 𝑦) = ((𝐴 ↑o 𝑦) ·o 𝐴)) |
| 40 | 39 | 3adant2 1132 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑o suc 𝑦) = ((𝐴 ↑o 𝑦) ·o 𝐴)) |
| 41 | 40 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦))) → (𝐴 ↑o suc 𝑦) = ((𝐴 ↑o 𝑦) ·o 𝐴)) |
| 42 | | oesuc 8565 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ↑o suc 𝑦) = ((𝐵 ↑o 𝑦) ·o 𝐵)) |
| 43 | 42 | 3adant1 1131 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ↑o suc 𝑦) = ((𝐵 ↑o 𝑦) ·o 𝐵)) |
| 44 | 43 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦))) → (𝐵 ↑o suc 𝑦) = ((𝐵 ↑o 𝑦) ·o 𝐵)) |
| 45 | 38, 41, 44 | 3sstr4d 4039 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦))) → (𝐴 ↑o suc 𝑦) ⊆ (𝐵 ↑o suc 𝑦)) |
| 46 | 45 | exp520 1358 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (𝐴 ⊆ 𝐵 → ((𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦) → (𝐴 ↑o suc 𝑦) ⊆ (𝐵 ↑o suc 𝑦)))))) |
| 47 | 46 | com3r 87 |
. . . . . 6
⊢ (𝑦 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → (𝐴 ⊆ 𝐵 → ((𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦) → (𝐴 ↑o suc 𝑦) ⊆ (𝐵 ↑o suc 𝑦)))))) |
| 48 | 47 | imp4c 423 |
. . . . 5
⊢ (𝑦 ∈ On → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ((𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦) → (𝐴 ↑o suc 𝑦) ⊆ (𝐵 ↑o suc 𝑦)))) |
| 49 | 24, 48 | syl5 34 |
. . . 4
⊢ (𝑦 ∈ On → ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → ((𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦) → (𝐴 ↑o suc 𝑦) ⊆ (𝐵 ↑o suc 𝑦)))) |
| 50 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
| 51 | | limelon 6448 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On) |
| 52 | 50, 51 | mpan 690 |
. . . . . . . . . . 11
⊢ (Lim
𝑥 → 𝑥 ∈ On) |
| 53 | | 0ellim 6447 |
. . . . . . . . . . 11
⊢ (Lim
𝑥 → ∅ ∈
𝑥) |
| 54 | | oe0m1 8559 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 ↔ (∅
↑o 𝑥) =
∅)) |
| 55 | 54 | biimpa 476 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ On ∧ ∅ ∈
𝑥) → (∅
↑o 𝑥) =
∅) |
| 56 | 52, 53, 55 | syl2anc 584 |
. . . . . . . . . 10
⊢ (Lim
𝑥 → (∅
↑o 𝑥) =
∅) |
| 57 | | 0ss 4400 |
. . . . . . . . . 10
⊢ ∅
⊆ (𝐵
↑o 𝑥) |
| 58 | 56, 57 | eqsstrdi 4028 |
. . . . . . . . 9
⊢ (Lim
𝑥 → (∅
↑o 𝑥)
⊆ (𝐵
↑o 𝑥)) |
| 59 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → (𝐴 ↑o 𝑥) = (∅ ↑o
𝑥)) |
| 60 | 59 | sseq1d 4015 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → ((𝐴 ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥) ↔ (∅ ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥))) |
| 61 | 58, 60 | imbitrrid 246 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (Lim 𝑥 → (𝐴 ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥))) |
| 62 | 61 | adantl 481 |
. . . . . . 7
⊢ (((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) ∧ 𝐴 = ∅) → (Lim 𝑥 → (𝐴 ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥))) |
| 63 | 62 | a1dd 50 |
. . . . . 6
⊢ (((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) ∧ 𝐴 = ∅) → (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦) → (𝐴 ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥)))) |
| 64 | | ss2iun 5010 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝑥 (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦) → ∪
𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦) ⊆ ∪
𝑦 ∈ 𝑥 (𝐵 ↑o 𝑦)) |
| 65 | | oelim 8572 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 66 | 50, 65 | mpanlr1 706 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 67 | 66 | an32s 652 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ Lim 𝑥) → (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 68 | 67 | adantllr 719 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴 ∈ 𝐵)) ∧ ∅ ∈ 𝐴) ∧ Lim 𝑥) → (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 69 | 21 | anim1i 615 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) ∧ Lim 𝑥) → (𝐵 ∈ On ∧ Lim 𝑥)) |
| 70 | | ne0i 4341 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝐵 → 𝐵 ≠ ∅) |
| 71 | | on0eln0 6440 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
| 72 | 70, 71 | imbitrrid 246 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → ∅ ∈ 𝐵)) |
| 73 | 72 | imp 406 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → ∅ ∈ 𝐵) |
| 74 | 73 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) ∧ Lim 𝑥) → ∅ ∈ 𝐵) |
| 75 | | oelim 8572 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐵) → (𝐵 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐵 ↑o 𝑦)) |
| 76 | 50, 75 | mpanlr1 706 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) → (𝐵 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐵 ↑o 𝑦)) |
| 77 | 69, 74, 76 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) ∧ Lim 𝑥) → (𝐵 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐵 ↑o 𝑦)) |
| 78 | 77 | ad4ant24 754 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴 ∈ 𝐵)) ∧ ∅ ∈ 𝐴) ∧ Lim 𝑥) → (𝐵 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐵 ↑o 𝑦)) |
| 79 | 68, 78 | sseq12d 4017 |
. . . . . . . 8
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴 ∈ 𝐵)) ∧ ∅ ∈ 𝐴) ∧ Lim 𝑥) → ((𝐴 ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥) ↔ ∪
𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦) ⊆ ∪
𝑦 ∈ 𝑥 (𝐵 ↑o 𝑦))) |
| 80 | 64, 79 | imbitrrid 246 |
. . . . . . 7
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴 ∈ 𝐵)) ∧ ∅ ∈ 𝐴) ∧ Lim 𝑥) → (∀𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦) → (𝐴 ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥))) |
| 81 | 80 | ex 412 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴 ∈ 𝐵)) ∧ ∅ ∈ 𝐴) → (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦) → (𝐴 ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥)))) |
| 82 | 63, 81 | oe0lem 8551 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴 ∈ 𝐵)) → (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦) → (𝐴 ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥)))) |
| 83 | 13 | ancri 549 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴 ∈ 𝐵))) |
| 84 | 82, 83 | syl11 33 |
. . . 4
⊢ (Lim
𝑥 → ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (∀𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦) ⊆ (𝐵 ↑o 𝑦) → (𝐴 ↑o 𝑥) ⊆ (𝐵 ↑o 𝑥)))) |
| 85 | 3, 6, 9, 12, 20, 49, 84 | tfinds3 7886 |
. . 3
⊢ (𝐶 ∈ On → ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝐴 ↑o 𝐶) ⊆ (𝐵 ↑o 𝐶))) |
| 86 | 85 | expd 415 |
. 2
⊢ (𝐶 ∈ On → (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (𝐴 ↑o 𝐶) ⊆ (𝐵 ↑o 𝐶)))) |
| 87 | 86 | impcom 407 |
1
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 ↑o 𝐶) ⊆ (𝐵 ↑o 𝐶))) |