Step |
Hyp |
Ref |
Expression |
1 |
|
saddisj.1 |
⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 ) |
2 |
|
saddisj.2 |
⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 ) |
3 |
|
saddisj.3 |
⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ ) |
4 |
|
sadcl |
⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ) → ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 ) |
5 |
1 2 4
|
syl2anc |
⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 ) |
6 |
5
|
sseld |
⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 sadd 𝐵 ) → 𝑘 ∈ ℕ0 ) ) |
7 |
1 2
|
unssd |
⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ ℕ0 ) |
8 |
7
|
sseld |
⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) → 𝑘 ∈ ℕ0 ) ) |
9 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ⊆ ℕ0 ) |
10 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ⊆ ℕ0 ) |
11 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ∩ 𝐵 ) = ∅ ) |
12 |
|
eqid |
⊢ seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ∅ , ( 𝑥 − 1 ) ) ) ) = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ∅ , ( 𝑥 − 1 ) ) ) ) |
13 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 ) |
14 |
9 10 11 12 13
|
saddisjlem |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ( 𝐴 sadd 𝐵 ) ↔ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) ) |
15 |
14
|
ex |
⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 → ( 𝑘 ∈ ( 𝐴 sadd 𝐵 ) ↔ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) ) ) |
16 |
6 8 15
|
pm5.21ndd |
⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 sadd 𝐵 ) ↔ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) ) |
17 |
16
|
eqrdv |
⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) = ( 𝐴 ∪ 𝐵 ) ) |