| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sadcp1.n | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 2 |  | nn0uz 12920 | . . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) | 
| 3 | 1, 2 | eleqtrdi 2851 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) | 
| 4 |  | seqp1 14057 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘0) → (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))))‘(𝑁 + 1)) =
((seq0((𝑐 ∈
2o, 𝑚 ∈
ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))))‘𝑁)(𝑐 ∈ 2o, 𝑚 ∈ ℕ0
↦ if(cadd(𝑚 ∈
𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅))((𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))‘(𝑁 +
1)))) | 
| 5 | 3, 4 | syl 17 | . . . . 5
⊢ (𝜑 → (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))))‘(𝑁 + 1)) =
((seq0((𝑐 ∈
2o, 𝑚 ∈
ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))))‘𝑁)(𝑐 ∈ 2o, 𝑚 ∈ ℕ0
↦ if(cadd(𝑚 ∈
𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅))((𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))‘(𝑁 +
1)))) | 
| 6 |  | sadval.c | . . . . . 6
⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))) | 
| 7 | 6 | fveq1i 6907 | . . . . 5
⊢ (𝐶‘(𝑁 + 1)) = (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))))‘(𝑁 +
1)) | 
| 8 | 6 | fveq1i 6907 | . . . . . 6
⊢ (𝐶‘𝑁) = (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))))‘𝑁) | 
| 9 | 8 | oveq1i 7441 | . . . . 5
⊢ ((𝐶‘𝑁)(𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅))((𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))‘(𝑁 + 1))) =
((seq0((𝑐 ∈
2o, 𝑚 ∈
ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))))‘𝑁)(𝑐 ∈ 2o, 𝑚 ∈ ℕ0
↦ if(cadd(𝑚 ∈
𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅))((𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))‘(𝑁 +
1))) | 
| 10 | 5, 7, 9 | 3eqtr4g 2802 | . . . 4
⊢ (𝜑 → (𝐶‘(𝑁 + 1)) = ((𝐶‘𝑁)(𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅))((𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))‘(𝑁 +
1)))) | 
| 11 |  | peano2nn0 12566 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) | 
| 12 |  | eqeq1 2741 | . . . . . . . . 9
⊢ (𝑛 = (𝑁 + 1) → (𝑛 = 0 ↔ (𝑁 + 1) = 0)) | 
| 13 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑛 = (𝑁 + 1) → (𝑛 − 1) = ((𝑁 + 1) − 1)) | 
| 14 | 12, 13 | ifbieq2d 4552 | . . . . . . . 8
⊢ (𝑛 = (𝑁 + 1) → if(𝑛 = 0, ∅, (𝑛 − 1)) = if((𝑁 + 1) = 0, ∅, ((𝑁 + 1) − 1))) | 
| 15 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 − 1))) = (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))) | 
| 16 |  | 0ex 5307 | . . . . . . . . 9
⊢ ∅
∈ V | 
| 17 |  | ovex 7464 | . . . . . . . . 9
⊢ ((𝑁 + 1) − 1) ∈
V | 
| 18 | 16, 17 | ifex 4576 | . . . . . . . 8
⊢ if((𝑁 + 1) = 0, ∅, ((𝑁 + 1) − 1)) ∈
V | 
| 19 | 14, 15, 18 | fvmpt 7016 | . . . . . . 7
⊢ ((𝑁 + 1) ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))‘(𝑁 + 1)) = if((𝑁 + 1) = 0, ∅, ((𝑁 + 1) − 1))) | 
| 20 | 1, 11, 19 | 3syl 18 | . . . . . 6
⊢ (𝜑 → ((𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))‘(𝑁 + 1)) = if((𝑁 + 1) = 0, ∅, ((𝑁 + 1) − 1))) | 
| 21 |  | nn0p1nn 12565 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) | 
| 22 | 1, 21 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (𝑁 + 1) ∈ ℕ) | 
| 23 | 22 | nnne0d 12316 | . . . . . . 7
⊢ (𝜑 → (𝑁 + 1) ≠ 0) | 
| 24 |  | ifnefalse 4537 | . . . . . . 7
⊢ ((𝑁 + 1) ≠ 0 → if((𝑁 + 1) = 0, ∅, ((𝑁 + 1) − 1)) = ((𝑁 + 1) −
1)) | 
| 25 | 23, 24 | syl 17 | . . . . . 6
⊢ (𝜑 → if((𝑁 + 1) = 0, ∅, ((𝑁 + 1) − 1)) = ((𝑁 + 1) − 1)) | 
| 26 | 1 | nn0cnd 12589 | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 27 |  | 1cnd 11256 | . . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) | 
| 28 | 26, 27 | pncand 11621 | . . . . . 6
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) | 
| 29 | 20, 25, 28 | 3eqtrd 2781 | . . . . 5
⊢ (𝜑 → ((𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))‘(𝑁 + 1)) = 𝑁) | 
| 30 | 29 | oveq2d 7447 | . . . 4
⊢ (𝜑 → ((𝐶‘𝑁)(𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅))((𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))‘(𝑁 + 1))) =
((𝐶‘𝑁)(𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅))𝑁)) | 
| 31 |  | sadval.a | . . . . . . 7
⊢ (𝜑 → 𝐴 ⊆
ℕ0) | 
| 32 |  | sadval.b | . . . . . . 7
⊢ (𝜑 → 𝐵 ⊆
ℕ0) | 
| 33 | 31, 32, 6 | sadcf 16490 | . . . . . 6
⊢ (𝜑 → 𝐶:ℕ0⟶2o) | 
| 34 | 33, 1 | ffvelcdmd 7105 | . . . . 5
⊢ (𝜑 → (𝐶‘𝑁) ∈ 2o) | 
| 35 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝑥 = (𝐶‘𝑁) ∧ 𝑦 = 𝑁) → 𝑦 = 𝑁) | 
| 36 | 35 | eleq1d 2826 | . . . . . . . 8
⊢ ((𝑥 = (𝐶‘𝑁) ∧ 𝑦 = 𝑁) → (𝑦 ∈ 𝐴 ↔ 𝑁 ∈ 𝐴)) | 
| 37 | 35 | eleq1d 2826 | . . . . . . . 8
⊢ ((𝑥 = (𝐶‘𝑁) ∧ 𝑦 = 𝑁) → (𝑦 ∈ 𝐵 ↔ 𝑁 ∈ 𝐵)) | 
| 38 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑥 = (𝐶‘𝑁) ∧ 𝑦 = 𝑁) → 𝑥 = (𝐶‘𝑁)) | 
| 39 | 38 | eleq2d 2827 | . . . . . . . 8
⊢ ((𝑥 = (𝐶‘𝑁) ∧ 𝑦 = 𝑁) → (∅ ∈ 𝑥 ↔ ∅ ∈ (𝐶‘𝑁))) | 
| 40 | 36, 37, 39 | cadbi123d 1610 | . . . . . . 7
⊢ ((𝑥 = (𝐶‘𝑁) ∧ 𝑦 = 𝑁) → (cadd(𝑦 ∈ 𝐴, 𝑦 ∈ 𝐵, ∅ ∈ 𝑥) ↔ cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)))) | 
| 41 | 40 | ifbid 4549 | . . . . . 6
⊢ ((𝑥 = (𝐶‘𝑁) ∧ 𝑦 = 𝑁) → if(cadd(𝑦 ∈ 𝐴, 𝑦 ∈ 𝐵, ∅ ∈ 𝑥), 1o, ∅) = if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), 1o,
∅)) | 
| 42 |  | biidd 262 | . . . . . . . . 9
⊢ (𝑐 = 𝑥 → (𝑚 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴)) | 
| 43 |  | biidd 262 | . . . . . . . . 9
⊢ (𝑐 = 𝑥 → (𝑚 ∈ 𝐵 ↔ 𝑚 ∈ 𝐵)) | 
| 44 |  | eleq2w 2825 | . . . . . . . . 9
⊢ (𝑐 = 𝑥 → (∅ ∈ 𝑐 ↔ ∅ ∈ 𝑥)) | 
| 45 | 42, 43, 44 | cadbi123d 1610 | . . . . . . . 8
⊢ (𝑐 = 𝑥 → (cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐) ↔ cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑥))) | 
| 46 | 45 | ifbid 4549 | . . . . . . 7
⊢ (𝑐 = 𝑥 → if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅) = if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑥), 1o, ∅)) | 
| 47 |  | eleq1w 2824 | . . . . . . . . 9
⊢ (𝑚 = 𝑦 → (𝑚 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | 
| 48 |  | eleq1w 2824 | . . . . . . . . 9
⊢ (𝑚 = 𝑦 → (𝑚 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) | 
| 49 |  | biidd 262 | . . . . . . . . 9
⊢ (𝑚 = 𝑦 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝑥)) | 
| 50 | 47, 48, 49 | cadbi123d 1610 | . . . . . . . 8
⊢ (𝑚 = 𝑦 → (cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑥) ↔ cadd(𝑦 ∈ 𝐴, 𝑦 ∈ 𝐵, ∅ ∈ 𝑥))) | 
| 51 | 50 | ifbid 4549 | . . . . . . 7
⊢ (𝑚 = 𝑦 → if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑥), 1o, ∅) = if(cadd(𝑦 ∈ 𝐴, 𝑦 ∈ 𝐵, ∅ ∈ 𝑥), 1o, ∅)) | 
| 52 | 46, 51 | cbvmpov 7528 | . . . . . 6
⊢ (𝑐 ∈ 2o, 𝑚 ∈ ℕ0
↦ if(cadd(𝑚 ∈
𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)) = (𝑥 ∈ 2o, 𝑦 ∈ ℕ0
↦ if(cadd(𝑦 ∈
𝐴, 𝑦 ∈ 𝐵, ∅ ∈ 𝑥), 1o, ∅)) | 
| 53 |  | 1oex 8516 | . . . . . . 7
⊢
1o ∈ V | 
| 54 | 53, 16 | ifex 4576 | . . . . . 6
⊢
if(cadd(𝑁 ∈
𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), 1o, ∅) ∈
V | 
| 55 | 41, 52, 54 | ovmpoa 7588 | . . . . 5
⊢ (((𝐶‘𝑁) ∈ 2o ∧ 𝑁 ∈ ℕ0)
→ ((𝐶‘𝑁)(𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅))𝑁) = if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), 1o,
∅)) | 
| 56 | 34, 1, 55 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((𝐶‘𝑁)(𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅))𝑁) = if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), 1o,
∅)) | 
| 57 | 10, 30, 56 | 3eqtrd 2781 | . . 3
⊢ (𝜑 → (𝐶‘(𝑁 + 1)) = if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), 1o,
∅)) | 
| 58 | 57 | eleq2d 2827 | . 2
⊢ (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ ∅ ∈ if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), 1o,
∅))) | 
| 59 |  | noel 4338 | . . . . 5
⊢  ¬
∅ ∈ ∅ | 
| 60 |  | iffalse 4534 | . . . . . 6
⊢ (¬
cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) → if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), 1o, ∅) =
∅) | 
| 61 | 60 | eleq2d 2827 | . . . . 5
⊢ (¬
cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) → (∅ ∈ if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), 1o, ∅) ↔ ∅
∈ ∅)) | 
| 62 | 59, 61 | mtbiri 327 | . . . 4
⊢ (¬
cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) → ¬ ∅ ∈ if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), 1o,
∅)) | 
| 63 | 62 | con4i 114 | . . 3
⊢ (∅
∈ if(cadd(𝑁 ∈
𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), 1o, ∅) →
cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁))) | 
| 64 |  | 0lt1o 8542 | . . . 4
⊢ ∅
∈ 1o | 
| 65 |  | iftrue 4531 | . . . 4
⊢
(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) → if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), 1o, ∅) =
1o) | 
| 66 | 64, 65 | eleqtrrid 2848 | . . 3
⊢
(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) → ∅ ∈ if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), 1o,
∅)) | 
| 67 | 63, 66 | impbii 209 | . 2
⊢ (∅
∈ if(cadd(𝑁 ∈
𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), 1o, ∅) ↔
cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁))) | 
| 68 | 58, 67 | bitrdi 287 | 1
⊢ (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)))) |