Metamath Proof Explorer

Theorem saddisjlem

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

Ref Expression
Hypotheses saddisj.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
saddisj.2 ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
saddisj.3 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
saddisjlem.c ⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
saddisjlem.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion saddisjlem ( 𝜑 → ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) ↔ 𝑁 ∈ ( 𝐴 ∪ 𝐵 ) ) )

Proof

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