| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝐴 +o 𝑦) = (𝐴 +o 𝐵)) | 
| 2 | 1 | sseq2d 4015 | . . . . . . 7
⊢ (𝑦 = 𝐵 → (𝐵 ⊆ (𝐴 +o 𝑦) ↔ 𝐵 ⊆ (𝐴 +o 𝐵))) | 
| 3 |  | simplr 768 | . . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ∈ ω) | 
| 4 |  | nnon 7894 | . . . . . . . 8
⊢ (𝐵 ∈ ω → 𝐵 ∈ On) | 
| 5 | 3, 4 | syl 17 | . . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ∈ On) | 
| 6 |  | simpll 766 | . . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐴 ∈ ω) | 
| 7 |  | nnaword2 8669 | . . . . . . . 8
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → 𝐵 ⊆ (𝐴 +o 𝐵)) | 
| 8 | 3, 6, 7 | syl2anc 584 | . . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ⊆ (𝐴 +o 𝐵)) | 
| 9 | 2, 5, 8 | elrabd 3693 | . . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) | 
| 10 |  | intss1 4962 | . . . . . 6
⊢ (𝐵 ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ⊆ 𝐵) | 
| 11 | 9, 10 | syl 17 | . . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ⊆ 𝐵) | 
| 12 |  | ssrab2 4079 | . . . . . . . 8
⊢ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ⊆ On | 
| 13 | 9 | ne0d 4341 | . . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ≠ ∅) | 
| 14 |  | oninton 7816 | . . . . . . . 8
⊢ (({𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ≠ ∅) → ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ On) | 
| 15 | 12, 13, 14 | sylancr 587 | . . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ∈ On) | 
| 16 |  | eloni 6393 | . . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ On → Ord ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)}) | 
| 17 | 15, 16 | syl 17 | . . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → Ord ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) | 
| 18 |  | ordom 7898 | . . . . . 6
⊢ Ord
ω | 
| 19 |  | ordtr2 6427 | . . . . . 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 699 | . . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ∈ ω) | 
| 22 |  | nna0 8643 | . . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴) | 
| 23 | 22 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +o ∅) = 𝐴) | 
| 24 |  | simpr 484 | . . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐴 ⊆ 𝐵) | 
| 25 | 23, 24 | eqsstrd 4017 | . . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +o ∅) ⊆ 𝐵) | 
| 26 |  | oveq2 7440 | . . . . . . . 8
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = ∅ → (𝐴 +o ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)}) = (𝐴 +o ∅)) | 
| 27 | 26 | sseq1d 4014 | . . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = ∅ → ((𝐴 +o ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)}) ⊆ 𝐵 ↔ (𝐴 +o ∅) ⊆ 𝐵)) | 
| 28 | 25, 27 | syl5ibrcom 247 | . . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} = ∅ → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) ⊆ 𝐵)) | 
| 29 |  | simprr 772 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} = suc 𝑥) | 
| 30 | 29 | oveq2d 7448 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) = (𝐴 +o suc 𝑥)) | 
| 31 | 6 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → 𝐴 ∈ ω) | 
| 32 |  | simprl 770 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → 𝑥 ∈ ω) | 
| 33 |  | nnasuc 8645 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +o suc 𝑥) = suc (𝐴 +o 𝑥)) | 
| 34 | 31, 32, 33 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐴 +o suc 𝑥) = suc (𝐴 +o 𝑥)) | 
| 35 | 30, 34 | eqtrd 2776 | . . . . . . . 8
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) = suc (𝐴 +o 𝑥)) | 
| 36 |  | nnord 7896 | . . . . . . . . . . 11
⊢ (𝐵 ∈ ω → Ord 𝐵) | 
| 37 | 3, 36 | syl 17 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → Ord 𝐵) | 
| 38 | 37 | adantr 480 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → Ord 𝐵) | 
| 39 |  | nnon 7894 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ω → 𝑥 ∈ On) | 
| 40 | 39 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥) → 𝑥 ∈ On) | 
| 41 |  | vex 3483 | . . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V | 
| 42 | 41 | sucid 6465 | . . . . . . . . . . . . 13
⊢ 𝑥 ∈ suc 𝑥 | 
| 43 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} = suc 𝑥) | 
| 44 | 42, 43 | eleqtrrid 2847 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥) → 𝑥 ∈ ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) | 
| 45 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (𝐴 +o 𝑦) = (𝐴 +o 𝑥)) | 
| 46 | 45 | sseq2d 4015 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → (𝐵 ⊆ (𝐴 +o 𝑦) ↔ 𝐵 ⊆ (𝐴 +o 𝑥))) | 
| 47 | 46 | onnminsb 7820 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ On → (𝑥 ∈ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} → ¬ 𝐵 ⊆ (𝐴 +o 𝑥))) | 
| 48 | 40, 44, 47 | sylc 65 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥) → ¬ 𝐵 ⊆ (𝐴 +o 𝑥)) | 
| 49 | 48 | adantl 481 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → ¬ 𝐵 ⊆ (𝐴 +o 𝑥)) | 
| 50 |  | nnacl 8650 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) ∈
ω) | 
| 51 | 31, 32, 50 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐴 +o 𝑥) ∈ ω) | 
| 52 |  | nnord 7896 | . . . . . . . . . . . . 13
⊢ ((𝐴 +o 𝑥) ∈ ω → Ord
(𝐴 +o 𝑥)) | 
| 53 | 51, 52 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → Ord (𝐴 +o 𝑥)) | 
| 54 |  | ordtri1 6416 | . . . . . . . . . . . 12
⊢ ((Ord
𝐵 ∧ Ord (𝐴 +o 𝑥)) → (𝐵 ⊆ (𝐴 +o 𝑥) ↔ ¬ (𝐴 +o 𝑥) ∈ 𝐵)) | 
| 55 | 38, 53, 54 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐵 ⊆ (𝐴 +o 𝑥) ↔ ¬ (𝐴 +o 𝑥) ∈ 𝐵)) | 
| 56 | 55 | con2bid 354 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → ((𝐴 +o 𝑥) ∈ 𝐵 ↔ ¬ 𝐵 ⊆ (𝐴 +o 𝑥))) | 
| 57 | 49, 56 | mpbird 257 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐴 +o 𝑥) ∈ 𝐵) | 
| 58 |  | ordsucss 7839 | . . . . . . . . 9
⊢ (Ord
𝐵 → ((𝐴 +o 𝑥) ∈ 𝐵 → suc (𝐴 +o 𝑥) ⊆ 𝐵)) | 
| 59 | 38, 57, 58 | sylc 65 | . . . . . . . 8
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → suc (𝐴 +o 𝑥) ⊆ 𝐵) | 
| 60 | 35, 59 | eqsstrd 4017 | . . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ∈ ω ∧ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) ⊆ 𝐵) | 
| 61 | 60 | rexlimdvaa 3155 | . . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (∃𝑥 ∈ ω ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} = suc 𝑥 → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) ⊆ 𝐵)) | 
| 62 |  | nn0suc 7917 | . . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ ω → (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = ∅ ∨ ∃𝑥 ∈ ω ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} = suc 𝑥)) | 
| 63 | 21, 62 | syl 17 | . . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} = ∅ ∨ ∃𝑥 ∈ ω ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} = suc 𝑥)) | 
| 64 | 28, 61, 63 | mpjaod 860 | . . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) ⊆ 𝐵) | 
| 65 |  | onint 7811 | . . . . . . 7
⊢ (({𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ≠ ∅) → ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) | 
| 66 | 12, 13, 65 | sylancr 587 | . . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) | 
| 67 |  | nfrab1 3456 | . . . . . . . . 9
⊢
Ⅎ𝑦{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} | 
| 68 | 67 | nfint 4955 | . . . . . . . 8
⊢
Ⅎ𝑦∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} | 
| 69 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑦On | 
| 70 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑦𝐵 | 
| 71 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑦𝐴 | 
| 72 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑦
+o | 
| 73 | 71, 72, 68 | nfov 7462 | . . . . . . . . 9
⊢
Ⅎ𝑦(𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) | 
| 74 | 70, 73 | nfss 3975 | . . . . . . . 8
⊢
Ⅎ𝑦 𝐵 ⊆ (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) | 
| 75 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑦 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} → (𝐴 +o 𝑦) = (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)})) | 
| 76 | 75 | sseq2d 4015 | . . . . . . . 8
⊢ (𝑦 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} → (𝐵 ⊆ (𝐴 +o 𝑦) ↔ 𝐵 ⊆ (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}))) | 
| 77 | 68, 69, 74, 76 | elrabf 3687 | . . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ↔ (∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ∈ On ∧ 𝐵 ⊆ (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}))) | 
| 78 | 77 | simprbi 496 | . . . . . 6
⊢ (∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} → 𝐵 ⊆ (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)})) | 
| 79 | 66, 78 | syl 17 | . . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ⊆ (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)})) | 
| 80 | 64, 79 | eqssd 4000 | . . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) = 𝐵) | 
| 81 |  | oveq2 7440 | . . . . . 6
⊢ (𝑥 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} → (𝐴 +o 𝑥) = (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)})) | 
| 82 | 81 | eqeq1d 2738 | . . . . 5
⊢ (𝑥 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} → ((𝐴 +o 𝑥) = 𝐵 ↔ (𝐴 +o ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)}) = 𝐵)) | 
| 83 | 82 | rspcev 3621 | . . . 4
⊢ ((∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)} ∈ ω ∧ (𝐴 +o ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +o 𝑦)}) = 𝐵) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵) | 
| 84 | 21, 80, 83 | syl2anc 584 | . . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ⊆ 𝐵) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵) | 
| 85 | 84 | ex 412 | . 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) | 
| 86 |  | nnaword1 8668 | . . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → 𝐴 ⊆ (𝐴 +o 𝑥)) | 
| 87 | 86 | adantlr 715 | . . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑥 ∈ ω) → 𝐴 ⊆ (𝐴 +o 𝑥)) | 
| 88 |  | sseq2 4009 | . . . 4
⊢ ((𝐴 +o 𝑥) = 𝐵 → (𝐴 ⊆ (𝐴 +o 𝑥) ↔ 𝐴 ⊆ 𝐵)) | 
| 89 | 87, 88 | syl5ibcom 245 | . . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑥 ∈ ω) → ((𝐴 +o 𝑥) = 𝐵 → 𝐴 ⊆ 𝐵)) | 
| 90 | 89 | rexlimdva 3154 | . 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
(∃𝑥 ∈ ω
(𝐴 +o 𝑥) = 𝐵 → 𝐴 ⊆ 𝐵)) | 
| 91 | 85, 90 | impbid 212 | 1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |