Step | Hyp | Ref
| Expression |
1 | | saddisj.1 |
. . 3
⊢ (𝜑 → 𝐴 ⊆
ℕ0) |
2 | | saddisj.2 |
. . 3
⊢ (𝜑 → 𝐵 ⊆
ℕ0) |
3 | | saddisjlem.c |
. . 3
⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))) |
4 | | saddisjlem.3 |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
5 | 1, 2, 3, 4 | sadval 16161 |
. 2
⊢ (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ hadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)))) |
6 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝐶‘𝑥) = (𝐶‘0)) |
7 | 6 | eleq2d 2826 |
. . . . . . 7
⊢ (𝑥 = 0 → (∅ ∈
(𝐶‘𝑥) ↔ ∅ ∈ (𝐶‘0))) |
8 | 7 | notbid 318 |
. . . . . 6
⊢ (𝑥 = 0 → (¬ ∅
∈ (𝐶‘𝑥) ↔ ¬ ∅ ∈
(𝐶‘0))) |
9 | 8 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = 0 → ((𝜑 → ¬ ∅ ∈ (𝐶‘𝑥)) ↔ (𝜑 → ¬ ∅ ∈ (𝐶‘0)))) |
10 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (𝐶‘𝑥) = (𝐶‘𝑘)) |
11 | 10 | eleq2d 2826 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (∅ ∈ (𝐶‘𝑥) ↔ ∅ ∈ (𝐶‘𝑘))) |
12 | 11 | notbid 318 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (¬ ∅ ∈ (𝐶‘𝑥) ↔ ¬ ∅ ∈ (𝐶‘𝑘))) |
13 | 12 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = 𝑘 → ((𝜑 → ¬ ∅ ∈ (𝐶‘𝑥)) ↔ (𝜑 → ¬ ∅ ∈ (𝐶‘𝑘)))) |
14 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝑥 = (𝑘 + 1) → (𝐶‘𝑥) = (𝐶‘(𝑘 + 1))) |
15 | 14 | eleq2d 2826 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (∅ ∈ (𝐶‘𝑥) ↔ ∅ ∈ (𝐶‘(𝑘 + 1)))) |
16 | 15 | notbid 318 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → (¬ ∅ ∈ (𝐶‘𝑥) ↔ ¬ ∅ ∈ (𝐶‘(𝑘 + 1)))) |
17 | 16 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = (𝑘 + 1) → ((𝜑 → ¬ ∅ ∈ (𝐶‘𝑥)) ↔ (𝜑 → ¬ ∅ ∈ (𝐶‘(𝑘 + 1))))) |
18 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝐶‘𝑥) = (𝐶‘𝑁)) |
19 | 18 | eleq2d 2826 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (∅ ∈ (𝐶‘𝑥) ↔ ∅ ∈ (𝐶‘𝑁))) |
20 | 19 | notbid 318 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (¬ ∅ ∈ (𝐶‘𝑥) ↔ ¬ ∅ ∈ (𝐶‘𝑁))) |
21 | 20 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((𝜑 → ¬ ∅ ∈ (𝐶‘𝑥)) ↔ (𝜑 → ¬ ∅ ∈ (𝐶‘𝑁)))) |
22 | 1, 2, 3 | sadc0 16159 |
. . . . 5
⊢ (𝜑 → ¬ ∅ ∈
(𝐶‘0)) |
23 | | noel 4270 |
. . . . . . . . 9
⊢ ¬
𝑘 ∈
∅ |
24 | 1 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
∅ ∈ (𝐶‘𝑘)) → 𝐴 ⊆
ℕ0) |
25 | 2 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
∅ ∈ (𝐶‘𝑘)) → 𝐵 ⊆
ℕ0) |
26 | | simplr 766 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
∅ ∈ (𝐶‘𝑘)) → 𝑘 ∈ ℕ0) |
27 | 24, 25, 3, 26 | sadcp1 16160 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
∅ ∈ (𝐶‘𝑘)) → (∅ ∈ (𝐶‘(𝑘 + 1)) ↔ cadd(𝑘 ∈ 𝐴, 𝑘 ∈ 𝐵, ∅ ∈ (𝐶‘𝑘)))) |
28 | | cad0 1624 |
. . . . . . . . . . 11
⊢ (¬
∅ ∈ (𝐶‘𝑘) → (cadd(𝑘 ∈ 𝐴, 𝑘 ∈ 𝐵, ∅ ∈ (𝐶‘𝑘)) ↔ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵))) |
29 | 28 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
∅ ∈ (𝐶‘𝑘)) → (cadd(𝑘 ∈ 𝐴, 𝑘 ∈ 𝐵, ∅ ∈ (𝐶‘𝑘)) ↔ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵))) |
30 | | elin 3908 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (𝐴 ∩ 𝐵) ↔ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) |
31 | | saddisj.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) |
32 | 31 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
∅ ∈ (𝐶‘𝑘)) → (𝐴 ∩ 𝐵) = ∅) |
33 | 32 | eleq2d 2826 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
∅ ∈ (𝐶‘𝑘)) → (𝑘 ∈ (𝐴 ∩ 𝐵) ↔ 𝑘 ∈ ∅)) |
34 | 30, 33 | bitr3id 285 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
∅ ∈ (𝐶‘𝑘)) → ((𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ 𝑘 ∈ ∅)) |
35 | 27, 29, 34 | 3bitrd 305 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
∅ ∈ (𝐶‘𝑘)) → (∅ ∈ (𝐶‘(𝑘 + 1)) ↔ 𝑘 ∈ ∅)) |
36 | 23, 35 | mtbiri 327 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
∅ ∈ (𝐶‘𝑘)) → ¬ ∅ ∈ (𝐶‘(𝑘 + 1))) |
37 | 36 | ex 413 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (¬
∅ ∈ (𝐶‘𝑘) → ¬ ∅ ∈ (𝐶‘(𝑘 + 1)))) |
38 | 37 | expcom 414 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝜑 → (¬
∅ ∈ (𝐶‘𝑘) → ¬ ∅ ∈ (𝐶‘(𝑘 + 1))))) |
39 | 38 | a2d 29 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ ((𝜑 → ¬
∅ ∈ (𝐶‘𝑘)) → (𝜑 → ¬ ∅ ∈ (𝐶‘(𝑘 + 1))))) |
40 | 9, 13, 17, 21, 22, 39 | nn0ind 12415 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝜑 → ¬
∅ ∈ (𝐶‘𝑁))) |
41 | 4, 40 | mpcom 38 |
. . 3
⊢ (𝜑 → ¬ ∅ ∈
(𝐶‘𝑁)) |
42 | | hadrot 1607 |
. . . 4
⊢
(hadd(∅ ∈ (𝐶‘𝑁), 𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵) ↔ hadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁))) |
43 | | had0 1610 |
. . . 4
⊢ (¬
∅ ∈ (𝐶‘𝑁) → (hadd(∅ ∈ (𝐶‘𝑁), 𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵) ↔ (𝑁 ∈ 𝐴 ⊻ 𝑁 ∈ 𝐵))) |
44 | 42, 43 | bitr3id 285 |
. . 3
⊢ (¬
∅ ∈ (𝐶‘𝑁) → (hadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ (𝑁 ∈ 𝐴 ⊻ 𝑁 ∈ 𝐵))) |
45 | 41, 44 | syl 17 |
. 2
⊢ (𝜑 → (hadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ (𝑁 ∈ 𝐴 ⊻ 𝑁 ∈ 𝐵))) |
46 | | noel 4270 |
. . . . 5
⊢ ¬
𝑁 ∈
∅ |
47 | | elin 3908 |
. . . . . 6
⊢ (𝑁 ∈ (𝐴 ∩ 𝐵) ↔ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵)) |
48 | 31 | eleq2d 2826 |
. . . . . 6
⊢ (𝜑 → (𝑁 ∈ (𝐴 ∩ 𝐵) ↔ 𝑁 ∈ ∅)) |
49 | 47, 48 | bitr3id 285 |
. . . . 5
⊢ (𝜑 → ((𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵) ↔ 𝑁 ∈ ∅)) |
50 | 46, 49 | mtbiri 327 |
. . . 4
⊢ (𝜑 → ¬ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵)) |
51 | | xor2 1513 |
. . . . 5
⊢ ((𝑁 ∈ 𝐴 ⊻ 𝑁 ∈ 𝐵) ↔ ((𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵) ∧ ¬ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵))) |
52 | 51 | rbaib 539 |
. . . 4
⊢ (¬
(𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵) → ((𝑁 ∈ 𝐴 ⊻ 𝑁 ∈ 𝐵) ↔ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵))) |
53 | 50, 52 | syl 17 |
. . 3
⊢ (𝜑 → ((𝑁 ∈ 𝐴 ⊻ 𝑁 ∈ 𝐵) ↔ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵))) |
54 | | elun 4088 |
. . 3
⊢ (𝑁 ∈ (𝐴 ∪ 𝐵) ↔ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵)) |
55 | 53, 54 | bitr4di 289 |
. 2
⊢ (𝜑 → ((𝑁 ∈ 𝐴 ⊻ 𝑁 ∈ 𝐵) ↔ 𝑁 ∈ (𝐴 ∪ 𝐵))) |
56 | 5, 45, 55 | 3bitrd 305 |
1
⊢ (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ 𝑁 ∈ (𝐴 ∪ 𝐵))) |