Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  saddisjlem Structured version   Visualization version   GIF version

 Description: Lemma for sadadd 15810. (Contributed by Mario Carneiro, 9-Sep-2016.)
Hypotheses
Ref Expression
saddisj.1 (𝜑𝐴 ⊆ ℕ0)
saddisj.2 (𝜑𝐵 ⊆ ℕ0)
saddisj.3 (𝜑 → (𝐴𝐵) = ∅)
saddisjlem.c 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
saddisjlem.3 (𝜑𝑁 ∈ ℕ0)
Assertion
Ref Expression
saddisjlem (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ 𝑁 ∈ (𝐴𝐵)))
Distinct variable groups:   𝑚,𝑐,𝑛   𝐴,𝑐,𝑚   𝐵,𝑐,𝑚   𝑛,𝑁
Allowed substitution hints:   𝜑(𝑚,𝑛,𝑐)   𝐴(𝑛)   𝐵(𝑛)   𝐶(𝑚,𝑛,𝑐)   𝑁(𝑚,𝑐)

Proof of Theorem saddisjlem
Dummy variables 𝑘 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef 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)
51, 2, 3, 4sadval 15799 . 2 (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ hadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁))))
6 fveq2 6649 . . . . . . . 8 (𝑥 = 0 → (𝐶𝑥) = (𝐶‘0))
76eleq2d 2878 . . . . . . 7 (𝑥 = 0 → (∅ ∈ (𝐶𝑥) ↔ ∅ ∈ (𝐶‘0)))
87notbid 321 . . . . . 6 (𝑥 = 0 → (¬ ∅ ∈ (𝐶𝑥) ↔ ¬ ∅ ∈ (𝐶‘0)))
98imbi2d 344 . . . . 5 (𝑥 = 0 → ((𝜑 → ¬ ∅ ∈ (𝐶𝑥)) ↔ (𝜑 → ¬ ∅ ∈ (𝐶‘0))))
10 fveq2 6649 . . . . . . . 8 (𝑥 = 𝑘 → (𝐶𝑥) = (𝐶𝑘))
1110eleq2d 2878 . . . . . . 7 (𝑥 = 𝑘 → (∅ ∈ (𝐶𝑥) ↔ ∅ ∈ (𝐶𝑘)))
1211notbid 321 . . . . . 6 (𝑥 = 𝑘 → (¬ ∅ ∈ (𝐶𝑥) ↔ ¬ ∅ ∈ (𝐶𝑘)))
1312imbi2d 344 . . . . 5 (𝑥 = 𝑘 → ((𝜑 → ¬ ∅ ∈ (𝐶𝑥)) ↔ (𝜑 → ¬ ∅ ∈ (𝐶𝑘))))
14 fveq2 6649 . . . . . . . 8 (𝑥 = (𝑘 + 1) → (𝐶𝑥) = (𝐶‘(𝑘 + 1)))
1514eleq2d 2878 . . . . . . 7 (𝑥 = (𝑘 + 1) → (∅ ∈ (𝐶𝑥) ↔ ∅ ∈ (𝐶‘(𝑘 + 1))))
1615notbid 321 . . . . . 6 (𝑥 = (𝑘 + 1) → (¬ ∅ ∈ (𝐶𝑥) ↔ ¬ ∅ ∈ (𝐶‘(𝑘 + 1))))
1716imbi2d 344 . . . . 5 (𝑥 = (𝑘 + 1) → ((𝜑 → ¬ ∅ ∈ (𝐶𝑥)) ↔ (𝜑 → ¬ ∅ ∈ (𝐶‘(𝑘 + 1)))))
18 fveq2 6649 . . . . . . . 8 (𝑥 = 𝑁 → (𝐶𝑥) = (𝐶𝑁))
1918eleq2d 2878 . . . . . . 7 (𝑥 = 𝑁 → (∅ ∈ (𝐶𝑥) ↔ ∅ ∈ (𝐶𝑁)))
2019notbid 321 . . . . . 6 (𝑥 = 𝑁 → (¬ ∅ ∈ (𝐶𝑥) ↔ ¬ ∅ ∈ (𝐶𝑁)))
2120imbi2d 344 . . . . 5 (𝑥 = 𝑁 → ((𝜑 → ¬ ∅ ∈ (𝐶𝑥)) ↔ (𝜑 → ¬ ∅ ∈ (𝐶𝑁))))
221, 2, 3sadc0 15797 . . . . 5 (𝜑 → ¬ ∅ ∈ (𝐶‘0))
23 noel 4250 . . . . . . . . 9 ¬ 𝑘 ∈ ∅
241ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ ∅ ∈ (𝐶𝑘)) → 𝐴 ⊆ ℕ0)
252ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ ∅ ∈ (𝐶𝑘)) → 𝐵 ⊆ ℕ0)
26 simplr 768 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ ∅ ∈ (𝐶𝑘)) → 𝑘 ∈ ℕ0)
2724, 25, 3, 26sadcp1 15798 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ ∅ ∈ (𝐶𝑘)) → (∅ ∈ (𝐶‘(𝑘 + 1)) ↔ cadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))))
28 cad0 1619 . . . . . . . . . . 11 (¬ ∅ ∈ (𝐶𝑘) → (cadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘)) ↔ (𝑘𝐴𝑘𝐵)))
2928adantl 485 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ ∅ ∈ (𝐶𝑘)) → (cadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘)) ↔ (𝑘𝐴𝑘𝐵)))
30 elin 3900 . . . . . . . . . . 11 (𝑘 ∈ (𝐴𝐵) ↔ (𝑘𝐴𝑘𝐵))
31 saddisj.3 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐵) = ∅)
3231ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ ∅ ∈ (𝐶𝑘)) → (𝐴𝐵) = ∅)
3332eleq2d 2878 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ ∅ ∈ (𝐶𝑘)) → (𝑘 ∈ (𝐴𝐵) ↔ 𝑘 ∈ ∅))
3430, 33bitr3id 288 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ ∅ ∈ (𝐶𝑘)) → ((𝑘𝐴𝑘𝐵) ↔ 𝑘 ∈ ∅))
3527, 29, 343bitrd 308 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ ∅ ∈ (𝐶𝑘)) → (∅ ∈ (𝐶‘(𝑘 + 1)) ↔ 𝑘 ∈ ∅))
3623, 35mtbiri 330 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ ∅ ∈ (𝐶𝑘)) → ¬ ∅ ∈ (𝐶‘(𝑘 + 1)))
3736ex 416 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (¬ ∅ ∈ (𝐶𝑘) → ¬ ∅ ∈ (𝐶‘(𝑘 + 1))))
3837expcom 417 . . . . . 6 (𝑘 ∈ ℕ0 → (𝜑 → (¬ ∅ ∈ (𝐶𝑘) → ¬ ∅ ∈ (𝐶‘(𝑘 + 1)))))
3938a2d 29 . . . . 5 (𝑘 ∈ ℕ0 → ((𝜑 → ¬ ∅ ∈ (𝐶𝑘)) → (𝜑 → ¬ ∅ ∈ (𝐶‘(𝑘 + 1)))))
409, 13, 17, 21, 22, 39nn0ind 12069 . . . 4 (𝑁 ∈ ℕ0 → (𝜑 → ¬ ∅ ∈ (𝐶𝑁)))
414, 40mpcom 38 . . 3 (𝜑 → ¬ ∅ ∈ (𝐶𝑁))
42 hadrot 1603 . . . 4 (hadd(∅ ∈ (𝐶𝑁), 𝑁𝐴, 𝑁𝐵) ↔ hadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)))
43 had0 1606 . . . 4 (¬ ∅ ∈ (𝐶𝑁) → (hadd(∅ ∈ (𝐶𝑁), 𝑁𝐴, 𝑁𝐵) ↔ (𝑁𝐴𝑁𝐵)))
4442, 43bitr3id 288 . . 3 (¬ ∅ ∈ (𝐶𝑁) → (hadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ (𝑁𝐴𝑁𝐵)))
4541, 44syl 17 . 2 (𝜑 → (hadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ (𝑁𝐴𝑁𝐵)))
46 noel 4250 . . . . 5 ¬ 𝑁 ∈ ∅
47 elin 3900 . . . . . 6 (𝑁 ∈ (𝐴𝐵) ↔ (𝑁𝐴𝑁𝐵))
4831eleq2d 2878 . . . . . 6 (𝜑 → (𝑁 ∈ (𝐴𝐵) ↔ 𝑁 ∈ ∅))
4947, 48bitr3id 288 . . . . 5 (𝜑 → ((𝑁𝐴𝑁𝐵) ↔ 𝑁 ∈ ∅))
5046, 49mtbiri 330 . . . 4 (𝜑 → ¬ (𝑁𝐴𝑁𝐵))
51 xor2 1509 . . . . 5 ((𝑁𝐴𝑁𝐵) ↔ ((𝑁𝐴𝑁𝐵) ∧ ¬ (𝑁𝐴𝑁𝐵)))
5251rbaib 542 . . . 4 (¬ (𝑁𝐴𝑁𝐵) → ((𝑁𝐴𝑁𝐵) ↔ (𝑁𝐴𝑁𝐵)))
5350, 52syl 17 . . 3 (𝜑 → ((𝑁𝐴𝑁𝐵) ↔ (𝑁𝐴𝑁𝐵)))
54 elun 4079 . . 3 (𝑁 ∈ (𝐴𝐵) ↔ (𝑁𝐴𝑁𝐵))
5553, 54syl6bbr 292 . 2 (𝜑 → ((𝑁𝐴𝑁𝐵) ↔ 𝑁 ∈ (𝐴𝐵)))
565, 45, 553bitrd 308 1 (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ 𝑁 ∈ (𝐴𝐵)))