Metamath Proof Explorer

Theorem vdwmc2

Description: Expand out the definition of an arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdwmc.1 ⊢X∈V
vdwmc.2 ⊢φ→K∈ℕ0
vdwmc.3 ⊢φ→F:X⟶R
vdwmc2.4 ⊢φ→A∈X
Assertion vdwmc2 ⊢φ→KMonoAPF↔∃c∈R∃a∈ℕ∃d∈ℕ∀m∈0…K−1a+m⁢d∈F-1c

Proof

Step Hyp Ref Expression
1 vdwmc.1 ⊢X∈V
2 vdwmc.2 ⊢φ→K∈ℕ0
3 vdwmc.3 ⊢φ→F:X⟶R
4 vdwmc2.4 ⊢φ→A∈X
5 1 2 3 vdwmc ⊢φ→KMonoAPF↔∃c∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
6 vdwapid1 ⊢K∈ℕ∧a∈ℕ∧d∈ℕ→a∈aAP⁡Kd
7 6 ne0d ⊢K∈ℕ∧a∈ℕ∧d∈ℕ→aAP⁡Kd≠∅
8 7 3expb ⊢K∈ℕ∧a∈ℕ∧d∈ℕ→aAP⁡Kd≠∅
9 8 adantll ⊢φ∧K∈ℕ∧a∈ℕ∧d∈ℕ→aAP⁡Kd≠∅
10 ssn0 ⊢aAP⁡Kd⊆F-1c∧aAP⁡Kd≠∅→F-1c≠∅
11 10 expcom ⊢aAP⁡Kd≠∅→aAP⁡Kd⊆F-1c→F-1c≠∅
12 9 11 syl ⊢φ∧K∈ℕ∧a∈ℕ∧d∈ℕ→aAP⁡Kd⊆F-1c→F-1c≠∅
13 disjsn ⊢R∩c=∅↔¬c∈R
14 3 adantr ⊢φ∧K∈ℕ→F:X⟶R
15 fimacnvdisj ⊢F:X⟶R∧R∩c=∅→F-1c=∅
16 15 ex ⊢F:X⟶R→R∩c=∅→F-1c=∅
17 14 16 syl ⊢φ∧K∈ℕ→R∩c=∅→F-1c=∅
18 17 adantr ⊢φ∧K∈ℕ∧a∈ℕ∧d∈ℕ→R∩c=∅→F-1c=∅
19 13 18 biimtrrid ⊢φ∧K∈ℕ∧a∈ℕ∧d∈ℕ→¬c∈R→F-1c=∅
20 19 necon1ad ⊢φ∧K∈ℕ∧a∈ℕ∧d∈ℕ→F-1c≠∅→c∈R
21 12 20 syld ⊢φ∧K∈ℕ∧a∈ℕ∧d∈ℕ→aAP⁡Kd⊆F-1c→c∈R
22 21 rexlimdvva ⊢φ∧K∈ℕ→∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c→c∈R
23 22 pm4.71rd ⊢φ∧K∈ℕ→∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c↔c∈R∧∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
24 23 exbidv ⊢φ∧K∈ℕ→∃c∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c↔∃cc∈R∧∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
25 df-rex ⊢∃c∈R∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c↔∃cc∈R∧∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
26 24 25 bitr4di ⊢φ∧K∈ℕ→∃c∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c↔∃c∈R∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
27 3 4 ffvelcdmd ⊢φ→F⁡A∈R
28 27 ne0d ⊢φ→R≠∅
29 1nn ⊢1∈ℕ
30 29 ne0ii ⊢ℕ≠∅
31 simpllr ⊢φ∧K=0∧a∈ℕ∧d∈ℕ→K=0
32 31 fveq2d ⊢φ∧K=0∧a∈ℕ∧d∈ℕ→AP⁡K=AP⁡0
33 32 oveqd ⊢φ∧K=0∧a∈ℕ∧d∈ℕ→aAP⁡Kd=aAP⁡0d
34 vdwap0 ⊢a∈ℕ∧d∈ℕ→aAP⁡0d=∅
35 34 adantll ⊢φ∧K=0∧a∈ℕ∧d∈ℕ→aAP⁡0d=∅
36 33 35 eqtrd ⊢φ∧K=0∧a∈ℕ∧d∈ℕ→aAP⁡Kd=∅
37 0ss ⊢∅⊆F-1c
38 36 37 eqsstrdi ⊢φ∧K=0∧a∈ℕ∧d∈ℕ→aAP⁡Kd⊆F-1c
39 38 ralrimiva ⊢φ∧K=0∧a∈ℕ→∀d∈ℕaAP⁡Kd⊆F-1c
40 r19.2z ⊢ℕ≠∅∧∀d∈ℕaAP⁡Kd⊆F-1c→∃d∈ℕaAP⁡Kd⊆F-1c
41 30 39 40 sylancr ⊢φ∧K=0∧a∈ℕ→∃d∈ℕaAP⁡Kd⊆F-1c
42 41 ralrimiva ⊢φ∧K=0→∀a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
43 r19.2z ⊢ℕ≠∅∧∀a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c→∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
44 30 42 43 sylancr ⊢φ∧K=0→∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
45 44 ralrimivw ⊢φ∧K=0→∀c∈R∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
46 r19.2z ⊢R≠∅∧∀c∈R∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c→∃c∈R∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
47 28 45 46 syl2an2r ⊢φ∧K=0→∃c∈R∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
48 rexex ⊢∃c∈R∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c→∃c∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
49 47 48 syl ⊢φ∧K=0→∃c∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
50 49 47 2thd ⊢φ∧K=0→∃c∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c↔∃c∈R∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
51 elnn0 ⊢K∈ℕ0↔K∈ℕ∨K=0
52 2 51 sylib ⊢φ→K∈ℕ∨K=0
53 26 50 52 mpjaodan ⊢φ→∃c∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c↔∃c∈R∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c
54 vdwapval ⊢K∈ℕ0∧a∈ℕ∧d∈ℕ→x∈aAP⁡Kd↔∃m∈0…K−1x=a+m⁢d
55 54 3expb ⊢K∈ℕ0∧a∈ℕ∧d∈ℕ→x∈aAP⁡Kd↔∃m∈0…K−1x=a+m⁢d
56 2 55 sylan ⊢φ∧a∈ℕ∧d∈ℕ→x∈aAP⁡Kd↔∃m∈0…K−1x=a+m⁢d
57 56 imbi1d ⊢φ∧a∈ℕ∧d∈ℕ→x∈aAP⁡Kd→x∈F-1c↔∃m∈0…K−1x=a+m⁢d→x∈F-1c
58 57 albidv ⊢φ∧a∈ℕ∧d∈ℕ→∀xx∈aAP⁡Kd→x∈F-1c↔∀x∃m∈0…K−1x=a+m⁢d→x∈F-1c
59 dfss2 ⊢aAP⁡Kd⊆F-1c↔∀xx∈aAP⁡Kd→x∈F-1c
60 ralcom4 ⊢∀m∈0…K−1∀xx=a+m⁢d→x∈F-1c↔∀x∀m∈0…K−1x=a+m⁢d→x∈F-1c
61 ovex ⊢a+m⁢d∈V
62 eleq1 ⊢x=a+m⁢d→x∈F-1c↔a+m⁢d∈F-1c
63 61 62 ceqsalv ⊢∀xx=a+m⁢d→x∈F-1c↔a+m⁢d∈F-1c
64 63 ralbii ⊢∀m∈0…K−1∀xx=a+m⁢d→x∈F-1c↔∀m∈0…K−1a+m⁢d∈F-1c
65 r19.23v ⊢∀m∈0…K−1x=a+m⁢d→x∈F-1c↔∃m∈0…K−1x=a+m⁢d→x∈F-1c
66 65 albii ⊢∀x∀m∈0…K−1x=a+m⁢d→x∈F-1c↔∀x∃m∈0…K−1x=a+m⁢d→x∈F-1c
67 60 64 66 3bitr3i ⊢∀m∈0…K−1a+m⁢d∈F-1c↔∀x∃m∈0…K−1x=a+m⁢d→x∈F-1c
68 58 59 67 3bitr4g ⊢φ∧a∈ℕ∧d∈ℕ→aAP⁡Kd⊆F-1c↔∀m∈0…K−1a+m⁢d∈F-1c
69 68 2rexbidva ⊢φ→∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c↔∃a∈ℕ∃d∈ℕ∀m∈0…K−1a+m⁢d∈F-1c
70 69 rexbidv ⊢φ→∃c∈R∃a∈ℕ∃d∈ℕaAP⁡Kd⊆F-1c↔∃c∈R∃a∈ℕ∃d∈ℕ∀m∈0…K−1a+m⁢d∈F-1c
71 5 53 70 3bitrd ⊢φ→KMonoAPF↔∃c∈R∃a∈ℕ∃d∈ℕ∀m∈0…K−1a+m⁢d∈F-1c