Step | Hyp | Ref
| Expression |
1 | | noel 3418 |
. . . . . . 7
⊢ ¬
𝐴 ∈
∅ |
2 | | uni0 3821 |
. . . . . . . 8
⊢ ∪ ∅ = ∅ |
3 | 2 | eleq2i 2237 |
. . . . . . 7
⊢ (𝐴 ∈ ∪ ∅ ↔ 𝐴 ∈ ∅) |
4 | 1, 3 | mtbir 666 |
. . . . . 6
⊢ ¬
𝐴 ∈ ∪ ∅ |
5 | | unieq 3803 |
. . . . . . 7
⊢ (𝐵 = ∅ → ∪ 𝐵 =
∪ ∅) |
6 | 5 | eleq2d 2240 |
. . . . . 6
⊢ (𝐵 = ∅ → (𝐴 ∈ ∪ 𝐵
↔ 𝐴 ∈ ∪ ∅)) |
7 | 4, 6 | mtbiri 670 |
. . . . 5
⊢ (𝐵 = ∅ → ¬ 𝐴 ∈ ∪ 𝐵) |
8 | 7 | pm2.21d 614 |
. . . 4
⊢ (𝐵 = ∅ → (𝐴 ∈ ∪ 𝐵
→ suc 𝐴 ∈ 𝐵)) |
9 | 8 | adantl 275 |
. . 3
⊢ ((𝐵 ∈ ω ∧ 𝐵 = ∅) → (𝐴 ∈ ∪ 𝐵
→ suc 𝐴 ∈ 𝐵)) |
10 | | unieq 3803 |
. . . . . . . . . . . 12
⊢ (𝐵 = suc 𝑛 → ∪ 𝐵 = ∪
suc 𝑛) |
11 | 10 | eleq2d 2240 |
. . . . . . . . . . 11
⊢ (𝐵 = suc 𝑛 → (𝐴 ∈ ∪ 𝐵 ↔ 𝐴 ∈ ∪ suc
𝑛)) |
12 | 11 | ad2antll 488 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ω ∧ (𝑛 ∈ ω ∧ 𝐵 = suc 𝑛)) → (𝐴 ∈ ∪ 𝐵 ↔ 𝐴 ∈ ∪ suc
𝑛)) |
13 | 12 | biimpa 294 |
. . . . . . . . 9
⊢ (((𝐵 ∈ ω ∧ (𝑛 ∈ ω ∧ 𝐵 = suc 𝑛)) ∧ 𝐴 ∈ ∪ 𝐵) → 𝐴 ∈ ∪ suc
𝑛) |
14 | | simplrl 530 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ ω ∧ (𝑛 ∈ ω ∧ 𝐵 = suc 𝑛)) ∧ 𝐴 ∈ ∪ 𝐵) → 𝑛 ∈ ω) |
15 | | nnord 4594 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω → Ord 𝑛) |
16 | | ordtr 4361 |
. . . . . . . . . . . . 13
⊢ (Ord
𝑛 → Tr 𝑛) |
17 | 15, 16 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ω → Tr 𝑛) |
18 | | vex 2733 |
. . . . . . . . . . . . 13
⊢ 𝑛 ∈ V |
19 | 18 | unisuc 4396 |
. . . . . . . . . . . 12
⊢ (Tr 𝑛 ↔ ∪ suc 𝑛 = 𝑛) |
20 | 17, 19 | sylib 121 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ω → ∪ suc 𝑛 = 𝑛) |
21 | 14, 20 | syl 14 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ ω ∧ (𝑛 ∈ ω ∧ 𝐵 = suc 𝑛)) ∧ 𝐴 ∈ ∪ 𝐵) → ∪ suc 𝑛 = 𝑛) |
22 | 21 | eleq2d 2240 |
. . . . . . . . 9
⊢ (((𝐵 ∈ ω ∧ (𝑛 ∈ ω ∧ 𝐵 = suc 𝑛)) ∧ 𝐴 ∈ ∪ 𝐵) → (𝐴 ∈ ∪ suc
𝑛 ↔ 𝐴 ∈ 𝑛)) |
23 | 13, 22 | mpbid 146 |
. . . . . . . 8
⊢ (((𝐵 ∈ ω ∧ (𝑛 ∈ ω ∧ 𝐵 = suc 𝑛)) ∧ 𝐴 ∈ ∪ 𝐵) → 𝐴 ∈ 𝑛) |
24 | | nnsucelsuc 6468 |
. . . . . . . . 9
⊢ (𝑛 ∈ ω → (𝐴 ∈ 𝑛 ↔ suc 𝐴 ∈ suc 𝑛)) |
25 | 14, 24 | syl 14 |
. . . . . . . 8
⊢ (((𝐵 ∈ ω ∧ (𝑛 ∈ ω ∧ 𝐵 = suc 𝑛)) ∧ 𝐴 ∈ ∪ 𝐵) → (𝐴 ∈ 𝑛 ↔ suc 𝐴 ∈ suc 𝑛)) |
26 | 23, 25 | mpbid 146 |
. . . . . . 7
⊢ (((𝐵 ∈ ω ∧ (𝑛 ∈ ω ∧ 𝐵 = suc 𝑛)) ∧ 𝐴 ∈ ∪ 𝐵) → suc 𝐴 ∈ suc 𝑛) |
27 | | simplrr 531 |
. . . . . . 7
⊢ (((𝐵 ∈ ω ∧ (𝑛 ∈ ω ∧ 𝐵 = suc 𝑛)) ∧ 𝐴 ∈ ∪ 𝐵) → 𝐵 = suc 𝑛) |
28 | 26, 27 | eleqtrrd 2250 |
. . . . . 6
⊢ (((𝐵 ∈ ω ∧ (𝑛 ∈ ω ∧ 𝐵 = suc 𝑛)) ∧ 𝐴 ∈ ∪ 𝐵) → suc 𝐴 ∈ 𝐵) |
29 | 28 | ex 114 |
. . . . 5
⊢ ((𝐵 ∈ ω ∧ (𝑛 ∈ ω ∧ 𝐵 = suc 𝑛)) → (𝐴 ∈ ∪ 𝐵 → suc 𝐴 ∈ 𝐵)) |
30 | 29 | rexlimdvaa 2588 |
. . . 4
⊢ (𝐵 ∈ ω →
(∃𝑛 ∈ ω
𝐵 = suc 𝑛 → (𝐴 ∈ ∪ 𝐵 → suc 𝐴 ∈ 𝐵))) |
31 | 30 | imp 123 |
. . 3
⊢ ((𝐵 ∈ ω ∧
∃𝑛 ∈ ω
𝐵 = suc 𝑛) → (𝐴 ∈ ∪ 𝐵 → suc 𝐴 ∈ 𝐵)) |
32 | | nn0suc 4586 |
. . 3
⊢ (𝐵 ∈ ω → (𝐵 = ∅ ∨ ∃𝑛 ∈ ω 𝐵 = suc 𝑛)) |
33 | 9, 31, 32 | mpjaodan 793 |
. 2
⊢ (𝐵 ∈ ω → (𝐴 ∈ ∪ 𝐵
→ suc 𝐴 ∈ 𝐵)) |
34 | | sucunielr 4492 |
. 2
⊢ (suc
𝐴 ∈ 𝐵 → 𝐴 ∈ ∪ 𝐵) |
35 | 33, 34 | impbid1 141 |
1
⊢ (𝐵 ∈ ω → (𝐴 ∈ ∪ 𝐵
↔ suc 𝐴 ∈ 𝐵)) |