Step | Hyp | Ref
| Expression |
1 | | oveq2 7275 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝐴 +o 𝑦) = (𝐴 +o 𝐵)) |
2 | 1 | sseq2d 3952 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝐵 ⊆ (𝐴 +o 𝑦) ↔ 𝐵 ⊆ (𝐴 +o 𝐵))) |
3 | | simplr 766 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ∈ ω) |
4 | | nnon 7708 |
. . . . . . . 8
⊢ (𝐵 ∈ ω → 𝐵 ∈ On) |
5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ∈ On) |
6 | | simpll 764 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐴 ∈ ω) |
7 | | nnaword2 8448 |
. . . . . . . 8
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → 𝐵 ⊆ (𝐴 +o 𝐵)) |
8 | 3, 6, 7 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ⊆ (𝐴 +o 𝐵)) |
9 | 2, 5, 8 | elrabd 3625 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) |
10 | | intss1 4894 |
. . . . . 6
⊢ (𝐵 ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ⊆ 𝐵) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ⊆ 𝐵) |
12 | | ssrab2 4012 |
. . . . . . . 8
⊢ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ⊆ On |
13 | 9 | ne0d 4269 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ≠ ∅) |
14 | | oninton 7635 |
. . . . . . . 8
⊢ (({𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ≠ ∅) → ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ On) |
15 | 12, 13, 14 | sylancr 587 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ∈ On) |
16 | | eloni 6269 |
. . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ On → Ord ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)}) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → Ord ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) |
18 | | ordom 7712 |
. . . . . 6
⊢ Ord
ω |
19 | | ordtr2 6303 |
. . . . . 6
⊢ ((Ord
∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ∧ Ord ω) → ((∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ⊆ 𝐵 ∧ 𝐵 ∈ ω) → ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈
ω)) |
20 | 17, 18, 19 | sylancl 586 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ((∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ⊆ 𝐵 ∧ 𝐵 ∈ ω) → ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈
ω)) |
21 | 11, 3, 20 | mp2and 696 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ∈ ω) |
22 | | nna0 8422 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴) |
23 | 22 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +o ∅) = 𝐴) |
24 | | simpr 485 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐴 ⊆ 𝐵) |
25 | 23, 24 | eqsstrd 3958 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +o ∅) ⊆ 𝐵) |
26 | | oveq2 7275 |
. . . . . . . 8
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = ∅ → (𝐴 +o ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)}) = (𝐴 +o ∅)) |
27 | 26 | sseq1d 3951 |
. . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = ∅ → ((𝐴 +o ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)}) ⊆ 𝐵 ↔ (𝐴 +o ∅) ⊆ 𝐵)) |
28 | 25, 27 | syl5ibrcom 246 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} = ∅ → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) ⊆ 𝐵)) |
29 | | simprr 770 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} = suc 𝑥) |
30 | 29 | oveq2d 7283 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) = (𝐴 +o suc 𝑥)) |
31 | 6 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → 𝐴 ∈ ω) |
32 | | simprl 768 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → 𝑥 ∈ ω) |
33 | | nnasuc 8424 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +o suc 𝑥) = suc (𝐴 +o 𝑥)) |
34 | 31, 32, 33 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐴 +o suc 𝑥) = suc (𝐴 +o 𝑥)) |
35 | 30, 34 | eqtrd 2778 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) = suc (𝐴 +o 𝑥)) |
36 | | nnord 7710 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ω → Ord 𝐵) |
37 | 3, 36 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → Ord 𝐵) |
38 | 37 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → Ord 𝐵) |
39 | | nnon 7708 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ω → 𝑥 ∈ On) |
40 | 39 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥) → 𝑥 ∈ On) |
41 | | vex 3433 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
42 | 41 | sucid 6338 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ suc 𝑥 |
43 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} = suc 𝑥) |
44 | 42, 43 | eleqtrrid 2846 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥) → 𝑥 ∈ ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) |
45 | | oveq2 7275 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (𝐴 +o 𝑦) = (𝐴 +o 𝑥)) |
46 | 45 | sseq2d 3952 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → (𝐵 ⊆ (𝐴 +o 𝑦) ↔ 𝐵 ⊆ (𝐴 +o 𝑥))) |
47 | 46 | onnminsb 7639 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → (𝑥 ∈ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} → ¬ 𝐵 ⊆ (𝐴 +o 𝑥))) |
48 | 40, 44, 47 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥) → ¬ 𝐵 ⊆ (𝐴 +o 𝑥)) |
49 | 48 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → ¬ 𝐵 ⊆ (𝐴 +o 𝑥)) |
50 | | nnacl 8429 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) ∈
ω) |
51 | 31, 32, 50 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐴 +o 𝑥) ∈ ω) |
52 | | nnord 7710 |
. . . . . . . . . . . . 13
⊢ ((𝐴 +o 𝑥) ∈ ω → Ord
(𝐴 +o 𝑥)) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → Ord (𝐴 +o 𝑥)) |
54 | | ordtri1 6292 |
. . . . . . . . . . . 12
⊢ ((Ord
𝐵 ∧ Ord (𝐴 +o 𝑥)) → (𝐵 ⊆ (𝐴 +o 𝑥) ↔ ¬ (𝐴 +o 𝑥) ∈ 𝐵)) |
55 | 38, 53, 54 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐵 ⊆ (𝐴 +o 𝑥) ↔ ¬ (𝐴 +o 𝑥) ∈ 𝐵)) |
56 | 55 | con2bid 355 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → ((𝐴 +o 𝑥) ∈ 𝐵 ↔ ¬ 𝐵 ⊆ (𝐴 +o 𝑥))) |
57 | 49, 56 | mpbird 256 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐴 +o 𝑥) ∈ 𝐵) |
58 | | ordsucss 7655 |
. . . . . . . . 9
⊢ (Ord
𝐵 → ((𝐴 +o 𝑥) ∈ 𝐵 → suc (𝐴 +o 𝑥) ⊆ 𝐵)) |
59 | 38, 57, 58 | sylc 65 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → suc (𝐴 +o 𝑥) ⊆ 𝐵) |
60 | 35, 59 | eqsstrd 3958 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) ⊆ 𝐵) |
61 | 60 | rexlimdvaa 3212 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (∃𝑥 ∈ ω ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} = suc 𝑥 → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) ⊆ 𝐵)) |
62 | | nn0suc 7732 |
. . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ ω → (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = ∅ ∨ ∃𝑥 ∈ ω ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) |
63 | 21, 62 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} = ∅ ∨ ∃𝑥 ∈ ω ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} = suc 𝑥)) |
64 | 28, 61, 63 | mpjaod 857 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) ⊆ 𝐵) |
65 | | onint 7630 |
. . . . . . 7
⊢ (({𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ≠ ∅) → ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) |
66 | 12, 13, 65 | sylancr 587 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) |
67 | | nfrab1 3315 |
. . . . . . . . 9
⊢
Ⅎ𝑦{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} |
68 | 67 | nfint 4889 |
. . . . . . . 8
⊢
Ⅎ𝑦∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} |
69 | | nfcv 2907 |
. . . . . . . 8
⊢
Ⅎ𝑦On |
70 | | nfcv 2907 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝐵 |
71 | | nfcv 2907 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝐴 |
72 | | nfcv 2907 |
. . . . . . . . . 10
⊢
Ⅎ𝑦
+o |
73 | 71, 72, 68 | nfov 7297 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) |
74 | 70, 73 | nfss 3912 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝐵 ⊆ (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) |
75 | | oveq2 7275 |
. . . . . . . . 9
⊢ (𝑦 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} → (𝐴 +o 𝑦) = (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)})) |
76 | 75 | sseq2d 3952 |
. . . . . . . 8
⊢ (𝑦 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} → (𝐵 ⊆ (𝐴 +o 𝑦) ↔ 𝐵 ⊆ (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}))) |
77 | 68, 69, 74, 76 | elrabf 3619 |
. . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ↔ (∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ∈ On ∧ 𝐵 ⊆ (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}))) |
78 | 77 | simprbi 497 |
. . . . . 6
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} → 𝐵 ⊆ (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)})) |
79 | 66, 78 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ⊆ (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)})) |
80 | 64, 79 | eqssd 3937 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) = 𝐵) |
81 | | oveq2 7275 |
. . . . . 6
⊢ (𝑥 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} → (𝐴 +o 𝑥) = (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)})) |
82 | 81 | eqeq1d 2740 |
. . . . 5
⊢ (𝑥 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} → ((𝐴 +o 𝑥) = 𝐵 ↔ (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) = 𝐵)) |
83 | 82 | rspcev 3559 |
. . . 4
⊢ ((∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ ω ∧ (𝐴 +o ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)}) = 𝐵) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵) |
84 | 21, 80, 83 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵) |
85 | 84 | ex 413 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |
86 | | nnaword1 8447 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → 𝐴 ⊆ (𝐴 +o 𝑥)) |
87 | 86 | adantlr 712 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑥 ∈ ω) → 𝐴 ⊆ (𝐴 +o 𝑥)) |
88 | | sseq2 3946 |
. . . 4
⊢ ((𝐴 +o 𝑥) = 𝐵 → (𝐴 ⊆ (𝐴 +o 𝑥) ↔ 𝐴 ⊆ 𝐵)) |
89 | 87, 88 | syl5ibcom 244 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑥 ∈ ω) → ((𝐴 +o 𝑥) = 𝐵 → 𝐴 ⊆ 𝐵)) |
90 | 89 | rexlimdva 3211 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
(∃𝑥 ∈ ω
(𝐴 +o 𝑥) = 𝐵 → 𝐴 ⊆ 𝐵)) |
91 | 85, 90 | impbid 211 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |