Metamath Proof Explorer

Theorem saddisjlem

Description: Lemma for sadadd . (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses saddisj.1 ⊢ φ → A ⊆ ℕ 0
saddisj.2 ⊢ φ → B ⊆ ℕ 0
saddisj.3 ⊢ φ → A ∩ B = ∅
saddisjlem.c ⊢ C = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
saddisjlem.3 ⊢ φ → N ∈ ℕ 0
Assertion saddisjlem ⊢ φ → N ∈ A sadd B ↔ N ∈ A ∪ B

Proof

Step Hyp Ref Expression
1 saddisj.1 ⊢ φ → A ⊆ ℕ 0
2 saddisj.2 ⊢ φ → B ⊆ ℕ 0
3 saddisj.3 ⊢ φ → A ∩ B = ∅
4 saddisjlem.c ⊢ C = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
5 saddisjlem.3 ⊢ φ → N ∈ ℕ 0
6 1 2 4 5 sadval ⊢ φ → N ∈ A sadd B ↔ hadd N ∈ A N ∈ B ∅ ∈ C ⁡ N
7 fveq2 ⊢ x = 0 → C ⁡ x = C ⁡ 0
8 7 eleq2d ⊢ x = 0 → ∅ ∈ C ⁡ x ↔ ∅ ∈ C ⁡ 0
9 8 notbid ⊢ x = 0 → ¬ ∅ ∈ C ⁡ x ↔ ¬ ∅ ∈ C ⁡ 0
10 9 imbi2d ⊢ x = 0 → φ → ¬ ∅ ∈ C ⁡ x ↔ φ → ¬ ∅ ∈ C ⁡ 0
11 fveq2 ⊢ x = k → C ⁡ x = C ⁡ k
12 11 eleq2d ⊢ x = k → ∅ ∈ C ⁡ x ↔ ∅ ∈ C ⁡ k
13 12 notbid ⊢ x = k → ¬ ∅ ∈ C ⁡ x ↔ ¬ ∅ ∈ C ⁡ k
14 13 imbi2d ⊢ x = k → φ → ¬ ∅ ∈ C ⁡ x ↔ φ → ¬ ∅ ∈ C ⁡ k
15 fveq2 ⊢ x = k + 1 → C ⁡ x = C ⁡ k + 1
16 15 eleq2d ⊢ x = k + 1 → ∅ ∈ C ⁡ x ↔ ∅ ∈ C ⁡ k + 1
17 16 notbid ⊢ x = k + 1 → ¬ ∅ ∈ C ⁡ x ↔ ¬ ∅ ∈ C ⁡ k + 1
18 17 imbi2d ⊢ x = k + 1 → φ → ¬ ∅ ∈ C ⁡ x ↔ φ → ¬ ∅ ∈ C ⁡ k + 1
19 fveq2 ⊢ x = N → C ⁡ x = C ⁡ N
20 19 eleq2d ⊢ x = N → ∅ ∈ C ⁡ x ↔ ∅ ∈ C ⁡ N
21 20 notbid ⊢ x = N → ¬ ∅ ∈ C ⁡ x ↔ ¬ ∅ ∈ C ⁡ N
22 21 imbi2d ⊢ x = N → φ → ¬ ∅ ∈ C ⁡ x ↔ φ → ¬ ∅ ∈ C ⁡ N
23 1 2 4 sadc0 ⊢ φ → ¬ ∅ ∈ C ⁡ 0
24 noel ⊢ ¬ k ∈ ∅
25 1 ad2antrr ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ ∅ ∈ C ⁡ k → A ⊆ ℕ 0
26 2 ad2antrr ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ ∅ ∈ C ⁡ k → B ⊆ ℕ 0
27 simplr ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ ∅ ∈ C ⁡ k → k ∈ ℕ 0
28 25 26 4 27 sadcp1 ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ ∅ ∈ C ⁡ k → ∅ ∈ C ⁡ k + 1 ↔ cadd k ∈ A k ∈ B ∅ ∈ C ⁡ k
29 cad0 ⊢ ¬ ∅ ∈ C ⁡ k → cadd k ∈ A k ∈ B ∅ ∈ C ⁡ k ↔ k ∈ A ∧ k ∈ B
30 29 adantl ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ ∅ ∈ C ⁡ k → cadd k ∈ A k ∈ B ∅ ∈ C ⁡ k ↔ k ∈ A ∧ k ∈ B
31 elin ⊢ k ∈ A ∩ B ↔ k ∈ A ∧ k ∈ B
32 3 ad2antrr ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ ∅ ∈ C ⁡ k → A ∩ B = ∅
33 32 eleq2d ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ ∅ ∈ C ⁡ k → k ∈ A ∩ B ↔ k ∈ ∅
34 31 33 bitr3id ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ ∅ ∈ C ⁡ k → k ∈ A ∧ k ∈ B ↔ k ∈ ∅
35 28 30 34 3bitrd ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ ∅ ∈ C ⁡ k → ∅ ∈ C ⁡ k + 1 ↔ k ∈ ∅
36 24 35 mtbiri ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ ∅ ∈ C ⁡ k → ¬ ∅ ∈ C ⁡ k + 1
37 36 ex ⊢ φ ∧ k ∈ ℕ 0 → ¬ ∅ ∈ C ⁡ k → ¬ ∅ ∈ C ⁡ k + 1
38 37 expcom ⊢ k ∈ ℕ 0 → φ → ¬ ∅ ∈ C ⁡ k → ¬ ∅ ∈ C ⁡ k + 1
39 38 a2d ⊢ k ∈ ℕ 0 → φ → ¬ ∅ ∈ C ⁡ k → φ → ¬ ∅ ∈ C ⁡ k + 1
40 10 14 18 22 23 39 nn0ind ⊢ N ∈ ℕ 0 → φ → ¬ ∅ ∈ C ⁡ N
41 5 40 mpcom ⊢ φ → ¬ ∅ ∈ C ⁡ N
42 hadrot ⊢ hadd ∅ ∈ C ⁡ N N ∈ A N ∈ B ↔ hadd N ∈ A N ∈ B ∅ ∈ C ⁡ N
43 had0 ⊢ ¬ ∅ ∈ C ⁡ N → hadd ∅ ∈ C ⁡ N N ∈ A N ∈ B ↔ N ∈ A ⊻ N ∈ B
44 42 43 bitr3id ⊢ ¬ ∅ ∈ C ⁡ N → hadd N ∈ A N ∈ B ∅ ∈ C ⁡ N ↔ N ∈ A ⊻ N ∈ B
45 41 44 syl ⊢ φ → hadd N ∈ A N ∈ B ∅ ∈ C ⁡ N ↔ N ∈ A ⊻ N ∈ B
46 noel ⊢ ¬ N ∈ ∅
47 elin ⊢ N ∈ A ∩ B ↔ N ∈ A ∧ N ∈ B
48 3 eleq2d ⊢ φ → N ∈ A ∩ B ↔ N ∈ ∅
49 47 48 bitr3id ⊢ φ → N ∈ A ∧ N ∈ B ↔ N ∈ ∅
50 46 49 mtbiri ⊢ φ → ¬ N ∈ A ∧ N ∈ B
51 xor2 ⊢ N ∈ A ⊻ N ∈ B ↔ N ∈ A ∨ N ∈ B ∧ ¬ N ∈ A ∧ N ∈ B
52 51 rbaib ⊢ ¬ N ∈ A ∧ N ∈ B → N ∈ A ⊻ N ∈ B ↔ N ∈ A ∨ N ∈ B
53 50 52 syl ⊢ φ → N ∈ A ⊻ N ∈ B ↔ N ∈ A ∨ N ∈ B
54 elun ⊢ N ∈ A ∪ B ↔ N ∈ A ∨ N ∈ B
55 53 54 bitr4di ⊢ φ → N ∈ A ⊻ N ∈ B ↔ N ∈ A ∪ B
56 6 45 55 3bitrd ⊢ φ → N ∈ A sadd B ↔ N ∈ A ∪ B