Metamath Proof Explorer

Theorem eulerpartlemt0

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 19-Sep-2017)

Ref Expression
Hypotheses eulerpart.p ⊢P=f∈ℕ0ℕ|f-1ℕ∈Fin∧∑k∈ℕf⁡k⁢k=N
eulerpart.o ⊢O=g∈P|∀n∈g-1ℕ¬2∥n
eulerpart.d ⊢D=g∈P|∀n∈ℕg⁡n≤1
eulerpart.j ⊢J=z∈ℕ|¬2∥z
eulerpart.f ⊢F=x∈J,y∈ℕ0⟼2y⁢x
eulerpart.h ⊢H=r∈𝒫ℕ0∩FinJ|rsupp∅∈Fin
eulerpart.m ⊢M=r∈H⟼xy|x∈J∧y∈r⁡x
eulerpart.r ⊢R=f|f-1ℕ∈Fin
eulerpart.t ⊢T=f∈ℕ0ℕ|f-1ℕ⊆J
Assertion eulerpartlemt0 ⊢A∈T∩R↔A∈ℕ0ℕ∧A-1ℕ∈Fin∧A-1ℕ⊆J

Proof

Step Hyp Ref Expression
1 eulerpart.p ⊢P=f∈ℕ0ℕ|f-1ℕ∈Fin∧∑k∈ℕf⁡k⁢k=N
2 eulerpart.o ⊢O=g∈P|∀n∈g-1ℕ¬2∥n
3 eulerpart.d ⊢D=g∈P|∀n∈ℕg⁡n≤1
4 eulerpart.j ⊢J=z∈ℕ|¬2∥z
5 eulerpart.f ⊢F=x∈J,y∈ℕ0⟼2y⁢x
6 eulerpart.h ⊢H=r∈𝒫ℕ0∩FinJ|rsupp∅∈Fin
7 eulerpart.m ⊢M=r∈H⟼xy|x∈J∧y∈r⁡x
8 eulerpart.r ⊢R=f|f-1ℕ∈Fin
9 eulerpart.t ⊢T=f∈ℕ0ℕ|f-1ℕ⊆J
10 cnveq ⊢f=A→f-1=A-1
11 10 imaeq1d ⊢f=A→f-1ℕ=A-1ℕ
12 11 sseq1d ⊢f=A→f-1ℕ⊆J↔A-1ℕ⊆J
13 12 9 elrab2 ⊢A∈T↔A∈ℕ0ℕ∧A-1ℕ⊆J
14 11 eleq1d ⊢f=A→f-1ℕ∈Fin↔A-1ℕ∈Fin
15 14 8 elab4g ⊢A∈R↔A∈V∧A-1ℕ∈Fin
16 13 15 anbi12i ⊢A∈T∧A∈R↔A∈ℕ0ℕ∧A-1ℕ⊆J∧A∈V∧A-1ℕ∈Fin
17 elin ⊢A∈T∩R↔A∈T∧A∈R
18 elex ⊢A∈ℕ0ℕ→A∈V
19 18 pm4.71i ⊢A∈ℕ0ℕ↔A∈ℕ0ℕ∧A∈V
20 19 anbi1i ⊢A∈ℕ0ℕ∧A-1ℕ∈Fin∧A-1ℕ⊆J↔A∈ℕ0ℕ∧A∈V∧A-1ℕ∈Fin∧A-1ℕ⊆J
21 3anass ⊢A∈ℕ0ℕ∧A-1ℕ∈Fin∧A-1ℕ⊆J↔A∈ℕ0ℕ∧A-1ℕ∈Fin∧A-1ℕ⊆J
22 an42 ⊢A∈ℕ0ℕ∧A-1ℕ⊆J∧A∈V∧A-1ℕ∈Fin↔A∈ℕ0ℕ∧A∈V∧A-1ℕ∈Fin∧A-1ℕ⊆J
23 20 21 22 3bitr4i ⊢A∈ℕ0ℕ∧A-1ℕ∈Fin∧A-1ℕ⊆J↔A∈ℕ0ℕ∧A-1ℕ⊆J∧A∈V∧A-1ℕ∈Fin
24 16 17 23 3bitr4i ⊢A∈T∩R↔A∈ℕ0ℕ∧A-1ℕ∈Fin∧A-1ℕ⊆J