Step | Hyp | Ref
| Expression |
1 | | simplr 792 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ∈ ω) |
2 | | nnon 7071 |
. . . . . . . 8
⊢ (𝐵 ∈ ω → 𝐵 ∈ On) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ∈ On) |
4 | | simpll 790 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐴 ∈ ω) |
5 | | nnaword2 7710 |
. . . . . . . 8
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → 𝐵 ⊆ (𝐴 +𝑜 𝐵)) |
6 | 1, 4, 5 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ⊆ (𝐴 +𝑜 𝐵)) |
7 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → (𝐴 +𝑜 𝑦) = (𝐴 +𝑜 𝐵)) |
8 | 7 | sseq2d 3633 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝐵 ⊆ (𝐴 +𝑜 𝑦) ↔ 𝐵 ⊆ (𝐴 +𝑜 𝐵))) |
9 | 8 | elrab 3363 |
. . . . . . 7
⊢ (𝐵 ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ↔ (𝐵 ∈ On ∧ 𝐵 ⊆ (𝐴 +𝑜 𝐵))) |
10 | 3, 6, 9 | sylanbrc 698 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) |
11 | | intss1 4492 |
. . . . . 6
⊢ (𝐵 ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ 𝐵) |
12 | 10, 11 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ 𝐵) |
13 | | ssrab2 3687 |
. . . . . . . 8
⊢ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ On |
14 | | ne0i 3921 |
. . . . . . . . 9
⊢ (𝐵 ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ≠ ∅) |
15 | 10, 14 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ≠ ∅) |
16 | | oninton 7000 |
. . . . . . . 8
⊢ (({𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ≠ ∅) → ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} ∈
On) |
17 | 13, 15, 16 | sylancr 695 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ On) |
18 | | eloni 5733 |
. . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} ∈ On → Ord
∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → Ord ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) |
20 | | ordom 7074 |
. . . . . 6
⊢ Ord
ω |
21 | | ordtr2 5768 |
. . . . . 6
⊢ ((Ord
∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∧ Ord ω) → ((∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} ⊆ 𝐵 ∧ 𝐵 ∈ ω) → ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} ∈
ω)) |
22 | 19, 20, 21 | sylancl 694 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ((∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ 𝐵 ∧ 𝐵 ∈ ω) → ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} ∈
ω)) |
23 | 12, 1, 22 | mp2and 715 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ ω) |
24 | | nna0 7684 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐴 +𝑜 ∅)
= 𝐴) |
25 | 24 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +𝑜 ∅) = 𝐴) |
26 | | simpr 477 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐴 ⊆ 𝐵) |
27 | 25, 26 | eqsstrd 3639 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +𝑜 ∅) ⊆
𝐵) |
28 | | oveq2 6658 |
. . . . . . . 8
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = ∅ → (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) = (𝐴 +𝑜
∅)) |
29 | 28 | sseq1d 3632 |
. . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = ∅ →
((𝐴 +𝑜
∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) ⊆ 𝐵 ↔ (𝐴 +𝑜 ∅) ⊆
𝐵)) |
30 | 27, 29 | syl5ibrcom 237 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = ∅ → (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) ⊆ 𝐵)) |
31 | | simprr 796 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥) |
32 | 31 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) = (𝐴 +𝑜 suc 𝑥)) |
33 | 4 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → 𝐴 ∈ ω) |
34 | | simprl 794 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → 𝑥 ∈ ω) |
35 | | nnasuc 7686 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +𝑜 suc 𝑥) = suc (𝐴 +𝑜 𝑥)) |
36 | 33, 34, 35 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → (𝐴 +𝑜 suc 𝑥) = suc (𝐴 +𝑜 𝑥)) |
37 | 32, 36 | eqtrd 2656 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) = suc (𝐴 +𝑜 𝑥)) |
38 | | nnord 7073 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ω → Ord 𝐵) |
39 | 1, 38 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → Ord 𝐵) |
40 | 39 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → Ord 𝐵) |
41 | | nnon 7071 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ω → 𝑥 ∈ On) |
42 | 41 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥) → 𝑥 ∈ On) |
43 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
44 | 43 | sucid 5804 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ suc 𝑥 |
45 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥) → ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥) |
46 | 44, 45 | syl5eleqr 2708 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥) → 𝑥 ∈ ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) |
47 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (𝐴 +𝑜 𝑦) = (𝐴 +𝑜 𝑥)) |
48 | 47 | sseq2d 3633 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → (𝐵 ⊆ (𝐴 +𝑜 𝑦) ↔ 𝐵 ⊆ (𝐴 +𝑜 𝑥))) |
49 | 48 | onnminsb 7004 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → (𝑥 ∈ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} → ¬ 𝐵 ⊆ (𝐴 +𝑜 𝑥))) |
50 | 42, 46, 49 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥) → ¬ 𝐵 ⊆ (𝐴 +𝑜 𝑥)) |
51 | 50 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → ¬ 𝐵 ⊆ (𝐴 +𝑜 𝑥)) |
52 | | nnacl 7691 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +𝑜 𝑥) ∈
ω) |
53 | 33, 34, 52 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → (𝐴 +𝑜 𝑥) ∈ ω) |
54 | | nnord 7073 |
. . . . . . . . . . . . 13
⊢ ((𝐴 +𝑜 𝑥) ∈ ω → Ord
(𝐴 +𝑜
𝑥)) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → Ord (𝐴 +𝑜 𝑥)) |
56 | | ordtri1 5756 |
. . . . . . . . . . . 12
⊢ ((Ord
𝐵 ∧ Ord (𝐴 +𝑜 𝑥)) → (𝐵 ⊆ (𝐴 +𝑜 𝑥) ↔ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐵)) |
57 | 40, 55, 56 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → (𝐵 ⊆ (𝐴 +𝑜 𝑥) ↔ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐵)) |
58 | 57 | con2bid 344 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → ((𝐴 +𝑜 𝑥) ∈ 𝐵 ↔ ¬ 𝐵 ⊆ (𝐴 +𝑜 𝑥))) |
59 | 51, 58 | mpbird 247 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → (𝐴 +𝑜 𝑥) ∈ 𝐵) |
60 | | ordsucss 7018 |
. . . . . . . . 9
⊢ (Ord
𝐵 → ((𝐴 +𝑜 𝑥) ∈ 𝐵 → suc (𝐴 +𝑜 𝑥) ⊆ 𝐵)) |
61 | 40, 59, 60 | sylc 65 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → suc (𝐴 +𝑜 𝑥) ⊆ 𝐵) |
62 | 37, 61 | eqsstrd 3639 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} = suc 𝑥)) → (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) ⊆ 𝐵) |
63 | 62 | rexlimdvaa 3032 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (∃𝑥 ∈ ω ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥 → (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) ⊆ 𝐵)) |
64 | | nn0suc 7090 |
. . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} ∈ ω →
(∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = ∅ ∨ ∃𝑥 ∈ ω ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) |
65 | 23, 64 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = ∅ ∨ ∃𝑥 ∈ ω ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) |
66 | 30, 63, 65 | mpjaod 396 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) ⊆ 𝐵) |
67 | | onint 6995 |
. . . . . . 7
⊢ (({𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ≠ ∅) → ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) |
68 | 13, 15, 67 | sylancr 695 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) |
69 | | nfrab1 3122 |
. . . . . . . . 9
⊢
Ⅎ𝑦{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} |
70 | 69 | nfint 4486 |
. . . . . . . 8
⊢
Ⅎ𝑦∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} |
71 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑦On |
72 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝐵 |
73 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝐴 |
74 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑦
+𝑜 |
75 | 73, 74, 70 | nfov 6676 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) |
76 | 72, 75 | nfss 3596 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝐵 ⊆ (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) |
77 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑦 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → (𝐴 +𝑜 𝑦) = (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)})) |
78 | 77 | sseq2d 3633 |
. . . . . . . 8
⊢ (𝑦 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → (𝐵 ⊆ (𝐴 +𝑜 𝑦) ↔ 𝐵 ⊆ (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}))) |
79 | 70, 71, 76, 78 | elrabf 3360 |
. . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ↔ (∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ On ∧ 𝐵 ⊆ (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}))) |
80 | 79 | simprbi 480 |
. . . . . 6
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → 𝐵 ⊆ (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)})) |
81 | 68, 80 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ⊆ (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)})) |
82 | 66, 81 | eqssd 3620 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) = 𝐵) |
83 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)})) |
84 | 83 | eqeq1d 2624 |
. . . . 5
⊢ (𝑥 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → ((𝐴 +𝑜 𝑥) = 𝐵 ↔ (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) = 𝐵)) |
85 | 84 | rspcev 3309 |
. . . 4
⊢ ((∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} ∈ ω ∧
(𝐴 +𝑜
∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) = 𝐵) → ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝐵) |
86 | 23, 82, 85 | syl2anc 693 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝐵) |
87 | 86 | ex 450 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝐵)) |
88 | | nnaword1 7709 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → 𝐴 ⊆ (𝐴 +𝑜 𝑥)) |
89 | 88 | adantlr 751 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑥 ∈ ω) → 𝐴 ⊆ (𝐴 +𝑜 𝑥)) |
90 | | sseq2 3627 |
. . . 4
⊢ ((𝐴 +𝑜 𝑥) = 𝐵 → (𝐴 ⊆ (𝐴 +𝑜 𝑥) ↔ 𝐴 ⊆ 𝐵)) |
91 | 89, 90 | syl5ibcom 235 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑥 ∈ ω) → ((𝐴 +𝑜 𝑥) = 𝐵 → 𝐴 ⊆ 𝐵)) |
92 | 91 | rexlimdva 3031 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
(∃𝑥 ∈ ω
(𝐴 +𝑜
𝑥) = 𝐵 → 𝐴 ⊆ 𝐵)) |
93 | 87, 92 | impbid 202 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝐵)) |